The maximal elementary-2 quotient G / G² of a commutative group

For a commutative group G, the quotient by its subgroup of squares, G / G², has every element of order dividing 2, so it is a vector space over 𝔽₂ = ZMod 2. When G is finite its dimension is the 2-rank of G. This file develops that construction at the level of an arbitrary commutative group; the genus-theory specialization to a class group lives in TauCeti.NumberTheory.ClassGroup.ElementaryTwoQuotient, and the square-class group Kˣ ⧸ (Kˣ)² of TauCeti.FieldTheory.SquareClassGroup.Basic is the same construction for G = Kˣ.

⚠ This quotient is the maximal elementary-2 quotient of G, not its 2-torsion subgroup {g | g² = 1}. The two are different objects — a quotient and a subgroup — but for a finite group they have the same cardinality, because the squaring endomorphism g ↦ g² has G² as its range and the 2-torsion as its kernel, and a finite group has the same cardinality as the product of the range and kernel of any endomorphism. We keep the two distinct in names and statements and record the cardinality identity as card_elementaryTwoQuotient_eq_card_twoTorsion.

This file uses Mathlib's additive quotient ModN (Additive G) 2 and adds multiplicative-square names around it. The cardinality identity is still expressed through the squaring homomorphism powMonoidHom 2 and Subgroup.index_range.

Main definitions and results

• TauCeti.ElementaryTwoQuotient: the quotient G ⧸ G², a ZMod 2-module.
• TauCeti.elementaryTwoQuotientMkAdd, TauCeti.elementaryTwoQuotientMk, and TauCeti.elementaryTwoQuotientMk_eq_zero_iff: the quotient map and the class of an element, trivial iff the element is a square; elementaryTwoQuotientMk_mul, elementaryTwoQuotientMk_one, elementaryTwoQuotientMk_inv, elementaryTwoQuotientMk_div, elementaryTwoQuotientMk_pow, and elementaryTwoQuotientMk_prod record its additivity.
• TauCeti.elementaryTwoQuotientMk_surjective and TauCeti.elementaryTwoQuotientMk_eq_iff: the class map is surjective, and two elements have the same class iff they differ by a square.
• TauCeti.elementaryTwoQuotientLiftEquiv and TauCeti.elementaryTwoQuotientLinearLiftEquiv: the universal property for maps out of G/G², inherited from ModN.liftEquiv, with TauCeti.elementaryTwoQuotientLinearLiftEquiv_symm_mk as its computation rule.
• TauCeti.elementaryTwoQuotientMap and TauCeti.elementaryTwoQuotientCongr: transport along homomorphisms and equivalences of commutative groups.
• TauCeti.elementaryTwoQuotientMap_apply_eq_self_of_isSquare_div, TauCeti.elementaryTwoQuotientMap_apply_eq_self_of_apply_eq_inv, and TauCeti.elementaryTwoQuotientCongr_apply_eq_self_of_apply_eq_inv: inversion acts trivially on the elementary-2 quotient.
• TauCeti.elementaryTwoQuotientEquivSquareQuotient: the equivalence between Mathlib's ModN model and the quotient by the additive form of G².
• TauCeti.card_elementaryTwoQuotient_eq_index_square: the quotient cardinality as the index of the subgroup of squares.
• TauCeti.card_elementaryTwoQuotient_eq_card_twoTorsion: |G/G²| = |{g | g² = 1}|.
• TauCeti.card_le_card_elementaryTwoQuotient_of_forall_sq_eq_one and TauCeti.le_twoRank_of_card_eq_two_pow: a subgroup of exponent dividing two bounds the elementary-2 quotient, hence the 2-rank, from below.
• TauCeti.sq_eq_one_of_card_elementaryTwoQuotient_eq_card: a finite group as large as G/G² has exponent dividing two.
• TauCeti.twoRank and TauCeti.card_elementaryTwoQuotient_eq_two_pow_twoRank: the 2-rank, with |G/G²| = 2 ^ twoRank, and TauCeti.twoRank_eq_of_card_elementaryTwoQuotient_eq_two_pow its inversion (|G/G²| = 2 ^ n → twoRank G = n).
• TauCeti.card_elementaryTwoQuotient_of_odd_card and TauCeti.twoRank_of_odd_card: a group of odd order has a single square class.
• TauCeti.card_elementaryTwoQuotient_dvd_card and TauCeti.two_pow_twoRank_dvd_card: the quotient cardinality and its rank form divide |G|.
• TauCeti.twoRank_eq_of_mulEquiv and TauCeti.twoRank_le_twoRank_of_surjective: the 2-rank is invariant under isomorphisms and monotonic under surjections.
• MonoidHom.twoRank_le_twoRank_add_of_card_ker_le_two_pow: a surjection with a kernel of order at most 2 ^ n drops the 2-rank by at most n, via MonoidHom.card_ker_elementaryTwoQuotientMap_le_card_ker.
• MonoidHom.twoRank_eq_twoRank_iff_ker_le_square: a surjection keeps the 2-rank exactly when its kernel consists of squares.

