The units congruent to one modulo an ideal

For an ideal I of a ring R, the units u with u - 1 ∈ I form a subgroup of Rˣ, the principal unit group of I. The name is borrowed from Mathlib's ValuationSubring.principalUnitGroup, which for a valuation subring A of a field K is a subgroup of Kˣ; under ValuationSubring.unitGroupMulEquiv it corresponds to this subgroup of Aˣ for the maximal ideal of A. Here I is arbitrary. When I consists of topologically nilpotent elements of a complete linearly topologized ℚ-algebra, the exponential is an isomorphism from the additive group of I onto this group (Ideal.expMulEquiv).

The principal unit group of I is the kernel of reduction of units modulo I, and when I lies in the Jacobson radical this reduction is surjective, so that Rˣ ⧸ (1 + I) ≃ (R ⧸ I)ˣ. For ideals J' ≤ J with J * J ≤ J' and J in the Jacobson radical, the map 1 + x ↦ x identifies (1 + J) ⧸ (1 + J') with the additive group J ⧸ J', because (1 + x)(1 + y) = 1 + (x + y) + x y with x y ∈ J'. Without J' ≤ J, the same map identifies (1 + J) ⧸ ((1 + J) ∩ (1 + J')) with J ⧸ (J ∩ J'); these are the quotients the API states, via Subgroup.subgroupOf and Submodule.comap J.subtype J'. Applied to the powers of an ideal I in the Jacobson radical, this gives the filtration of 1 + I by the subgroups 1 + I ^ n, whose successive quotients are the additive groups I ^ n ⧸ I ^ (n + 1). When I ^ n = 0 the filtration reaches the trivial group at step n (principalUnitGroup_bot), so 1 + I is an iterated extension of additive groups.

Main definitions

• Ideal.principalUnitGroup: the units u with u - 1 ∈ I.
• Ideal.unitsQuotientPrincipalUnitGroupEquiv: for I in the Jacobson radical, Rˣ ⧸ (1 + I) ≃* (R ⧸ I)ˣ.
• Ideal.principalUnitGroupToQuotient: for J * J ≤ J', the homomorphism 1 + x ↦ x mod J' from 1 + J to the additive group of J ⧸ (J ∩ J'), which is J ⧸ J' when J' ≤ J.
• Ideal.principalUnitGroupQuotientEquiv: for J * J ≤ J' and J in the Jacobson radical, (1 + J) ⧸ ((1 + J) ∩ (1 + J')) ≃* J ⧸ (J ∩ J'), which reads (1 + J) ⧸ (1 + J') ≃* J ⧸ J' when J' ≤ J.
• Ideal.principalUnitGroupPowQuotientEquiv: the successive quotients (1 + I ^ (n + 1)) ⧸ (1 + I ^ (n + 2)) ≃* I ^ (n + 1) ⧸ I ^ (n + 2) of the filtration by powers.

Main results

• Ideal.principalUnitGroup_ker: the principal unit group of the kernel of a ring homomorphism is the kernel of the induced map on units.
• Ideal.unitsMap_quotientMk_surjective: reduction of units modulo an ideal in the Jacobson radical is surjective.
• Ideal.principalUnitGroup_pow_antitone: the subgroups 1 + I ^ n decrease with n.

References

• J.-P. Serre, Local Fields, Chapter IV, §2, for the filtration of the units of a local ring.

def Ideal.principalUnitGroup {R : Type u_1} [Ring R] (I : Ideal R) : Subgroup Rˣ

The principal unit group of an ideal I: the units u with u - 1 ∈ I.

@[simp]

theorem Ideal.mem_principalUnitGroup {R : Type u_1} [Ring R] {I : Ideal R} {u : Rˣ} : u ∈ I.principalUnitGroup ↔ ↑u - 1 ∈ I

theorem Ideal.principalUnitGroup_mono {R : Type u_1} [Ring R] : Monotone principalUnitGroup

@[simp]

theorem Ideal.principalUnitGroup_top {R : Type u_1} [Ring R] : ⊤.principalUnitGroup = ⊤

@[simp]

theorem Ideal.principalUnitGroup_bot {R : Type u_1} [Ring R] : ⊥.principalUnitGroup = ⊥

theorem Ideal.principalUnitGroup_ker {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (f : R →+* S) : (RingHom.ker f).principalUnitGroup = (Units.map ↑f).ker

The principal unit group of the kernel of a ring homomorphism is the kernel of the induced map on units.

theorem Ideal.principalUnitGroup_pow_antitone {R : Type u_2} [CommRing R] (I : Ideal R) : Antitone fun (n : ℕ) => (I ^ n).principalUnitGroup

theorem Ideal.principalUnitGroup_eq_ker_unitsMap {R : Type u_2} [CommRing R] (I : Ideal R) : I.principalUnitGroup = (Units.map ↑(Quotient.mk I)).ker

The principal unit group of I is the kernel of reduction of units modulo I.

theorem Ideal.unitsMap_quotientMk_surjective {R : Type u_2} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) : Function.Surjective ⇑(Units.map ↑(Quotient.mk I))

Reduction of units modulo an ideal contained in the Jacobson radical is surjective.

noncomputable def Ideal.unitsQuotientPrincipalUnitGroupEquiv {R : Type u_2} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) : Rˣ ⧸ I.principalUnitGroup ≃* (R ⧸ I)ˣ

