NYLL
Module

H1GeneratorRank.lean

Nyll.ProCGroups.ProP.H1GeneratorRank
16 declarations indexed from sourceView source ↗

Module documentation

Generator rank as continuous H¹ dimension

This file identifies continuous trivial-coefficient degree-one classes with the linear dual of the power--commutator quotient. For a finitely generated pro-p group the quotient is finite, so continuity is automatic and P06 gives the generator-rank formula.

Imports3
Imported by1

Declarations

instance

(anonymous instance)

L29 ↗
Source context 5 commands

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

open scoped Topology IsMulCommutative
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)

L30 ↗
Source context 6 commands

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

open scoped Topology IsMulCommutative
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)

L31 ↗
Source context 7 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal
instance

(anonymous instance)

L33 ↗
Source context 8 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
Lean source · statement
instance : IsMulCommutative (powerCommutatorQuotient p G)
instance

(anonymous instance)

L35 ↗
Source context 9 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
Lean source · statement
instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G))
instance

(anonymous instance)

L39 ↗
Source context 10 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
Lean source · statement
instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

continuousPowerCommutatorDual

L43 ↗
ClassFieldTower.ProP.continuousPowerCommutatorDual
Documentation

The continuous part of the algebraic dual of the power--commutator quotient.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousPowerCommutatorDual :
    Submodule (ZMod p)
      (Module.Dual (ZMod p) (Additive (powerCommutatorQuotient p G))) where
  carrier := {f | Continuous f}
  zero_mem' := continuous_const
  add_mem' hf hg := hf.add hg
  smul_mem' c f hf := by
    change Continuous fun x => c * f x
    exact continuous_const.mul hf
def

quotientH1ToContinuousDual

L54 ↗
ClassFieldTower.ProP.quotientH1ToContinuousDual
Documentation

Turn a quotient degree-one class into its underlying continuous linear functional.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def quotientH1ToContinuousDual
    (f : ContinuousH1ZMod (p := p)
      (G := powerCommutatorQuotient p G)) :
    continuousPowerCommutatorDual (p := p) (G := G)
def

quotientH1OfContinuousDual

L61 ↗
ClassFieldTower.ProP.quotientH1OfContinuousDual
Documentation

Equip a continuous linear functional with its continuous additive-hom structure.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def quotientH1OfContinuousDual
    (f : continuousPowerCommutatorDual (p := p) (G := G)) :
    ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G) where
  toAddMonoidHom := f.1.toAddMonoidHom
  continuous_toFun := f.2
def

quotientH1ContinuousDualLinearEquiv

L68 ↗
ClassFieldTower.ProP.quotientH1ContinuousDualLinearEquiv
Documentation

Quotient degree-one classes are exactly the continuous linear dual.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def quotientH1ContinuousDualLinearEquiv :
    ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G) ≃ₗ[ZMod p]
      continuousPowerCommutatorDual (p := p) (G := G) where
  toFun := quotientH1ToContinuousDual
  invFun := quotientH1OfContinuousDual
  left_inv f := by ext x; rfl
  right_inv f := by ext x; rfl
  map_add' f g := by ext x; rfl
  map_smul' c f := by
    ext x
    let ev : ContinuousH1ZMod (p := p) (G := powerCommutatorQuotient p G) →+
        ZMod p :=
      { toFun := fun h => h x
        map_zero' := rfl
        map_add' := fun _ _ => rfl }
    exact ZMod.map_smul ev c f
def

continuousH1PowerCommutatorDualEquiv

L86 ↗
ClassFieldTower.ProP.continuousH1PowerCommutatorDualEquiv
Documentation

Continuous H¹ is the continuous dual of the elementary quotient.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1PowerCommutatorDualEquiv :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      continuousPowerCommutatorDual (p := p) (G := G)
theorem

continuousPowerCommutatorDual_eq_top

L92 ↗
ClassFieldTower.ProP.continuousPowerCommutatorDual_eq_top
Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousPowerCommutatorDual_eq_top
    [DiscreteTopology (powerCommutatorQuotient p G)] :
    continuousPowerCommutatorDual (p := p) (G := G) = ⊤
def

continuousH1PowerCommutatorFullDualLinearEquiv

L100 ↗
ClassFieldTower.ProP.continuousH1PowerCommutatorFullDualLinearEquiv
Documentation

For a discrete elementary quotient, continuous H¹ is the full algebraic dual.

Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1PowerCommutatorFullDualLinearEquiv
    [DiscreteTopology (powerCommutatorQuotient p G)] :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      Module.Dual (ZMod p) (Additive (powerCommutatorQuotient p G))
theorem

finrank_continuousH1_eq_finrank_powerCommutatorQuotient

L108 ↗
ClassFieldTower.ProP.finrank_continuousH1_eq_finrank_powerCommutatorQuotient
Source context 11 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finrank_continuousH1_eq_finrank_powerCommutatorQuotient
    [Fact p.Prime] [DiscreteTopology (powerCommutatorQuotient p G)] :
    Module.finrank (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) =
      Module.finrank (ZMod p) (Additive (powerCommutatorQuotient p G))
instance

(anonymous instance)

L120 ↗
Source context 13 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section Profinite
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [Fact p.Prime]
Lean source · statement
instance : IsClosed (closedPowerCommutator p G : Set G)
theorem

topologicalGeneratorRank_eq_finrank_continuousH1

L125 ↗
ClassFieldTower.ProP.topologicalGeneratorRank_eq_finrank_continuousH1
Documentation

For a finitely generated pro-p group, generator rank equals the dimension of continuous trivial-coefficient degree-one cohomology.

Source context 14 commands

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

open scoped Topology IsMulCommutative
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 : (closedPowerCommutator p G).Normal :=
  closedPowerCommutator_normal p G
local instance : IsMulCommutative (powerCommutatorQuotient p G) :=
  powerCommutatorQuotient_isMulCommutative p G
local instance : Module (ZMod p) (Additive (powerCommutatorQuotient p G)) :=
  AddCommGroup.zmodModule fun x => by
    change (Additive.toMul x) ^ p = 1
    exact powerCommutatorQuotient_pow_eq_one p G (Additive.toMul x)
local instance : Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
section Profinite
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
  [Fact p.Prime]
local instance : IsClosed (closedPowerCommutator p G : Set G) :=
  isClosed_closedPowerCommutator p G
Lean source · statement
theorem topologicalGeneratorRank_eq_finrank_continuousH1
    (hpG : ProCGroups.ProC.HasPGroupOpenNormalBasis p G)
    (hfg : ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated G) :
    topologicalGeneratorRank G =
      Module.finrank (ZMod p) (ContinuousH1ZMod (p := p) (G := G))

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