Module

FrattiniQuotient.lean

Nyll.ProCGroups.ProP.FrattiniQuotient

8 declarations indexed from sourceView source ↗

Module documentation

The power--commutator quotient

This file exposes the quotient by the closed subgroup generated by pth powers and commutators. The quotient is commutative and has exponent dividing p. These facts are the algebraic input for the pro-p Frattini quotient; no equality with the Frattini subgroup is assumed.

Imports1

Nyll.ProCGroups.ProP.FrattiniPowers

Imported by10

instance

(anonymous instance)

L28 ↗

Source context 4 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/

Lean source · statement

instance : (closedPowerCommutator p G).Normal

abbrev

powerCommutatorQuotient

L32 ↗

ClassFieldTower.ProP.powerCommutatorQuotient

Documentation

The quotient by the closed subgroup generated by pth powers and commutators.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

abbrev powerCommutatorQuotient

def

powerCommutatorQuotientMk

L36 ↗

ClassFieldTower.ProP.powerCommutatorQuotientMk

Documentation

The continuous quotient map to the power--commutator quotient.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

def powerCommutatorQuotientMk :
    G →ₜ* powerCommutatorQuotient p G

theorem

powerCommutatorQuotientMk_surjective

L42 ↗

ClassFieldTower.ProP.powerCommutatorQuotientMk_surjective

Documentation

The canonical map to the power--commutator quotient is surjective.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

theorem powerCommutatorQuotientMk_surjective :
    Function.Surjective (powerCommutatorQuotientMk p G)

theorem

ker_powerCommutatorQuotientMk

L47 ↗

ClassFieldTower.ProP.ker_powerCommutatorQuotientMk

Documentation

The kernel of the quotient map is the closed power--commutator subgroup.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

theorem ker_powerCommutatorQuotientMk :
    (powerCommutatorQuotientMk p G).ker = closedPowerCommutator p G

theorem

powerCommutatorQuotient_isMulCommutative

L52 ↗

ClassFieldTower.ProP.powerCommutatorQuotient_isMulCommutative

Documentation

The power--commutator quotient is commutative.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

theorem powerCommutatorQuotient_isMulCommutative :
    IsMulCommutative (powerCommutatorQuotient p G)

theorem

powerCommutatorQuotient_pow_eq_one

L58 ↗

ClassFieldTower.ProP.powerCommutatorQuotient_pow_eq_one

Documentation

Every element of the power--commutator quotient has pth power one.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

theorem powerCommutatorQuotient_pow_eq_one
    (x : powerCommutatorQuotient p G) : x ^ p = 1

theorem

powerCommutatorQuotient_mul_comm

L67 ↗

ClassFieldTower.ProP.powerCommutatorQuotient_mul_comm

Documentation

Multiplication in the power--commutator quotient is commutative.

Source context 5 commands

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

namespace ClassFieldTower.ProP
universe u
section
variable (p : ℕ) (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]

/- A single canonical local normality route supplies every quotient operation
in this file without exporting a competing global instance. -/
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G

Lean source · statement

theorem powerCommutatorQuotient_mul_comm
    (x y : powerCommutatorQuotient p G) : x * y = y * x

Module documentation

The power--commutator quotient

Declarations