Principal unit groups 1 + p^f ℤ_p, their closed subgroups, and pro-p subgroups of ℤ_pˣ

For a prime p and f : ℕ, the principal unit group of level f is U^(f) = 1 + p^f ℤ_p ≤ ℤ_pˣ, the kernel of reduction modulo p ^ f on units. The groups U^(f) are open, closed, decreasing, with trivial intersection, and they form a neighbourhood basis of 1 in ℤ_pˣ; the index of U^(f) in ℤ_pˣ is Euler's totient φ(p ^ f).

The main results are about the structure of these groups as topological groups. Raising to the p ^ k-th power moves an element of exact level f (in U^(f) but not in U^(f+1)) to exact level f + k, provided f ≥ 1, and f ≥ 2 when p = 2 (the lifting-the-exponent step, read off from Mathlib's expansion (1 + p^f x)^(p^k) = 1 + p^(f+k) (x + p y), ZMod.exists_one_add_mul_pow_prime_pow_eq; for p = 2 and f = 1 it fails, since (-1)^2 = 1). Hence an element of exact level f generates each finite quotient U^(f) / U^(f+k), which is cyclic of order p ^ k, so the closed subgroup it generates is all of U^(f): the groups U^(f) are procyclic. Consequently every nontrivial closed subgroup of 1 + pℤ_p (of 1 + 4ℤ_2 when p = 2) is one of the U^(f), and f is determined by the subgroup through its index.

The case p = 2 is the input to the description of all closed subgroups of ℤ_2ˣ, which are sorted by how they sit over {±1} inside ℤ_2ˣ = {±1} × (1 + 4ℤ_2).

The filtration also identifies the pro-p subgroups of the profinite group ℤ_pˣ: they are exactly the subgroups of 1 + pℤ_p. Every U^(f) with f ≥ 1 is pro-p, because its finite quotients U^(f) / U^(f+k) have order p ^ k, and a pro-p subgroup has trivial image in the quotient ℤ_pˣ / (1 + pℤ_p) of order p - 1. For p = 2 the principal unit group 1 + 2ℤ_2 is all of ℤ_2ˣ, so every subgroup of ℤ_2ˣ is pro-2.

Main declarations

• TauCeti.unitsPrincipal p f: the principal unit group U^(f) = 1 + p^f ℤ_p, with TauCeti.mem_unitsPrincipal_iff (u ∈ U^(f) ↔ p ^ f ∣ u - 1) and its norm form; at level one, TauCeti.mem_unitsPrincipal_one_iff_toZMod and TauCeti.mem_unitsPrincipal_one_iff_residue read the condition in ℤ/pℤ and in the residue field, and TauCeti.unitsPrincipal_one_eq_ker_unitsMap_residue identifies U^(1) with the kernel of reduction on units.
• TauCeti.unitsPrincipalMk: the element of U^(f) with a prescribed value v ≡ 1 mod p ^ f.
• TauCeti.isOpen_unitsPrincipal, TauCeti.isClosed_unitsPrincipal, TauCeti.unitsPrincipal_antitone, TauCeti.iInf_unitsPrincipal_eq_bot, TauCeti.hasBasis_nhds_one_unitsPrincipal: the topology of the filtration.
• TauCeti.index_unitsPrincipal: [ℤ_pˣ : U^(f)] = φ(p ^ f), so p ^ (f - 1) * (p - 1) for f ≥ 1, and 2 ^ (f - 1) for p = 2; TauCeti.relIndex_unitsPrincipal: [U^(f) : U^(f+k)] = p ^ k for f ≥ 1.
• TauCeti.exists_mem_unitsPrincipal_and_notMem_succ: every unit other than 1 has an exact level.
• TauCeti.neg_one_mem_unitsPrincipal_two_iff, TauCeti.neg_mem_unitsPrincipal_two_two_iff: in ℤ_2ˣ, -1 ∉ U^(f) for f ≥ 2, and u ≡ ±1 mod 4 with exactly one sign; TauCeti.inv_mul_mem_unitsPrincipal_two_succ: two dyadic units of the same exact level are congruent modulo the next level.
• TauCeti.pow_pow_mem_unitsPrincipal, TauCeti.pow_pow_notMem_unitsPrincipal: the p ^ k-th power of an element of exact level f has exact level f + k.
• TauCeti.infinite_unitsPrincipal: every U^(f) is infinite.
• TauCeti.topologicalClosure_zpowers_eq_unitsPrincipal: an element of exact level f topologically generates U^(f); TauCeti.exists_topologicalClosure_zpowers_eq_unitsPrincipal: U^(f) is procyclic.
• TauCeti.map_powMonoidHom_unitsPrincipal: (U^(f))^p = U^(f+1), the subgroup of p-th powers of U^(f); TauCeti.relIndex_map_powMonoidHom_unitsPrincipal: (U^(f) : (U^(f))^p) = p.
• TauCeti.exists_eq_unitsPrincipal_of_isClosed: a nontrivial closed subgroup of U^(f₀) is some U^(f) with f ≥ f₀; TauCeti.unitsPrincipal_inj, TauCeti.unitsPrincipal_injective: the level is unique, at every level when p is odd; TauCeti.exists_topologicalClosure_zpowers_eq_of_isClosed_of_le_unitsPrincipal: every closed subgroup of U^(f₀) is procyclic.
• TauCeti.isProP_unitsPrincipal: 1 + p^f ℤ_p is pro-p for f ≥ 1.
• TauCeti.IsProP.le_unitsPrincipal_one, TauCeti.isProP_iff_le_unitsPrincipal_one: a subgroup of ℤ_pˣ is pro-p exactly when it lies in 1 + pℤ_p.
• TauCeti.isProP_two_subgroup_units: every subgroup of ℤ_2ˣ is pro-2.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition 5.7.
• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), the remark following the corollary to Theorem 4.