@[reducible, inline]

abbrev TauCeti.ElementaryTwoQuotient (G : Type u_1) [CommGroup G] : Type u_1

The maximal elementary-2 quotient G / G² of a commutative group, written additively on Additive G.

Equations

• TauCeti.ElementaryTwoQuotient G = ModN (Additive G) 2

instance TauCeti.instFiniteElementaryTwoQuotient (G : Type u_1) [CommGroup G] [Finite G] : Finite (ElementaryTwoQuotient G)

def TauCeti.elementaryTwoQuotientMkAdd {G : Type u_1} [CommGroup G] : Additive G →+ ElementaryTwoQuotient G

The quotient homomorphism Additive G →+ G/G², exposed in the ModN additive form.

Equations

• TauCeti.elementaryTwoQuotientMkAdd = ModN.mkQ 2

def TauCeti.elementaryTwoQuotientMk {G : Type u_1} [CommGroup G] (g : G) : ElementaryTwoQuotient G

The class of an element of G in the maximal elementary-2 quotient G / G².

Equations

• TauCeti.elementaryTwoQuotientMk g = TauCeti.elementaryTwoQuotientMkAdd (Additive.ofMul g)

theorem TauCeti.elementaryTwoQuotientMk_eq_mkQ {G : Type u_1} [CommGroup G] (g : G) : elementaryTwoQuotientMk g = Submodule.Quotient.mk (Additive.ofMul g)

The class map G → G/G² is the quotient map of the ModN model: the class of g is the image of Additive.ofMul g under the quotient by the doubling submodule. This exposes the ModN representative so downstream files can match G/G² against Mathlib's quotient-by-range API.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_eq_zero_iff {G : Type u_1} [CommGroup G] (g : G) : elementaryTwoQuotientMk g = 0 ↔ IsSquare g

An element has trivial class in G / G² iff it is a square.

