The maximal elementary-2 quotient Cl(R)/Cl(R)² of a class group

For a domain R (for the genus-theory application, the ring of integers 𝓞 K of a number field, whose class group is finite), the class group ClassGroup R is an abelian group, and genus theory studies its 2-part through the quotient by its subgroup of squares, Cl(R) / Cl(R)². Every element of this quotient has order dividing 2, so it is a vector space over 𝔽₂ = ZMod 2; its dimension is the 2-rank of the class group, the quantity the genus-field theorems compute.

⚠ This quotient is the maximal elementary-2 quotient of the class group, not the 2-torsion subgroup Cl(R)[2] = {C | C² = 1}. The two are different objects — a quotient and a subgroup — but for a finite abelian group they have the same cardinality (see card_elementaryTwoQuotient_eq_card_twoTorsion); we keep them distinct in names and statements.

The construction itself is the general TauCeti.ElementaryTwoQuotient of a commutative group, specialized here to G = ClassGroup R under the genus-theory names Layer 2 of the multiquadratic roadmap targets (TauCetiRoadmap/Multiquadratic/README.md). The same general construction is the square-class group Kˣ ⧸ (Kˣ)² of TauCeti.FieldTheory.SquareClassGroup.Basic for G = Kˣ.

Main definitions and results

• TauCeti.ClassGroup.ElementaryTwoQuotient: the quotient Cl(R) ⧸ Cl(R)², a ZMod 2-module.
• TauCeti.ClassGroup.elementaryTwoQuotientMk and elementaryTwoQuotientMk_eq_zero_iff: the class of an ideal class, trivial iff that class is a square; elementaryTwoQuotientMk_mul, elementaryTwoQuotientMk_one, elementaryTwoQuotientMk_inv, elementaryTwoQuotientMk_div, elementaryTwoQuotientMk_pow, and elementaryTwoQuotientMk_prod record its additivity, while elementaryTwoQuotientMk_surjective and elementaryTwoQuotientMk_eq_iff give surjectivity and the equality criterion.
• TauCeti.ClassGroup.elementaryTwoQuotientCongr: a multiplicative equivalence of class groups induces a ZMod 2-linear equivalence of their elementary-2 quotients, with elementaryTwoQuotientCongr_apply_eq_self_of_apply_eq_inv recording that an automorphism acting pointwise by inversion (e.g. quadratic conjugation) is the identity on Cl(R)/Cl(R)².
• TauCeti.ClassGroup.card_elementaryTwoQuotient_eq_card_twoTorsion: |Cl(R)/Cl(R)²| = |Cl(R)[2]|, the quotient and the 2-torsion subgroup have equal cardinality.
• TauCeti.ClassGroup.twoRank and card_elementaryTwoQuotient_eq_two_pow_twoRank: the 2-rank, with |Cl(R)/Cl(R)²| = 2 ^ twoRank.
• TauCeti.ClassGroup.card_elementaryTwoQuotient_dvd_card and TauCeti.ClassGroup.two_pow_twoRank_dvd_card: the quotient cardinality and its rank form divide the class-group cardinality.

@[reducible, inline]

abbrev TauCeti.ClassGroup.ElementaryTwoQuotient (R : Type u_1) [CommRing R] [IsDomain R] : Type u_1

The maximal elementary-2 quotient Cl(R)/Cl(R)² of the class group, the general TauCeti.ElementaryTwoQuotient specialized to ClassGroup R.

Equations

• TauCeti.ClassGroup.ElementaryTwoQuotient R = TauCeti.ElementaryTwoQuotient (ClassGroup R)

noncomputable def TauCeti.ClassGroup.elementaryTwoQuotientMk (R : Type u_1) [CommRing R] [IsDomain R] (C : ClassGroup R) : ElementaryTwoQuotient R

The class of an ideal class in the maximal elementary-2 quotient Cl(R)/Cl(R)².

Equations

• TauCeti.ClassGroup.elementaryTwoQuotientMk R C = TauCeti.elementaryTwoQuotientMk C

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_eq_zero_iff (R : Type u_1) [CommRing R] [IsDomain R] (C : ClassGroup R) : elementaryTwoQuotientMk R C = 0 ↔ IsSquare C

An ideal class has trivial class in Cl(R)/Cl(R)² iff it is a square.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_mul (R : Type u_1) [CommRing R] [IsDomain R] (C D : ClassGroup R) : elementaryTwoQuotientMk R (C * D) = elementaryTwoQuotientMk R C + elementaryTwoQuotientMk R D

The class map to Cl(R)/Cl(R)² sends a product of ideal classes to the sum of the classes.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_one (R : Type u_1) [CommRing R] [IsDomain R] : elementaryTwoQuotientMk R 1 = 0