noncomputable def TauCeti.unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : Subgroup ℤ_[p]ˣ

The principal unit group of level f, U^(f) = 1 + p^f ℤ_p: the kernel of reduction modulo p ^ f on the units of ℤ_p. At f = 0 it is all of ℤ_pˣ.

Equations

• TauCeti.unitsPrincipal p f = (Units.map ↑(PadicInt.toZModPow f)).ker

@[simp]

theorem TauCeti.mem_unitsPrincipal_iff_toZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} {u : ℤ_[p]ˣ} : u ∈ unitsPrincipal p f ↔ (PadicInt.toZModPow f) ↑u = 1

A unit lies in U^(f) iff it reduces to 1 modulo p ^ f.

theorem TauCeti.mem_unitsPrincipal_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} {u : ℤ_[p]ˣ} : u ∈ unitsPrincipal p f ↔ ↑p ^ f ∣ ↑u - 1

u ∈ U^(f) iff u ≡ 1 mod p ^ f.

theorem TauCeti.mem_unitsPrincipal_iff_norm {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} {u : ℤ_[p]ˣ} : u ∈ unitsPrincipal p f ↔ ‖↑u - 1‖ ≤ ↑p ^ (-↑f)

u ∈ U^(f) iff ‖u - 1‖ ≤ p ^ (-f).

theorem TauCeti.mem_unitsPrincipal_one_iff_toZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} : u ∈ unitsPrincipal p 1 ↔ PadicInt.toZMod ↑u = 1

u ∈ U^(1) iff u ≡ 1 mod p, read in ℤ/pℤ.

theorem TauCeti.mem_unitsPrincipal_one_iff_residue {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} : u ∈ unitsPrincipal p 1 ↔ (IsLocalRing.residue ℤ_[p]) ↑u = 1

u ∈ U^(1) iff u reduces to 1 in the residue field of ℤ_p.

noncomputable def TauCeti.unitsPrincipalMk {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : f ≠ 0) {v : ℤ_[p]} (hv : ↑p ^ f ∣ v - 1) : ↥(unitsPrincipal p f)

The principal unit of level f ≠ 0 with a prescribed value: for v ≡ 1 mod p ^ f, the unit v of ℤ_p, as an element of U^(f).

Equations

• TauCeti.unitsPrincipalMk hf hv = ⟨⋯.unit, ⋯⟩

@[simp]

theorem TauCeti.coe_unitsPrincipalMk {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : f ≠ 0) {v : ℤ_[p]} (hv : ↑p ^ f ∣ v - 1) : ↑↑(unitsPrincipalMk hf hv) = v

theorem TauCeti.unitsPrincipal_one_eq_ker_unitsMap_residue (p : ℕ) [hp : Fact (Nat.Prime p)] : unitsPrincipal p 1 = (Units.map ↑(IsLocalRing.residue ℤ_[p])).ker

The principal unit group 1 + pℤ_p is the kernel of reduction on units.

@[simp]