def TauCeti.elementaryTwoQuotientLiftEquiv {G : Type u_1} [CommGroup G] {M : Type u_2} [AddMonoid M] : (ElementaryTwoQuotient G →+ M) ≃ { φ : Additive G →+ M // ∀ (g : Additive G), 2 • φ g = 0 }

The universal property of G/G² for additive homomorphisms: maps out of the quotient are additive homomorphisms from Additive G whose values are killed by 2.

Equations

• TauCeti.elementaryTwoQuotientLiftEquiv = ModN.liftEquiv

def TauCeti.elementaryTwoQuotientLinearLiftEquiv {G : Type u_1} [CommGroup G] {H : Type u_2} [AddCommGroup H] [Module (ZMod 2) H] : (ElementaryTwoQuotient G →ₗ[ZMod 2] H) ≃ { φ : Additive G →+ H // ∀ (g : Additive G), 2 • φ g = 0 }

The universal property of G/G² for ZMod 2-linear maps: linear maps out of the quotient are additive homomorphisms from Additive G whose values are killed by 2.

Equations

• TauCeti.elementaryTwoQuotientLinearLiftEquiv = ModN.liftEquiv'

@[simp]

theorem TauCeti.elementaryTwoQuotientLinearLiftEquiv_symm_mk {G : Type u_1} [CommGroup G] {H : Type u_2} [AddCommGroup H] [Module (ZMod 2) H] (φ : Additive G →+ H) (hφ : ∀ (g : Additive G), 2 • φ g = 0) (g : G) : (TauCeti.elementaryTwoQuotientLinearLiftEquiv.symm ⟨φ, hφ⟩) (elementaryTwoQuotientMk g) = φ (Additive.ofMul g)

The linear map obtained from the universal property of G/G² evaluates on the class of g as the original additive homomorphism evaluates on Additive.ofMul g.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_mul {G : Type u_1} [CommGroup G] (g h : G) : elementaryTwoQuotientMk (g * h) = elementaryTwoQuotientMk g + elementaryTwoQuotientMk h

The class map to G / G² sends a product to the sum of the classes.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_one {G : Type u_1} [CommGroup G] : elementaryTwoQuotientMk 1 = 0

The class map to G / G² sends 1 to 0.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_inv {G : Type u_1} [CommGroup G] (g : G) : elementaryTwoQuotientMk g⁻¹ = -elementaryTwoQuotientMk g

The class map to G / G² sends inverses to negatives.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_div {G : Type u_1} [CommGroup G] (g h : G) : elementaryTwoQuotientMk (g / h) = elementaryTwoQuotientMk g - elementaryTwoQuotientMk h

The class map to G / G² sends quotients to differences.

@[simp]

theorem TauCeti.elementaryTwoQuotientMk_pow {G : Type u_1} [CommGroup G] (g : G) (n : ℕ) : elementaryTwoQuotientMk (g ^ n) = n • elementaryTwoQuotientMk g

The class map to G / G² sends powers to scalar multiples.

theorem TauCeti.elementaryTwoQuotientMk_prod {G : Type u_1} [CommGroup G] {ι : Type u_2} (S : Finset ι) (g : ι → G) : elementaryTwoQuotientMk (∏ i ∈ S, g i) = ∑ i ∈ S, elementaryTwoQuotientMk (g i)

The class map to G / G² sends a finite product to the sum of the classes.

theorem TauCeti.elementaryTwoQuotientMk_surjective {G : Type u_1} [CommGroup G] : Function.Surjective elementaryTwoQuotientMk

Every element of G / G² is the class of some element of G.

theorem TauCeti.elementaryTwoQuotientMk_eq_iff {G : Type u_1} [CommGroup G] (g h : G) : elementaryTwoQuotientMk g = elementaryTwoQuotientMk h ↔ IsSquare (g / h)

Two elements have the same class in G / G² iff they differ by a square.

noncomputable def TauCeti.elementaryTwoQuotientMap {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (f : G →* H) : ElementaryTwoQuotient G →ₗ[ZMod 2] ElementaryTwoQuotient H

A homomorphism of commutative groups induces a ZMod 2-linear map on maximal elementary-2 quotients.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.elementaryTwoQuotientMap_mk {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (f : G →* H) (g : G) : (elementaryTwoQuotientMap f) (elementaryTwoQuotientMk g) = elementaryTwoQuotientMk (f g)

The induced map on G/G² sends the class of g to the class of f g.

theorem TauCeti.elementaryTwoQuotientMap_surjective {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (f : G →* H) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(elementaryTwoQuotientMap f)

A surjective homomorphism of commutative groups induces a surjective map on their maximal elementary-2 quotients.

@[simp]

theorem TauCeti.elementaryTwoQuotientMap_id_apply {G : Type u_1} [CommGroup G] (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientMap (MonoidHom.id G)) x = x

The map induced by the identity homomorphism fixes each class in the elementary-2 quotient.

theorem TauCeti.elementaryTwoQuotientMap_apply_eq_self_of_isSquare_div {G : Type u_1} [CommGroup G] (f : G →* G) (hf : ∀ (g : G), IsSquare (f g / g)) (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientMap f) x = x

A group endomorphism induces the identity on the maximal elementary-2 quotient if it sends each element to the same square class.

theorem TauCeti.elementaryTwoQuotientMap_apply_eq_self_of_apply_eq_inv {G : Type u_1} [CommGroup G] (f : G →* G) (hf : ∀ (g : G), f g = g⁻¹) (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientMap f) x = x

A group endomorphism that acts pointwise by inversion induces the identity on the maximal elementary-2 quotient. This is the abstract step used when quadratic conjugation acts on an ideal class group by inversion.

@[simp]

theorem TauCeti.elementaryTwoQuotientMap_comp_apply {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] {K : Type u_3} [CommGroup K] (f : G →* H) (g : H →* K) (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientMap (g.comp f)) x = (elementaryTwoQuotientMap g) ((elementaryTwoQuotientMap f) x)

Induced maps on elementary-2 quotients compose pointwise.

noncomputable def TauCeti.elementaryTwoQuotientCongr {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (e : G ≃* H) : ElementaryTwoQuotient G ≃ₗ[ZMod 2] ElementaryTwoQuotient H

A multiplicative equivalence of commutative groups induces a ZMod 2-linear equivalence of their maximal elementary-2 quotients.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.elementaryTwoQuotientCongr_mk {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (e : G ≃* H) (g : G) : (elementaryTwoQuotientCongr e) (elementaryTwoQuotientMk g) = elementaryTwoQuotientMk (e g)

The induced equivalence on G/G² sends the class of g to the class of e g.

@[simp]

theorem TauCeti.elementaryTwoQuotientCongr_symm_mk {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (e : G ≃* H) (h : H) : (elementaryTwoQuotientCongr e).symm (elementaryTwoQuotientMk h) = elementaryTwoQuotientMk (e.symm h)

The inverse induced equivalence on G/G² sends the class of h to the class of e.symm h.

@[simp]

theorem TauCeti.elementaryTwoQuotientCongr_refl_apply {G : Type u_1} [CommGroup G] (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientCongr (MulEquiv.refl G)) x = x

The identity equivalence induces the identity equivalence on the elementary-2 quotient.

@[simp]

theorem TauCeti.elementaryTwoQuotientCongr_trans_apply {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] {K : Type u_3} [CommGroup K] (e : G ≃* H) (e' : H ≃* K) (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientCongr (e.trans e')) x = (elementaryTwoQuotientCongr e') ((elementaryTwoQuotientCongr e) x)

Induced equivalences on elementary-2 quotients compose functorially.

theorem TauCeti.elementaryTwoQuotientCongr_apply_eq_self_of_apply_eq_inv {G : Type u_1} [CommGroup G] (e : G ≃* G) (he : ∀ (g : G), e g = g⁻¹) (x : ElementaryTwoQuotient G) : (elementaryTwoQuotientCongr e) x = x

A multiplicative automorphism that acts pointwise by inversion induces the identity on the maximal elementary-2 quotient. In genus theory this applies to the action of quadratic conjugation on Cl(K)/Cl(K)².

noncomputable def TauCeti.elementaryTwoQuotientEquivSquareQuotient (G : Type u_1) [CommGroup G] : ElementaryTwoQuotient G ≃+ Additive G ⧸ Subgroup.toAddSubgroup (Subgroup.square G)

Mathlib's ModN (Additive G) 2 model of G/G² agrees with the direct quotient by the additive form of the square subgroup.

Equations

• TauCeti.elementaryTwoQuotientEquivSquareQuotient G = QuotientAddGroup.quotientAddEquivOfEq ⋯

@[simp]

theorem TauCeti.elementaryTwoQuotientEquivSquareQuotient_mk (G : Type u_1) [CommGroup G] (g : G) : (elementaryTwoQuotientEquivSquareQuotient G) (elementaryTwoQuotientMk g) = ↑(Additive.ofMul g)

The comparison with the direct quotient by squares sends the ModN class of an element to its direct quotient class.

theorem TauCeti.card_elementaryTwoQuotient_eq_index_square (G : Type u_1) [CommGroup G] : Nat.card (ElementaryTwoQuotient G) = (Subgroup.square G).index

The cardinality of G/G² is the index of the subgroup of squares.

theorem TauCeti.card_elementaryTwoQuotient_eq_card_twoTorsion (G : Type u_1) [CommGroup G] [(powMonoidHom 2).ker.FiniteIndex] : Nat.card (ElementaryTwoQuotient G) = Nat.card { g : G // g ^ 2 = 1 }

The maximal elementary-2 quotient and the 2-torsion subgroup have the same cardinality. |G/G²| = |{g | g² = 1}|. The squaring endomorphism g ↦ g² has range G² and kernel the 2-torsion; when its kernel has finite index, the index of the range equals the cardinality of the kernel.

noncomputable def TauCeti.twoRank (G : Type u_1) [CommGroup G] : ℕ

The 2-rank of a commutative group: the ZMod 2-dimension of the maximal elementary-2 quotient G / G² (zero, by convention of Module.finrank, when the quotient is infinite-dimensional).

Equations

• TauCeti.twoRank G = Module.finrank (ZMod 2) (TauCeti.ElementaryTwoQuotient G)

@[simp]

theorem TauCeti.twoRank_def (G : Type u_1) [CommGroup G] : twoRank G = Module.finrank (ZMod 2) (ElementaryTwoQuotient G)

The 2-rank of G is the ZMod 2 dimension of its maximal elementary-2 quotient G / G².

theorem TauCeti.card_elementaryTwoQuotient_eq_two_pow_twoRank (G : Type u_1) [CommGroup G] [Module.Finite (ZMod 2) (ElementaryTwoQuotient G)] : Nat.card (ElementaryTwoQuotient G) = 2 ^ twoRank G

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

theorem TauCeti.twoRank_eq_of_card_elementaryTwoQuotient_eq_two_pow (G : Type u_1) [CommGroup G] {n : ℕ} (h : Nat.card (ElementaryTwoQuotient G) = 2 ^ n) : twoRank G = n

Reading the 2-rank off a cardinality computation: if G/G² has 2 ^ n elements, the 2-rank of G is n. This is the inversion of TauCeti.card_elementaryTwoQuotient_eq_two_pow_twoRank used to convert each concrete counting result into its rank form. The hypothesis already forces G/G² to be a finite ZMod 2-module, so no finiteness instance need be supplied.

theorem TauCeti.card_elementaryTwoQuotient_of_odd_card (G : Type u_1) [CommGroup G] (h : Odd (Nat.card G)) : Nat.card (ElementaryTwoQuotient G) = 1

A group of odd order has a single square class. For a finite commutative group of odd order, squaring is bijective (the exponent 2 is coprime to |G|), so G/G² is trivial. This is the odd-order half of the 2-rank computation — the even case genuinely needs more structure (a cyclic factor); this half holds for any commutative group.

theorem TauCeti.twoRank_of_odd_card (G : Type u_1) [CommGroup G] (h : Odd (Nat.card G)) : twoRank G = 0

A group of odd order has 2-rank zero.

theorem TauCeti.card_elementaryTwoQuotient_dvd_card (G : Type u_1) [CommGroup G] : Nat.card (ElementaryTwoQuotient G) ∣ Nat.card G

The cardinality of the maximal elementary-2 quotient of a commutative group divides the group cardinality.

theorem TauCeti.two_pow_twoRank_dvd_card (G : Type u_1) [CommGroup G] [Module.Finite (ZMod 2) (ElementaryTwoQuotient G)] : 2 ^ twoRank G ∣ Nat.card G

Rank form of TauCeti.card_elementaryTwoQuotient_dvd_card: when G / G² is a finite ZMod 2-vector space, 2 ^ TauCeti.twoRank G divides |G|.

theorem TauCeti.card_elementaryTwoQuotient_le_card (G : Type u_1) [CommGroup G] [Finite G] : Nat.card (ElementaryTwoQuotient G) ≤ Nat.card G

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

theorem TauCeti.two_pow_twoRank_le_card (G : Type u_1) [CommGroup G] [Finite G] : 2 ^ twoRank G ≤ Nat.card G

Rank form of TauCeti.card_elementaryTwoQuotient_le_card: for a finite commutative group G, 2 ^ TauCeti.twoRank G is at most |G|.

theorem TauCeti.card_le_card_elementaryTwoQuotient_of_forall_sq_eq_one (G : Type u_1) [CommGroup G] [Finite G] {H : Subgroup G} (hH : ∀ x ∈ H, x ^ 2 = 1) : Nat.card ↥H ≤ Nat.card (ElementaryTwoQuotient G)

A subgroup of exponent dividing two is no larger than the maximal elementary-2 quotient. Such a subgroup sits inside the 2-torsion {g | g² = 1}, which is equinumerous with G / G² (card_elementaryTwoQuotient_eq_card_twoTorsion). This is how an explicit family of independent 2-torsion elements bounds the 2-rank from below.

theorem TauCeti.le_twoRank_of_card_eq_two_pow (G : Type u_1) [CommGroup G] [Finite G] {H : Subgroup G} {r : ℕ} (hH : ∀ x ∈ H, x ^ 2 = 1) (hcard : Nat.card ↥H = 2 ^ r) : r ≤ twoRank G

A subgroup of exponent dividing two and order 2 ^ r forces the 2-rank to be at least r. The rank form of card_le_card_elementaryTwoQuotient_of_forall_sq_eq_one.

theorem TauCeti.sq_eq_one_of_card_elementaryTwoQuotient_eq_card {G : Type u_1} [CommGroup G] [Finite G] (h : Nat.card (ElementaryTwoQuotient G) = Nat.card G) (g : G) : g ^ 2 = 1

A finite commutative group as large as its maximal elementary-2 quotient has exponent dividing two. The 2-torsion {g | g² = 1} is equinumerous with G / G² (card_elementaryTwoQuotient_eq_card_twoTorsion), so it then exhausts G.

theorem TauCeti.finrank_elementaryTwoQuotient_eq_of_mulEquiv {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (e : G ≃* H) : Module.finrank (ZMod 2) (ElementaryTwoQuotient G) = Module.finrank (ZMod 2) (ElementaryTwoQuotient H)

Multiplicatively equivalent commutative groups have elementary-2 quotients with the same ZMod 2 finrank.

theorem TauCeti.twoRank_eq_of_mulEquiv {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (e : G ≃* H) : twoRank G = twoRank H

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

theorem TauCeti.twoRank_le_twoRank_of_surjective {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] [Module.Finite (ZMod 2) (ElementaryTwoQuotient G)] (f : G →* H) (hf : Function.Surjective ⇑f) : twoRank H ≤ twoRank G

A surjective homomorphism of commutative groups does not increase the 2-rank.

theorem MonoidHom.exists_mem_ker_elementaryTwoQuotientMk_eq {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (f : G →* H) (hf : Function.Surjective ⇑f) {x : TauCeti.ElementaryTwoQuotient G} (hx : (TauCeti.elementaryTwoQuotientMap f) x = 0) : ∃ g ∈ f.ker, TauCeti.elementaryTwoQuotientMk g = x

The kernel of the induced map is the image of the kernel. If f is surjective and the class of g in G / G² dies in H / H², then g may be corrected by a square so as to lie in ker f without changing its class: f g is a square f y * f y, and g * (y ^ 2)⁻¹ is a representative of the same class lying in ker f.

theorem MonoidHom.card_ker_elementaryTwoQuotientMap_le_card_ker {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] (f : G →* H) [Finite ↥f.ker] (hf : Function.Surjective ⇑f) : Nat.card ↥(TauCeti.elementaryTwoQuotientMap f).ker ≤ Nat.card ↥f.ker

The defect of the induced map is bounded by the kernel. For a surjective f : G →* H the kernel of G / G² → H / H² is the image of ker f, so it has at most |ker f| elements.

theorem MonoidHom.twoRank_le_twoRank_add_of_card_ker_le_two_pow {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] [Module.Finite (ZMod 2) (TauCeti.ElementaryTwoQuotient G)] {n : ℕ} (f : G →* H) [Finite ↥f.ker] (hf : Function.Surjective ⇑f) (hn : Nat.card ↥f.ker ≤ 2 ^ n) : TauCeti.twoRank G ≤ TauCeti.twoRank H + n

A surjection with a small kernel barely drops the 2-rank. If f : G →* H is surjective with |ker f| ≤ 2 ^ n, then twoRank G ≤ twoRank H + n. Together with TauCeti.twoRank_le_twoRank_of_surjective this pins the 2-rank of the quotient to within n of the 2-rank of G. The rank-nullity theorem for the induced map G / G² → H / H² turns the bound on the kernel of f into a bound on the dimension of the kernel of that map.

theorem MonoidHom.twoRank_eq_twoRank_iff_ker_le_square {G : Type u_1} [CommGroup G] {H : Type u_2} [CommGroup H] [Module.Finite (ZMod 2) (TauCeti.ElementaryTwoQuotient G)] (f : G →* H) (hf : Function.Surjective ⇑f) : TauCeti.twoRank H = TauCeti.twoRank G ↔ f.ker ≤ Subgroup.square G

A surjection keeps the 2-rank exactly when its kernel consists of squares. For a surjective f : G →* H, the groups G and H have the same 2-rank if and only if every element of ker f is a square in G.