Module

PowerQuotientAction.lean

Nyll.ProCGroups.Abelian.PowerQuotientAction

3 declarations indexed from sourceView source ↗

Module documentation

Automorphism actions on quotients by powers

Multiplicative automorphisms preserve the subgroup of powers and induce automorphisms of the corresponding quotient, with explicit evaluation.

Imports1

Mathlib.GroupTheory.QuotientGroup.Basic

Imported by2

theorem

map_powerRange

L22 ↗

ProCGroups.Abelian.map_powerRange

Documentation

Multiplicative automorphisms preserve the subgroup of nth powers.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Abelian
variable {A : Type*} [CommGroup A]

Lean source · statement

theorem map_powerRange (n : ℕ) (e : MulAut A) :
    ((powMonoidHom (α := A) n).range).map e.toMonoidHom =
      (powMonoidHom (α := A) n).range

def

powerQuotientAction

L34 ↗

ProCGroups.Abelian.powerQuotientAction

Documentation

The action of automorphisms on the quotient by nth powers.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Abelian
variable {A : Type*} [CommGroup A]

Lean source · full declaration

def powerQuotientAction (n : ℕ) :
    MulAut A →* MulAut (A ⧸ (powMonoidHom (α := A) n).range) where
  toFun e := QuotientGroup.congr _ _ e (map_powerRange n e)
  map_one' := by
    apply MulEquiv.ext
    intro x
    obtain ⟨a, rfl⟩ := QuotientGroup.mk'_surjective (powMonoidHom (α := A) n).range x
    rfl
  map_mul' e f := by
    apply MulEquiv.ext
    intro x
    obtain ⟨a, rfl⟩ := QuotientGroup.mk'_surjective (powMonoidHom (α := A) n).range x
    rfl

theorem

powerQuotientAction_mk

L49 ↗

ProCGroups.Abelian.powerQuotientAction_mk

Documentation

The quotient automorphism evaluates by applying the original automorphism.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.Abelian
variable {A : Type*} [CommGroup A]

Lean source · statement

theorem powerQuotientAction_mk (n : ℕ) (e : MulAut A) (a : A) :
    powerQuotientAction n e (QuotientGroup.mk' (powMonoidHom (α := A) n).range a) =
      QuotientGroup.mk' (powMonoidHom (α := A) n).range (e a)

Module documentation

Automorphism actions on quotients by powers

Declarations

map_powerRange

powerQuotientAction

powerQuotientAction_mk