NYLL
Module

H1PowerCommutator.lean

Nyll.ProCGroups.ProP.H1PowerCommutator
11 declarations indexed from sourceView source ↗

Module documentation

Factoring continuous degree-one classes through the elementary quotient

Every continuous ZMod p character factors uniquely through the closed power--commutator quotient. The resulting equivalence is linear and is kept separate from the later finite-dimensional duality argument.

Imports3
Imported by2

Declarations

instance

(anonymous instance)

L28 ↗
Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
Lean source · statement
instance : TopologicalSpace (ZMod p)
instance

(anonymous instance)

L29 ↗
Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance : DiscreteTopology (ZMod p)
instance

(anonymous instance)

L30 ↗
Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
Lean source · statement
instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
instance

(anonymous instance)

L32 ↗
Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
instance : (closedPowerCommutator p G).Normal
def

characterOnPowerCommutatorQuotient

L36 ↗
ClassFieldTower.ProP.characterOnPowerCommutatorQuotient
Documentation

Factor a character through the closed power--commutator quotient.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
def characterOnPowerCommutatorQuotient
    (f : G →ₜ* Multiplicative (ZMod p)) :
    powerCommutatorQuotient p G →ₜ* Multiplicative (ZMod p)
theorem

characterOnPowerCommutatorQuotient_mk

L42 ↗
ClassFieldTower.ProP.characterOnPowerCommutatorQuotient_mk
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
theorem characterOnPowerCommutatorQuotient_mk
    (f : G →ₜ* Multiplicative (ZMod p)) (g : G) :
    characterOnPowerCommutatorQuotient f (powerCommutatorQuotientMk p G g) = f g
def

characterFromPowerCommutatorQuotient

L48 ↗
ClassFieldTower.ProP.characterFromPowerCommutatorQuotient
Documentation

Pull a quotient character back along the quotient map.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
def characterFromPowerCommutatorQuotient
    (f : powerCommutatorQuotient p G →ₜ* Multiplicative (ZMod p)) :
    G →ₜ* Multiplicative (ZMod p)
def

h1OnPowerCommutatorQuotient

L54 ↗
ClassFieldTower.ProP.h1OnPowerCommutatorQuotient
Documentation

Factor a degree-one class through the closed power--commutator quotient.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
def h1OnPowerCommutatorQuotient
    (f : ContinuousH1ZMod (p := p) (G := G)) :
    ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G)
def

h1FromPowerCommutatorQuotient

L61 ↗
ClassFieldTower.ProP.h1FromPowerCommutatorQuotient
Documentation

Pull a quotient degree-one class back to the original group.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
def h1FromPowerCommutatorQuotient
    (f : ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G)) :
    ContinuousH1ZMod (p := p) (G := G)
def

h1PowerCommutatorQuotientLinearEquiv

L69 ↗
ClassFieldTower.ProP.h1PowerCommutatorQuotientLinearEquiv
Documentation

Continuous degree-one classes are unchanged after passing to the closed power--commutator quotient.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · full declaration
def h1PowerCommutatorQuotientLinearEquiv :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G) where
  toFun := h1OnPowerCommutatorQuotient
  invFun := h1FromPowerCommutatorQuotient
  left_inv f := by ext g; rfl
  right_inv f := by
    ext q
    obtain ⟨g, rfl⟩ := powerCommutatorQuotientMk_surjective p G q
    rfl
  map_add' f g := by
    ext q
    obtain ⟨x, rfl⟩ := powerCommutatorQuotientMk_surjective p G q
    rfl
  map_smul' c f := by
    ext q
    obtain ⟨x, rfl⟩ := powerCommutatorQuotientMk_surjective p G q
    let evG : ContinuousH1ZMod (p := p) (G := G) →+ ZMod p :=
      { toFun := fun h => h (Additive.ofMul x)
        map_zero' := rfl
        map_add' := fun _ _ => rfl }
    let evQ :
        ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G) →+ ZMod p :=
      { toFun := fun h => h (Additive.ofMul (powerCommutatorQuotientMk p G x))
        map_zero' := rfl
        map_add' := fun _ _ => rfl }
    exact (ZMod.map_smul evG c f).trans
      (ZMod.map_smul evQ c (h1OnPowerCommutatorQuotient f)).symm
def

characterPowerCommutatorQuotientEquiv

L99 ↗
ClassFieldTower.ProP.characterPowerCommutatorQuotientEquiv
Documentation

The multiplicative form of the same quotient universal property.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : TopologicalSpace (ZMod p) := ⊥
local instance : DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
local instance : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · full declaration
def characterPowerCommutatorQuotientEquiv :
    (G →ₜ* Multiplicative (ZMod p)) ≃
      (powerCommutatorQuotient p G →ₜ* Multiplicative (ZMod p)) where
  toFun := characterOnPowerCommutatorQuotient
  invFun := characterFromPowerCommutatorQuotient
  left_inv f := by
    ext g
    exact characterOnPowerCommutatorQuotient_mk f g
  right_inv f := by
    ext q
    obtain ⟨g, rfl⟩ := powerCommutatorQuotientMk_surjective p G q
    rfl

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.