ZMod p classesFor the trivial action, continuous degree-one cohomology is represented by continuous additive characters into the discrete group ZMod p. This file also proves that every such character kills the closed power--commutator subgroup. No general cohomology package is imported: that dependency is much larger than the degree-one statement needed by the tower argument.
Continuous degree-one classes for the trivial ZMod p action.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]abbrev ContinuousH1ZModThe canonical ZMod p-module structure on continuous degree-one classes.
It is deliberately a named definition rather than a global data instance; downstream files activate it once per section.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]def continuousH1ZModModule :
Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))Reinterpret an additive degree-one class as a multiplicative character.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
continuousH1ZModModuledef characterOfH1 (f : ContinuousH1ZMod (p := p) (G := G)) :
G →ₜ* Multiplicative (ZMod p) where
toFun g := Multiplicative.ofAdd (f (Additive.ofMul g))
map_one' := f.map_zero
map_mul' g h := f.map_add (Additive.ofMul g) (Additive.ofMul h)
continuous_toFun := f.continuous_toFunReinterpret a multiplicative ZMod p character as an additive degree-one class.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
continuousH1ZModModuledef h1OfCharacter (f : G →ₜ* Multiplicative (ZMod p)) :
ContinuousH1ZMod (p := p) (G := G) where
toFun g := Multiplicative.toAdd (f (Additive.toMul g))
map_zero' := f.map_one
map_add' g h := f.map_mul (Additive.toMul g) (Additive.toMul h)
continuous_toFun := f.continuous_toFunAdditive degree-one classes and multiplicative characters are equivalent.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
continuousH1ZModModuledef h1CharacterEquiv :
ContinuousH1ZMod (p := p) (G := G) ≃ (G →ₜ* Multiplicative (ZMod p)) where
toFun := characterOfH1
invFun := h1OfCharacter
left_inv f := by ext g; rfl
right_inv f := by ext g; rflA continuous ZMod p character kills both p-th powers and commutators, and hence their closed generated subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology commutatorElement
namespace ClassFieldTower.ProP
universe u
variable {p : ℕ} {G : Type u}
variable [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
continuousH1ZModModuletheorem closedPowerCommutator_le_character_ker
(f : G →ₜ* Multiplicative (ZMod p)) :
closedPowerCommutator p G ≤ f.toMonoidHom.ker