theorem TauCeti.unitsPrincipal_zero (p : ℕ) [hp : Fact (Nat.Prime p)] : unitsPrincipal p 0 = ⊤

theorem TauCeti.unitsPrincipal_antitone (p : ℕ) [hp : Fact (Nat.Prime p)] : Antitone (unitsPrincipal p)

The principal unit groups decrease with the level.

theorem TauCeti.unitsPrincipal_ne_bot (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : unitsPrincipal p f ≠ ⊥

No principal unit group is trivial: 1 + p ^ max f 1 is an element of U^(f) other than 1.

theorem TauCeti.isOpen_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : IsOpen ↑(unitsPrincipal p f)

Every principal unit group is open: it is the kernel of a continuous map to a discrete group.

theorem TauCeti.isClosed_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : IsClosed ↑(unitsPrincipal p f)

Every principal unit group is closed: it is the kernel of a continuous map to a discrete group.

instance TauCeti.compactSpace_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] (f : ℕ) : CompactSpace ↥(unitsPrincipal p f)

The principal unit groups are compact, being closed in the compact group ℤ_pˣ.

@[simp]

theorem TauCeti.iInf_unitsPrincipal_eq_bot (p : ℕ) [hp : Fact (Nat.Prime p)] : ⨅ (f : ℕ), unitsPrincipal p f = ⊥

The principal unit groups have trivial intersection: U^(∞) = {1}.

theorem TauCeti.exists_mem_unitsPrincipal_and_notMem_succ {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℤ_[p]ˣ} (hu : u ≠ 1) : ∃ (f : ℕ), u ∈ unitsPrincipal p f ∧ u ∉ unitsPrincipal p (f + 1)

Every unit u ≠ 1 has an exact level: a f with u ∈ U^(f) but u ∉ U^(f+1), namely the p-adic valuation of u - 1.

theorem TauCeti.hasBasis_nhds_one_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] : (nhds 1).HasBasis (fun (x : ℕ) => True) fun (f : ℕ) => ↑(unitsPrincipal p f)

The principal unit groups form a neighbourhood basis of 1 in ℤ_pˣ.

Indices

@[simp]

theorem TauCeti.index_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : (unitsPrincipal p f).index = (p ^ f).totient

[ℤ_pˣ : U^(f)] = φ(p ^ f): reduction modulo p ^ f is surjective on units.

theorem TauCeti.index_unitsPrincipal_of_pos (p : ℕ) [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) : (unitsPrincipal p f).index = p ^ (f - 1) * (p - 1)

[ℤ_pˣ : U^(f)] = p ^ (f - 1) * (p - 1) for f ≥ 1.

theorem TauCeti.index_unitsPrincipal_two (f : ℕ) : (unitsPrincipal 2 f).index = 2 ^ (f - 1)

[ℤ_2ˣ : U^(f)] = 2 ^ (f - 1), including the degenerate levels f = 0, 1 of index 1.

@[simp]

theorem TauCeti.unitsPrincipal_two_one : unitsPrincipal 2 1 = ⊤

The dyadic filtration starts at level 2: U^(1) = 1 + 2ℤ_2 is all of ℤ_2ˣ.

theorem TauCeti.neg_one_mem_unitsPrincipal_two_iff {f : ℕ} : -1 ∈ unitsPrincipal 2 f ↔ f ≤ 1

-1 ∈ U^(f) in ℤ_2ˣ iff f ≤ 1: -1 ≡ 1 mod 2 ^ f iff 2 ^ f ∣ 2.

theorem TauCeti.neg_mem_unitsPrincipal_two_two_iff {u : ℤ_[2]ˣ} : -u ∈ unitsPrincipal 2 2 ↔ u ∉ unitsPrincipal 2 2

U^(2) = 1 + 4ℤ_2 has index 2 in ℤ_2ˣ and does not contain -1, so a dyadic unit u lies outside 1 + 4ℤ_2 iff -u lies inside: u ≡ 1 or u ≡ -1 mod 4, and not both.

theorem TauCeti.notMem_unitsPrincipal_two_of_neg_mem {f : ℕ} (hf : 2 ≤ f) {u : ℤ_[2]ˣ} (hu : -u ∈ unitsPrincipal 2 f) : u ∉ unitsPrincipal 2 f

For f ≥ 2, a dyadic unit and its negative are never both in U^(f).

instance TauCeti.instFiniteIndexUnitsPadicIntUnitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] (f : ℕ) : (unitsPrincipal p f).FiniteIndex

