Documentation

TauCeti.Algebra.Group.ElementaryTwoQuotient.Prod

The maximal elementary-2 quotient distributes over products #

The maximal elementary-2 quotient G / G² of TauCeti.Algebra.Group.ElementaryTwoQuotient.Basic sends a product of commutative groups to the product of the quotients, ZMod 2-linearly: (G × H)/(G × H)² is G/G² × H/H², and the same holds for an arbitrary indexed product. Reading ZMod 2-dimensions over a finite index, the 2-rank is additive:

TauCeti.twoRank (G × H) = TauCeti.twoRank G + TauCeti.twoRank H

and TauCeti.twoRank (∀ i, G i) = ∑ i, TauCeti.twoRank (G i).

Both structural equivalences are transported from Mathlib's product-quotient API for quotients by the range of the doubling map (QuotientAddGroup.prodAddEquiv and QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom) through the identification of the ModN model of G/G² with the quotient by the range of doubling, rather than rebuilt by hand.

This is the structural tool behind computing a class group's 2-rank from a decomposition: a finite abelian group is a product of cyclic groups, and its 2-rank is the number of even-order factors. This product additivity supports the Layer 2 class-group quotient API and the later Layer 3 genus-field/2-rank theorem in the multiquadratic roadmap. For instance the class group (ℤ/2)² of ℚ(√-21) has 2-rank 1 + 1 = 2, matching the t - 1 = 3 - 1 count of ramified primes in the worked examples.

Main results #

source
noncomputable def TauCeti.elementaryTwoQuotientProdLinearEquiv (G : Type u_3) (H : Type u_4) [CommGroup G] [CommGroup H] :
ElementaryTwoQuotient (G × H) ≃ₗ[ZMod 2] ElementaryTwoQuotient G × ElementaryTwoQuotient H

The elementary-2 quotient of a product is the product of the elementary-2 quotients. For commutative groups G and H, the class map identifies (G × H)/(G × H)² with G/G² × H/H² ZMod 2-linearly. It is transported from Mathlib's QuotientAddGroup.prodAddEquiv through the identification of the ModN model of the quotient with the quotient by the doubling range.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.elementaryTwoQuotientProdLinearEquiv_mk (G : Type u_3) (H : Type u_4) [CommGroup G] [CommGroup H] (p : G × H) :
    (elementaryTwoQuotientProdLinearEquiv G H) (elementaryTwoQuotientMk p) = (elementaryTwoQuotientMk p.1, elementaryTwoQuotientMk p.2)

    The product equivalence sends the class of (a, b) to the pair of classes.

    source
    @[simp]
    theorem TauCeti.elementaryTwoQuotientProdLinearEquiv_symm_mk (G : Type u_3) (H : Type u_4) [CommGroup G] [CommGroup H] (a : G) (b : H) :
    (elementaryTwoQuotientProdLinearEquiv G H).symm (elementaryTwoQuotientMk a, elementaryTwoQuotientMk b) = elementaryTwoQuotientMk (a, b)

    The inverse product equivalence sends a pair of classes to the class of the pair.

    source
    theorem TauCeti.twoRank_prod (G : Type u_3) (H : Type u_4) [CommGroup G] [CommGroup H] [Module.Finite (ZMod 2) (ElementaryTwoQuotient G)] [Module.Finite (ZMod 2) (ElementaryTwoQuotient H)] :
    twoRank (G × H) = twoRank G + twoRank H

    The 2-rank is additive over products. For commutative groups whose elementary-2 quotients are finite-dimensional, twoRank (G × H) = twoRank G + twoRank H.

    source
    theorem TauCeti.card_elementaryTwoQuotient_prod (G : Type u_3) (H : Type u_4) [CommGroup G] [CommGroup H] :
    Nat.card (ElementaryTwoQuotient (G × H)) = Nat.card (ElementaryTwoQuotient G) * Nat.card (ElementaryTwoQuotient H)

    The cardinality reading of TauCeti.elementaryTwoQuotientProdLinearEquiv: |(G × H)/(G × H)²| = |G/G²| · |H/H²|.

    source
    noncomputable def TauCeti.elementaryTwoQuotientPiLinearEquiv {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → CommGroup (G i)] :
    ElementaryTwoQuotient ((i : ι) → G i) ≃ₗ[ZMod 2] (i : ι) → ElementaryTwoQuotient (G i)

    The elementary-2 quotient of an indexed product is the product of the elementary-2 quotients. For a family of commutative groups G i over an arbitrary index, the class map identifies (∀ i, G i)/(…)² with ∀ i, (G i)/(G i)² ZMod 2-linearly. It is transported from Mathlib's QuotientAddGroup.addEquivPiModRangeNSMulAddMonoidHom through the identification of the ModN model of the quotient with the quotient by the doubling range.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.elementaryTwoQuotientPiLinearEquiv_mk {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → CommGroup (G i)] (g : (i : ι) → G i) :
      (elementaryTwoQuotientPiLinearEquiv G) (elementaryTwoQuotientMk g) = fun (i : ι) => elementaryTwoQuotientMk (g i)

      The indexed-product equivalence sends the class of g to the family of componentwise classes.

      source
      @[simp]
      theorem TauCeti.elementaryTwoQuotientPiLinearEquiv_symm_mk {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → CommGroup (G i)] (g : (i : ι) → G i) :
      ((elementaryTwoQuotientPiLinearEquiv G).symm fun (i : ι) => elementaryTwoQuotientMk (g i)) = elementaryTwoQuotientMk g

      The inverse indexed-product equivalence sends a family of componentwise classes to the class of the assembled family.

      source
      theorem TauCeti.twoRank_pi {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → CommGroup (G i)] [Fintype ι] [∀ (i : ι), Module.Finite (ZMod 2) (ElementaryTwoQuotient (G i))] :
      twoRank ((i : ι) → G i) = ∑ i : ι, twoRank (G i)

      The 2-rank is additive over finite indexed products. For a finite family of commutative groups whose elementary-2 quotients are finite-dimensional, twoRank (∀ i, G i) = ∑ i, twoRank (G i).

      source
      theorem TauCeti.card_elementaryTwoQuotient_pi {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → CommGroup (G i)] [Fintype ι] :
      Nat.card (ElementaryTwoQuotient ((i : ι) → G i)) = ∏ i : ι, Nat.card (ElementaryTwoQuotient (G i))

      The cardinality reading of TauCeti.elementaryTwoQuotientPiLinearEquiv: |(∀ i, G i)/(…)²| = ∏ i, |(G i)/(G i)²|.