Multiplicative square classes

This file relates the literal quotient Kˣ ⧸ (Kˣ)² to the additive square-class group used by the multiquadratic development. The multiplicative quotient is convenient for products and for cardinality formulas, while SquareClassGroup K carries the canonical ZMod 2-module structure. The comparison with ElementaryTwoQuotient Kˣ reuses the generic functorial quotient developed for commutative groups.

Both presentations are functorial in field homomorphisms. Their canonical equivalence identifies the class of a unit on the multiplicative side with squareClass on the additive side, so results may move between the two conventions without choosing representatives.

Main definitions and results

• TauCeti.MultiplicativeSquareClassGroup: the literal quotient Kˣ ⧸ (Kˣ)².
• TauCeti.multiplicativeSquareClassEquiv: its canonical multiplicative equivalence with Multiplicative (SquareClassGroup K).
• TauCeti.elementaryTwoQuotientEquivSquareClassGroup: the ZMod 2-linear comparison with the generic elementary-two quotient.
• TauCeti.natCard_multiplicativeSquareClassGroup: equality of the cardinalities of the two presentations.
• RingHom.multiplicativeSquareClassMap and RingHom.squareClassMap: pushforward of square classes along a field homomorphism, in the two conventions.

@[reducible, inline]

abbrev TauCeti.MultiplicativeSquareClassGroup (K : Type u_2) [Field K] : Type u_2

The multiplicative square-class group, as the literal quotient of the unit group by its subgroup of squares.

Equations

• TauCeti.MultiplicativeSquareClassGroup K = (Kˣ ⧸ Subgroup.square Kˣ)

theorem TauCeti.squareClassHom_surjective {K : Type u_1} [Field K] : Function.Surjective ⇑squareClassHom

Every square class has a unit representative.

noncomputable def TauCeti.multiplicativeSquareClassEquiv {K : Type u_1} [Field K] : MultiplicativeSquareClassGroup K ≃* Multiplicative (SquareClassGroup K)

The canonical equivalence from the literal multiplicative quotient of units by squares to the multiplicative form of the additive square-class group.

Equations

• TauCeti.multiplicativeSquareClassEquiv = QuotientGroup.liftEquiv (Subgroup.square Kˣ) ⋯ ⋯

@[simp]

theorem TauCeti.multiplicativeSquareClassEquiv_mk {K : Type u_1} [Field K] (u : Kˣ) : multiplicativeSquareClassEquiv ↑u = Multiplicative.ofAdd (squareClass u)

The canonical equivalence sends the class of a unit to its additive square class.

noncomputable def TauCeti.elementaryTwoQuotientEquivSquareClassGroup {K : Type u_1} [Field K] : ElementaryTwoQuotient Kˣ ≃ₗ[ZMod 2] SquareClassGroup K

The generic elementary-two quotient of the unit group is canonically ZMod 2-linearly equivalent to the square-class group.

Equations

• TauCeti.elementaryTwoQuotientEquivSquareClassGroup = LinearEquiv.ofBijective (AddMonoidHom.toZModLinearMap 2 (TauCeti.elementaryTwoQuotientEquivSquareQuotient Kˣ).toAddMonoidHom) ⋯

@[simp]

theorem TauCeti.elementaryTwoQuotientEquivSquareClassGroup_mk {K : Type u_1} [Field K] (u : Kˣ) : elementaryTwoQuotientEquivSquareClassGroup (elementaryTwoQuotientMk u) = squareClass u

The generic elementary-two class of a unit corresponds to its square class.

theorem TauCeti.finite_multiplicativeSquareClassGroup_iff {K : Type u_1} [Field K] : Finite (MultiplicativeSquareClassGroup K) ↔ Finite (SquareClassGroup K)

The multiplicative and additive presentations of the square-class group are finite simultaneously.

theorem TauCeti.natCard_multiplicativeSquareClassGroup {K : Type u_1} [Field K] : Nat.card (MultiplicativeSquareClassGroup K) = Nat.card (SquareClassGroup K)

The multiplicative and additive presentations of the square-class group have the same Nat.card.

def RingHom.multiplicativeSquareClassMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) : TauCeti.MultiplicativeSquareClassGroup K →* TauCeti.MultiplicativeSquareClassGroup L

Pushforward on multiplicative square classes along a field homomorphism.

Equations

• f.multiplicativeSquareClassMap = QuotientGroup.map (Subgroup.square Kˣ) (Subgroup.square Lˣ) (Units.map ↑f) ⋯

@[simp]

theorem RingHom.multiplicativeSquareClassMap_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) (u : Kˣ) : f.multiplicativeSquareClassMap ↑u = ↑((Units.map ↑f) u)

Pushforward sends the class of a unit to the class of its image.

@[simp]

theorem RingHom.multiplicativeSquareClassMap_id {K : Type u_1} [Field K] : (id K).multiplicativeSquareClassMap = MonoidHom.id (TauCeti.MultiplicativeSquareClassGroup K)

Pushforward on multiplicative square classes preserves identity field homomorphisms.

@[simp]

theorem RingHom.multiplicativeSquareClassMap_comp {K : Type u_1} {L : Type u_2} {F : Type u_3} [Field K] [Field L] [Field F] (g : L →+* F) (f : K →+* L) : (g.comp f).multiplicativeSquareClassMap = g.multiplicativeSquareClassMap.comp f.multiplicativeSquareClassMap

Pushforward on multiplicative square classes preserves composition of field homomorphisms.

noncomputable def RingHom.squareClassMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) : TauCeti.SquareClassGroup K →ₛₗ[id (ZMod 2)] TauCeti.SquareClassGroup L

Pushforward on the additive square-class groups along a field homomorphism, transported from the generic functorial map on elementary-two quotients.

Equations

• f.squareClassMap = ↑TauCeti.elementaryTwoQuotientEquivSquareClassGroup ∘ₗ TauCeti.elementaryTwoQuotientMap (Units.map ↑f) ∘ₗ ↑TauCeti.elementaryTwoQuotientEquivSquareClassGroup.symm

@[simp]

theorem RingHom.squareClassMap_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) (u : Kˣ) : f.squareClassMap (TauCeti.squareClass u) = TauCeti.squareClass ((Units.map ↑f) u)

Pushforward sends the additive square class of a unit to the class of its image.

@[simp]

theorem RingHom.multiplicativeSquareClassEquiv_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) (x : TauCeti.MultiplicativeSquareClassGroup K) : TauCeti.multiplicativeSquareClassEquiv (f.multiplicativeSquareClassMap x) = Multiplicative.ofAdd (f.squareClassMap (Multiplicative.toAdd (TauCeti.multiplicativeSquareClassEquiv x)))

The canonical equivalence between the two square-class conventions commutes with pushforward along a field homomorphism.

@[simp]

theorem RingHom.squareClassMap_id {K : Type u_1} [Field K] : (id K).squareClassMap = LinearMap.id

Pushforward on additive square classes preserves identity field homomorphisms.

@[simp]

theorem RingHom.squareClassMap_comp {K : Type u_1} {L : Type u_2} {F : Type u_3} [Field K] [Field L] [Field F] (g : L →+* F) (f : K →+* L) : (g.comp f).squareClassMap = g.squareClassMap ∘ₗ f.squareClassMap

Pushforward on additive square classes preserves composition of field homomorphisms.