The group of nth power classes G ⧸ Gⁿ

For a commutative group G the subgroup Gⁿ of nth powers is the range of powMonoidHom n, and this file names it together with the quotient G ⧸ Gⁿ and the class of an element. At n = 2 the subgroup is Mathlib's Subgroup.square G, by TauCeti.square_eq_range_powMonoidHom.

Main definitions

• TauCeti.powerSubgroup: the subgroup Gⁿ ≤ G, whose elements are characterised as the nth powers by TauCeti.mem_powerSubgroup_iff, and which is the range of powMonoidHom n by TauCeti.powerSubgroup_eq_range_powMonoidHom.
• TauCeti.powerClassQuotient, TauCeti.powerClassHom: the quotient G ⧸ Gⁿ and the map taking an element to its power class. It is surjective (TauCeti.powerClassHom_surjective) with kernel Gⁿ (TauCeti.ker_powerClassHom), so it presents G ⧸ Gⁿ as the quotient of G by the nth powers.
• TauCeti.powerClassMap: the map G ⧸ Gⁿ → H ⧸ Hⁿ induced by a homomorphism G →* H, which carries nth powers to nth powers. It is functorial (TauCeti.powerClassMap_id, TauCeti.powerClassMap_comp); for a field extension L/K and f the map Kˣ →* Lˣ it is the map of power classes along which Kummer theory is natural in the field.

def TauCeti.powerSubgroup (G : Type u_1) [CommGroup G] (n : ℕ) : Subgroup G

The subgroup of nth powers Gⁿ ≤ G.

Equations

• TauCeti.powerSubgroup G n = (powMonoidHom n).range

theorem TauCeti.powerSubgroup_eq_range_powMonoidHom (G : Type u_1) [CommGroup G] (n : ℕ) : powerSubgroup G n = (powMonoidHom n).range

The subgroup Gⁿ is the range of the nth power homomorphism.

@[reducible, inline]

abbrev TauCeti.powerClassQuotient (G : Type u_1) [CommGroup G] (n : ℕ) : Type u_1

The group of nth power classes G ⧸ Gⁿ.

Equations

• TauCeti.powerClassQuotient G n = (G ⧸ TauCeti.powerSubgroup G n)

def TauCeti.powerClassHom (G : Type u_1) [CommGroup G] (n : ℕ) : G →* powerClassQuotient G n

The quotient homomorphism G → G ⧸ Gⁿ.

Equations

• TauCeti.powerClassHom G n = QuotientGroup.mk' (TauCeti.powerSubgroup G n)

@[simp]

theorem TauCeti.ker_powerClassHom (G : Type u_1) [CommGroup G] (n : ℕ) : (powerClassHom G n).ker = powerSubgroup G n

The kernel of the power-class homomorphism is the subgroup Gⁿ of nth powers.

theorem TauCeti.powerClassHom_surjective (G : Type u_1) [CommGroup G] (n : ℕ) : Function.Surjective ⇑(powerClassHom G n)

Every power class is the class of an element: powerClassHom is surjective.

@[simp]

theorem TauCeti.powerClassHom_apply {G : Type u_1} [CommGroup G] (n : ℕ) (g : G) : (powerClassHom G n) g = ↑g

The power-class homomorphism sends g to its quotient class.

@[simp]

theorem TauCeti.mem_powerSubgroup_iff {G : Type u_1} [CommGroup G] (n : ℕ) {g : G} : g ∈ powerSubgroup G n ↔ ∃ (h : G), h ^ n = g

An element belongs to Gⁿ exactly when it is an nth power.

Functoriality

theorem TauCeti.powerSubgroup_le_comap {G : Type u_1} [CommGroup G] (n : ℕ) {H : Type u_2} [CommGroup H] (f : G →* H) : powerSubgroup G n ≤ Subgroup.comap f (powerSubgroup H n)

A homomorphism carries nth powers to nth powers: Gⁿ lies in the preimage of Hⁿ.

def TauCeti.powerClassMap {G : Type u_1} [CommGroup G] (n : ℕ) {H : Type u_2} [CommGroup H] (f : G →* H) : powerClassQuotient G n →* powerClassQuotient H n

The map of power classes G ⧸ Gⁿ → H ⧸ Hⁿ induced by a homomorphism f : G →* H, the class of g going to the class of f g.

Equations

• TauCeti.powerClassMap n f = QuotientGroup.map (TauCeti.powerSubgroup G n) (TauCeti.powerSubgroup H n) f ⋯

@[simp]

theorem TauCeti.powerClassMap_mk {G : Type u_1} [CommGroup G] (n : ℕ) {H : Type u_2} [CommGroup H] (f : G →* H) (g : G) : (powerClassMap n f) ↑g = ↑(f g)

powerClassMap sends the class of g to the class of f g.

theorem TauCeti.powerClassMap_comp_powerClassHom {G : Type u_1} [CommGroup G] (n : ℕ) {H : Type u_2} [CommGroup H] (f : G →* H) : (powerClassMap n f).comp (powerClassHom G n) = (powerClassHom H n).comp f

powerClassMap is the map of power classes compatible with powerClassHom: powerClassMap n f ∘ powerClassHom G n = powerClassHom H n ∘ f.

@[simp]

theorem TauCeti.powerClassMap_id {G : Type u_1} [CommGroup G] (n : ℕ) : powerClassMap n (MonoidHom.id G) = MonoidHom.id (powerClassQuotient G n)

The identity induces the identity on power classes.

theorem TauCeti.powerClassMap_comp {G : Type u_1} [CommGroup G] (n : ℕ) {H : Type u_2} [CommGroup H] {P : Type u_3} [CommGroup P] (f : G →* H) (f' : H →* P) : powerClassMap n (f'.comp f) = (powerClassMap n f').comp (powerClassMap n f)

The map of power classes of a composite is the composite of the maps of power classes.