theorem TauCeti.relIndex_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (k : ℕ) : (unitsPrincipal p (f + k)).relIndex (unitsPrincipal p f) = p ^ k

[U^(f) : U^(f+k)] = p ^ k for f ≥ 1.

theorem TauCeti.inv_mul_mem_unitsPrincipal_two_succ {f : ℕ} (hf : 0 < f) {u x : ℤ_[2]ˣ} (hu : u ∈ unitsPrincipal 2 f) (hu' : u ∉ unitsPrincipal 2 (f + 1)) (hx : x ∈ unitsPrincipal 2 f) (hx' : x ∉ unitsPrincipal 2 (f + 1)) : u⁻¹ * x ∈ unitsPrincipal 2 (f + 1)

At p = 2, two elements of exact level f ≥ 1 are congruent modulo U^(f+1): the quotient U^(f) / U^(f+1) has order 2.

Lifting the exponent

theorem TauCeti.pow_pow_mem_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) {u : ℤ_[p]ˣ} (hu : u ∈ unitsPrincipal p f) (k : ℕ) : u ^ p ^ k ∈ unitsPrincipal p (f + k)

For u ≡ 1 mod p^f with f ≥ 1, u ^ (p ^ k) ≡ 1 mod p^(f+k).

theorem TauCeti.pow_pow_notMem_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : u ∈ unitsPrincipal p f) (hu' : u ∉ unitsPrincipal p (f + 1)) (k : ℕ) : u ^ p ^ k ∉ unitsPrincipal p (f + k + 1)

For u of exact level f, that is u ≡ 1 mod p^f but u ≢ 1 mod p^(f+1), the power u ^ (p ^ k) is not ≡ 1 mod p^(f+k+1), provided f ≥ 1, and f ≥ 2 when p = 2; together with pow_pow_mem_unitsPrincipal, it has exact level f + k. This is where the level restriction enters: (1 + p^f x)^(p^k) = 1 + p^(f+k) (x + p y) needs p^(f+2) ∣ p^(fp).

Procyclicity

theorem TauCeti.exists_zpow_inv_mul_mem_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : u ∈ unitsPrincipal p f) (hu' : u ∉ unitsPrincipal p (f + 1)) {x : ℤ_[p]ˣ} (hx : x ∈ unitsPrincipal p f) (k : ℕ) : ∃ (n : ℤ), (u ^ n)⁻¹ * x ∈ unitsPrincipal p (f + k)

An element u of exact level f generates U^(f) modulo every U^(f+k): each x ∈ U^(f) is congruent to a power of u modulo U^(f+k). This is the finite-level form of the procyclicity of U^(f); the quotient U^(f) / U^(f+k) is cyclic of order p ^ k generated by the class of u.

theorem TauCeti.topologicalClosure_zpowers_eq_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : u ∈ unitsPrincipal p f) (hu' : u ∉ unitsPrincipal p (f + 1)) : (Subgroup.zpowers u).topologicalClosure = unitsPrincipal p f

An element of exact level f topologically generates U^(f), provided f ≥ 1, and f ≥ 2 when p = 2.

theorem TauCeti.exists_mem_unitsPrincipal_and_notMem_succ_of_pos (p : ℕ) [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) : ∃ u ∈ unitsPrincipal p f, u ∉ unitsPrincipal p (f + 1)

Every positive level f is the exact level of some unit, namely 1 + p ^ f.

theorem TauCeti.infinite_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] (f : ℕ) : (↑(unitsPrincipal p f)).Infinite

Every principal unit group U^(f) is infinite: for each k, it contains a unit of exact level f + k + 1, and units of distinct exact levels are distinct.

theorem TauCeti.exists_topologicalClosure_zpowers_eq_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : ∃ (u : ℤ_[p]ˣ), (Subgroup.zpowers u).topologicalClosure = unitsPrincipal p f

The principal unit group U^(f) is procyclic for f ≥ 1, and f ≥ 2 when p = 2: it is the closed subgroup generated by 1 + p ^ f.

theorem TauCeti.not_isOfFinOrder_of_mem_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) {u : ℤ_[p]ˣ} (hu : u ∈ unitsPrincipal p f) (hu1 : u ≠ 1) : ¬IsOfFinOrder u

A principal unit u ≠ 1 of level f ≥ 1, with f ≥ 2 when p = 2, has infinite order.

The subgroup of p-th powers