The class map to Cl(R)/Cl(R)² sends the trivial ideal class to 0.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_inv (R : Type u_1) [CommRing R] [IsDomain R] (C : ClassGroup R) : elementaryTwoQuotientMk R C⁻¹ = -elementaryTwoQuotientMk R C

The class map to Cl(R)/Cl(R)² sends inverses to negatives.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_div (R : Type u_1) [CommRing R] [IsDomain R] (C D : ClassGroup R) : elementaryTwoQuotientMk R (C / D) = elementaryTwoQuotientMk R C - elementaryTwoQuotientMk R D

The class map to Cl(R)/Cl(R)² sends quotients to differences.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_pow (R : Type u_1) [CommRing R] [IsDomain R] (C : ClassGroup R) (n : ℕ) : elementaryTwoQuotientMk R (C ^ n) = n • elementaryTwoQuotientMk R C

The class map to Cl(R)/Cl(R)² sends powers to scalar multiples.

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_prod (R : Type u_1) [CommRing R] [IsDomain R] {ι : Type u_2} (S : Finset ι) (C : ι → ClassGroup R) : elementaryTwoQuotientMk R (∏ i ∈ S, C i) = ∑ i ∈ S, elementaryTwoQuotientMk R (C i)

The class map to Cl(R)/Cl(R)² sends a finite product of ideal classes to the sum of the classes.

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_surjective (R : Type u_1) [CommRing R] [IsDomain R] : Function.Surjective (elementaryTwoQuotientMk R)

Every element of Cl(R)/Cl(R)² is the class of some ideal class.

theorem TauCeti.ClassGroup.elementaryTwoQuotientMk_eq_iff (R : Type u_1) [CommRing R] [IsDomain R] (C D : ClassGroup R) : elementaryTwoQuotientMk R C = elementaryTwoQuotientMk R D ↔ IsSquare (C / D)

Two ideal classes have the same class in Cl(R)/Cl(R)² iff they differ by a square.

noncomputable def TauCeti.ClassGroup.elementaryTwoQuotientCongr {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] (e : ClassGroup R ≃* ClassGroup S) : ElementaryTwoQuotient R ≃ₗ[ZMod 2] ElementaryTwoQuotient S

A multiplicative equivalence of class groups induces a ZMod 2-linear equivalence on the maximal elementary-2 quotients. This is the transport API used when genus-field constructions identify class groups through canonical isomorphisms.

Equations

• TauCeti.ClassGroup.elementaryTwoQuotientCongr e = TauCeti.elementaryTwoQuotientCongr e

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientCongr_mk {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] (e : ClassGroup R ≃* ClassGroup S) (C : ClassGroup R) : (elementaryTwoQuotientCongr e) (elementaryTwoQuotientMk R C) = elementaryTwoQuotientMk S (e C)

The induced equivalence on Cl/Cl² sends the class of an ideal class to the class of its image.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientCongr_symm_mk {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] (e : ClassGroup R ≃* ClassGroup S) (C : ClassGroup S) : (elementaryTwoQuotientCongr e).symm (elementaryTwoQuotientMk S C) = elementaryTwoQuotientMk R (e.symm C)

The inverse induced equivalence on Cl/Cl² sends the class of an ideal class to the class of its inverse image.

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientCongr_refl_apply {R : Type u_1} [CommRing R] [IsDomain R] (x : ElementaryTwoQuotient R) : (elementaryTwoQuotientCongr (MulEquiv.refl (ClassGroup R))) x = x

The identity equivalence of class groups induces the identity equivalence on Cl/Cl².

@[simp]