For an ideal I contained in the Jacobson radical, the units of R modulo the principal unit group of I are the units of R ⧸ I.

@[simp]

theorem Ideal.unitsQuotientPrincipalUnitGroupEquiv_mk {R : Type u_2} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) (u : Rˣ) : (unitsQuotientPrincipalUnitGroupEquiv hI) ↑u = (Units.map ↑(Quotient.mk I)) u

def Ideal.principalUnitGroupToQuotient {R : Type u_2} [CommRing R] (J J' : Ideal R) (h : J * J ≤ J') : ↥J.principalUnitGroup →* Multiplicative (↥J ⧸ Submodule.comap (Submodule.subtype J) J')

For ideals with J * J ≤ J', the map 1 + x ↦ x mod J' is a homomorphism from the principal unit group of J to the additive group of J ⧸ (J ∩ J') (written Submodule.comap J.subtype J'; this is J ⧸ J' when J' ≤ J): (1 + x)(1 + y) = 1 + (x + y) + x y with x y ∈ J'.

@[simp]

theorem Ideal.principalUnitGroupToQuotient_apply {R : Type u_2} [CommRing R] {J J' : Ideal R} (h : J * J ≤ J') (u : ↥J.principalUnitGroup) : (J.principalUnitGroupToQuotient J' h) u = Multiplicative.ofAdd (Submodule.Quotient.mk ⟨↑↑u - 1, ⋯⟩)

theorem Ideal.ker_principalUnitGroupToQuotient {R : Type u_2} [CommRing R] {J J' : Ideal R} (h : J * J ≤ J') : (J.principalUnitGroupToQuotient J' h).ker = J'.principalUnitGroup.subgroupOf J.principalUnitGroup

theorem Ideal.principalUnitGroupToQuotient_surjective {R : Type u_2} [CommRing R] {J J' : Ideal R} (h : J * J ≤ J') (hJ : J ≤ ⊥.jacobson) : Function.Surjective ⇑(J.principalUnitGroupToQuotient J' h)

When J lies in the Jacobson radical, every element of J ⧸ (J ∩ J') is the class of u - 1 for a principal unit u of J: if x ∈ J, then 1 + x is a unit.

noncomputable def Ideal.principalUnitGroupQuotientEquiv {R : Type u_2} [CommRing R] {J J' : Ideal R} (h : J * J ≤ J') (hJ : J ≤ ⊥.jacobson) : ↥J.principalUnitGroup ⧸ J'.principalUnitGroup.subgroupOf J.principalUnitGroup ≃* Multiplicative (↥J ⧸ Submodule.comap (Submodule.subtype J) J')

For ideals with J * J ≤ J' and J contained in the Jacobson radical, the quotient of the principal unit group of J by its intersection with that of J' is the additive group J ⧸ (J ∩ J'), by 1 + x ↦ x. When J' ≤ J this is (1 + J) ⧸ (1 + J') ≃* J ⧸ J'.

@[simp]

theorem Ideal.principalUnitGroupQuotientEquiv_mk {R : Type u_2} [CommRing R] {J J' : Ideal R} (h : J * J ≤ J') (hJ : J ≤ ⊥.jacobson) (u : ↥J.principalUnitGroup) : (principalUnitGroupQuotientEquiv h hJ) ↑u = (J.principalUnitGroupToQuotient J' h) u

noncomputable def Ideal.principalUnitGroupPowQuotientEquiv {R : Type u_2} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) (n : ℕ) : ↥(I ^ (n + 1)).principalUnitGroup ⧸ (I ^ (n + 2)).principalUnitGroup.subgroupOf (I ^ (n + 1)).principalUnitGroup ≃* Multiplicative (↥(I ^ (n + 1)) ⧸ Submodule.comap (Submodule.subtype (I ^ (n + 1))) (I ^ (n + 2)))

The successive quotients of the filtration of the principal unit group of an ideal I in the Jacobson radical by the principal unit groups of its powers: (1 + I ^ (n + 1)) ⧸ (1 + I ^ (n + 2)) ≃* I ^ (n + 1) ⧸ I ^ (n + 2), by 1 + x ↦ x.

@[simp]

theorem Ideal.principalUnitGroupPowQuotientEquiv_mk {R : Type u_2} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) (n : ℕ) (u : ↥(I ^ (n + 1)).principalUnitGroup) : (principalUnitGroupPowQuotientEquiv hI n) ↑u = Multiplicative.ofAdd (Submodule.Quotient.mk ⟨↑↑u - 1, ⋯⟩)