@[simp]

theorem TauCeti.map_powMonoidHom_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : Subgroup.map (powMonoidHom p) (unitsPrincipal p f) = unitsPrincipal p (f + 1)

(U^(f))^p = U^(f+1): the p-th powers of the principal units of level f are exactly the principal units of level f + 1, for f ≥ 1, and f ≥ 2 when p = 2.

theorem TauCeti.relIndex_map_powMonoidHom_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : (Subgroup.map (powMonoidHom p) (unitsPrincipal p f)).relIndex (unitsPrincipal p f) = p

(U^(f) : (U^(f))^p) = p, for f ≥ 1, and f ≥ 2 when p = 2.

The closed subgroups of 1 + p ℤ_p

theorem TauCeti.unitsPrincipal_inj {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : ℕ} (hf : 0 < f) (hg : 0 < g) : unitsPrincipal p f = unitsPrincipal p g ↔ f = g

The level of a principal unit group is determined by the group, through its index, once the level is positive (at p = 2 the levels 0 and 1 both give all of ℤ_2ˣ).

theorem TauCeti.unitsPrincipal_injective {p : ℕ} [hp : Fact (Nat.Prime p)] (hp₂ : p ≠ 2) : Function.Injective (unitsPrincipal p)

For odd p the level is determined by the group at every level, including 0: the index of U^(f) is 1 for f = 0 and p ^ (f - 1) * (p - 1) ≥ 2 for f ≥ 1.

theorem TauCeti.exists_eq_unitsPrincipal_of_isClosed {p : ℕ} [hp : Fact (Nat.Prime p)] {f₀ : ℕ} (hf₀ : 0 < f₀) (hf₀₂ : p = 2 → 2 ≤ f₀) {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hle : A ≤ unitsPrincipal p f₀) (hA' : A ≠ ⊥) : ∃ (f : ℕ), f₀ ≤ f ∧ A = unitsPrincipal p f

Every nontrivial closed subgroup of U^(f₀) is a principal unit group U^(f) with f ≥ f₀, provided f₀ ≥ 1, and f₀ ≥ 2 when p = 2. In particular the nontrivial closed subgroups of 1 + pℤ_p for odd p, and of 1 + 4ℤ_2, are exactly the 1 + p^f ℤ_p.

theorem TauCeti.exists_topologicalClosure_zpowers_eq_of_isClosed_of_le_unitsPrincipal {p : ℕ} [hp : Fact (Nat.Prime p)] {f₀ : ℕ} (hf₀ : 0 < f₀) (hf₀₂ : p = 2 → 2 ≤ f₀) {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hle : A ≤ unitsPrincipal p f₀) : ∃ (u : ℤ_[p]ˣ), (Subgroup.zpowers u).topologicalClosure = A

Every closed subgroup of U^(f₀) is procyclic, provided f₀ ≥ 1, and f₀ ≥ 2 when p = 2: it is trivial or a principal unit group U^(f), each topologically generated by one element.

The pro-p subgroups of ℤ_pˣ

theorem TauCeti.isProP_unitsPrincipal (p : ℕ) [hp : Fact (Nat.Prime p)] {f : ℕ} (hf : 0 < f) : IsProP p ↥(unitsPrincipal p f)

The principal unit groups are pro-p: for f ≥ 1, 1 + p^f ℤ_p is a pro-p group.

theorem TauCeti.IsProP.le_unitsPrincipal_one {p : ℕ} [hp : Fact (Nat.Prime p)] {A : Subgroup ℤ_[p]ˣ} (hA : IsProP p ↥A) : A ≤ unitsPrincipal p 1

A pro-p subgroup of ℤ_pˣ consists of principal units. Its image in the quotient ℤ_pˣ / (1 + pℤ_p), a group of order p - 1, is a p-group, hence trivial.

theorem TauCeti.isProP_iff_le_unitsPrincipal_one {p : ℕ} [hp : Fact (Nat.Prime p)] (A : Subgroup ℤ_[p]ˣ) : IsProP p ↥A ↔ A ≤ unitsPrincipal p 1

The pro-p subgroups of ℤ_pˣ are exactly the subgroups of 1 + pℤ_p.

theorem TauCeti.isProP_two_subgroup_units (A : Subgroup ℤ_[2]ˣ) : IsProP 2 ↥A

Every subgroup of ℤ_2ˣ is pro-2, because 1 + 2ℤ_2 = ℤ_2ˣ.