theorem TauCeti.ClassGroup.elementaryTwoQuotientCongr_trans_apply {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_2} {T : Type u_3} [CommRing S] [IsDomain S] [CommRing T] [IsDomain T] (e : ClassGroup R ≃* ClassGroup S) (e' : ClassGroup S ≃* ClassGroup T) (x : ElementaryTwoQuotient R) : (elementaryTwoQuotientCongr (e.trans e')) x = (elementaryTwoQuotientCongr e') ((elementaryTwoQuotientCongr e) x)

Induced class-group equivalences on Cl/Cl² compose functorially.

theorem TauCeti.ClassGroup.elementaryTwoQuotientCongr_apply_eq_self_of_apply_eq_inv {R : Type u_1} [CommRing R] [IsDomain R] (e : ClassGroup R ≃* ClassGroup R) (he : ∀ (C : ClassGroup R), e C = C⁻¹) (x : ElementaryTwoQuotient R) : (elementaryTwoQuotientCongr e) x = x

An automorphism of the class group that acts pointwise by inversion induces the identity on the maximal elementary-2 quotient Cl(R)/Cl(R)². In genus theory this is the action of quadratic conjugation, which sends each ideal class to its inverse. This is the reusable class-group form of the generic TauCeti.elementaryTwoQuotientCongr_apply_eq_self_of_apply_eq_inv; it is stated here, where elementaryTwoQuotientCongr is exposed, so consumers in other modules (where the def is opaque) can apply it without unfolding.

noncomputable def TauCeti.ClassGroup.twoRank (R : Type u_1) [CommRing R] [IsDomain R] : ℕ

The 2-rank of the class group: the ZMod 2 dimension of the maximal elementary-2 quotient Cl(R)/Cl(R)² (zero, by convention of Module.finrank, when the quotient is infinite-dimensional). In genus-theory applications the t - 1 formula belongs to the narrow class group; for imaginary fields the narrow and ordinary class groups coincide.

Equations

• TauCeti.ClassGroup.twoRank R = TauCeti.twoRank (ClassGroup R)

@[simp]

theorem TauCeti.ClassGroup.twoRank_def (R : Type u_1) [CommRing R] [IsDomain R] : twoRank R = Module.finrank (ZMod 2) (ElementaryTwoQuotient R)

The 2-rank of the class group is the ZMod 2 dimension of its maximal elementary-2 quotient Cl(R) / Cl(R)².

theorem TauCeti.ClassGroup.card_elementaryTwoQuotient_eq_two_pow_twoRank (R : Type u_1) [CommRing R] [IsDomain R] [Module.Finite (ZMod 2) (ElementaryTwoQuotient R)] : Nat.card (ElementaryTwoQuotient R) = 2 ^ twoRank R

The maximal elementary-2 quotient has cardinality 2 ^ twoRank: it is a finite 𝔽₂-vector space of dimension the 2-rank.

theorem TauCeti.ClassGroup.finrank_elementaryTwoQuotient_eq_of_mulEquiv (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] (e : ClassGroup R ≃* ClassGroup S) : Module.finrank (ZMod 2) (ElementaryTwoQuotient R) = Module.finrank (ZMod 2) (ElementaryTwoQuotient S)

Multiplicatively equivalent class groups have Cl/Cl² quotients with the same ZMod 2 finrank.

theorem TauCeti.ClassGroup.twoRank_eq_of_mulEquiv (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_2} [CommRing S] [IsDomain S] (e : ClassGroup R ≃* ClassGroup S) : twoRank R = twoRank S

Multiplicatively equivalent class groups have the same elementary-2 rank.

theorem TauCeti.ClassGroup.card_elementaryTwoQuotient_dvd_card (R : Type u_1) [CommRing R] [IsDomain R] : Nat.card (ElementaryTwoQuotient R) ∣ Nat.card (ClassGroup R)

The cardinality of Cl(R)/Cl(R)² divides the cardinality of Cl(R) when the class group is finite, and more generally in Mathlib's cardinal arithmetic.

theorem TauCeti.ClassGroup.two_pow_twoRank_dvd_card (R : Type u_1) [CommRing R] [IsDomain R] [Module.Finite (ZMod 2) (ElementaryTwoQuotient R)] : 2 ^ twoRank R ∣ Nat.card (ClassGroup R)

Rank form of TauCeti.ClassGroup.card_elementaryTwoQuotient_dvd_card: 2 ^ TauCeti.ClassGroup.twoRank R divides the cardinality of Cl(R) when Cl(R)/Cl(R)² is finite-dimensional.

instance TauCeti.ClassGroup.instFiniteZModOfNatNatElementaryTwoQuotient (R : Type u_1) [CommRing R] [IsDomain R] [Finite (ClassGroup R)] : Module.Finite (ZMod 2) (ElementaryTwoQuotient R)

A finite class group has finite-dimensional elementary-2 quotient.

theorem TauCeti.ClassGroup.card_elementaryTwoQuotient_le_card (R : Type u_1) [CommRing R] [IsDomain R] [Finite (ClassGroup R)] : Nat.card (ElementaryTwoQuotient R) ≤ Nat.card (ClassGroup R)

The elementary-2 quotient of a finite class group has cardinality at most the class-group cardinality.

theorem TauCeti.ClassGroup.two_pow_twoRank_le_card (R : Type u_1) [CommRing R] [IsDomain R] [Finite (ClassGroup R)] : 2 ^ twoRank R ≤ Nat.card (ClassGroup R)

Rank form of TauCeti.ClassGroup.card_elementaryTwoQuotient_le_card: 2 ^ TauCeti.ClassGroup.twoRank R is bounded by the cardinality of Cl(R).

theorem TauCeti.ClassGroup.card_elementaryTwoQuotient_eq_card_twoTorsion (R : Type u_1) [CommRing R] [IsDomain R] [Finite (ClassGroup R)] : Nat.card (ElementaryTwoQuotient R) = Nat.card { C : ClassGroup R // C ^ 2 = 1 }

The maximal elementary-2 quotient and the 2-torsion subgroup have the same cardinality. |Cl(R)/Cl(R)²| = |Cl(R)[2]|.