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.
• Subgroup.powerSubgroup_index_le: a subgroup of index m contains Gᵐ.
• 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.

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ⁿ.

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

The quotient homomorphism G → G ⧸ Gⁿ.

@[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.

@[simp]

theorem TauCeti.powerClassQuotient_pow_eq_one {G : Type u_1} [CommGroup G] (n : ℕ) (x : powerClassQuotient G n) : x ^ n = 1

n kills the power classes: every element of G ⧸ Gⁿ has nth power 1.

theorem Subgroup.powerSubgroup_index_le {G : Type u_1} [CommGroup G] (H : Subgroup G) : TauCeti.powerSubgroup G H.index ≤ H

A subgroup contains the powers to the exponent of its index: (G ⧸ H) has order [G : H], so g ^ [G : H] ∈ H for every g. When H has infinite index the exponent is 0 and the statement is trivial.

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ⁿ.

instance MonoidHom.isFiniteRelIndex_comap_range_powMonoidHom {G : Type u_3} {H : Type u_4} [CommGroup G] [CommGroup H] (f : G →* H) (n : ℕ) (Δ : Subgroup G) [(powMonoidHom n).range.IsFiniteRelIndex Δ] : (Subgroup.comap f (powMonoidHom n).range).IsFiniteRelIndex Δ

A subgroup Δ of G meeting Gⁿ in a subgroup of finite index also meets the preimage of Hⁿ under a homomorphism f : G →* H in a subgroup of finite index.

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.

@[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.