Power classes as reduction modulo n

For a commutative group G, written additively, the integer multiples n • G are the additive form of the nth powers Gⁿ. Hence the reduction QuotSMulTop n (Additive G) of G modulo n is the group G ⧸ Gⁿ of nth power classes, written additively.

Main results

• TauCeti.zsmulTop_toAddSubgroup_eq_powerSubgroup: n • G is the additive form of Gⁿ.
• TauCeti.quotSMulTopPowerClassEquiv: the additive equivalence between reduction modulo n and the group of nth power classes. It is natural in G (TauCeti.quotSMulTopPowerClassEquiv_map).

theorem TauCeti.zsmulTop_toAddSubgroup_eq_powerSubgroup {G : Type u_1} [CommGroup G] (n : ℕ) : (↑n • ⊤).toAddSubgroup = Subgroup.toAddSubgroup (powerSubgroup G n)

In the additive group of a commutative group, the subgroup of integer multiples by n is the additive form of the subgroup of nth powers.

noncomputable def TauCeti.quotSMulTopPowerClassEquiv {G : Type u_1} [CommGroup G] (n : ℕ) : QuotSMulTop (↑n) (Additive G) ≃+ Additive (powerClassQuotient G n)

Reduction modulo n of a commutative group, written additively, is its group of nth power classes.

@[simp]

theorem TauCeti.quotSMulTopPowerClassEquiv_mk {G : Type u_1} [CommGroup G] (n : ℕ) (x : Additive G) : (quotSMulTopPowerClassEquiv n) (Submodule.Quotient.mk x) = Additive.ofMul ((powerClassHom G n) (Additive.toMul x))

The reduction/power-class equivalence sends the class of x to its power class.

theorem TauCeti.quotSMulTopPowerClassEquiv_map {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (n : ℕ) (f : G →* H) (x : QuotSMulTop (↑n) (Additive G)) : (quotSMulTopPowerClassEquiv n) (((QuotSMulTop.map ↑n) (MonoidHom.toAdditive f).toIntLinearMap) x) = (MonoidHom.toAdditive (powerClassMap n f)) ((quotSMulTopPowerClassEquiv n) x)

The reduction/power-class equivalence is natural: it intertwines the reduction modulo n of a homomorphism f with the map powerClassMap n f of power classes.