NYLL
Module

InvariantKernelH1.lean

Nyll.GaloisCohomology.ProP.InvariantKernelH1
13 declarations indexed from sourceView source ↗

Module documentation

Invariant continuous characters of a presentation kernel

This file packages the conjugation-invariant continuous ZMod p characters of the kernel of a finite pro-p presentation as a ZMod p-submodule. Evaluation on the displayed relators is injective, so this invariant character space is finite-dimensional of rank at most the displayed relation count.

Imports9
Imported by3

Declarations

instance

invariantKernelCanonicalZModAddCommGroup

L38 ↗
ClassFieldTower.ProP.invariantKernelCanonicalZModAddCommGroup
Source context 6 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

continuousH1ZModModuleInstance

L43 ↗
ClassFieldTower.ProP.continuousH1ZModModuleInstance
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
theorem

kernel_le_character_ker

L50 ↗
ClassFieldTower.ProP.FiniteProPPresentation.kernel_le_character_ker
Documentation

Minimality makes every continuous mod-p character of the free source vanish on the presentation kernel.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem FiniteProPPresentation.kernel_le_character_ker
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal)
    (chi : sourceData.carrier →ₜ* Multiplicative (ZMod p)) :
    P.quotient.toMonoidHom.ker ≤ chi.toMonoidHom.ker
theorem

kernel_h1_eq_zero

L62 ↗
ClassFieldTower.ProP.FiniteProPPresentation.kernel_h1_eq_zero
Documentation

Additively, every continuous degree-one class of the free source vanishes on the kernel of a minimal presentation.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem FiniteProPPresentation.kernel_h1_eq_zero
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) (hP : P.IsMinimal)
    (chi : ContinuousH1ZMod (p := p) (G := sourceData.carrier))
    (n : P.quotient.toMonoidHom.ker) :
    chi (Additive.ofMul n) = 0
def

InvariantKernelCharacter

L75 ↗
ClassFieldTower.ProP.InvariantKernelCharacter
Documentation

Continuous kernel characters fixed by conjugation from the free source.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def InvariantKernelCharacter
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G)
def

invariantKernelCharacterRelatorEval

L86 ↗
ClassFieldTower.ProP.invariantKernelCharacterRelatorEval
Documentation

Evaluate an invariant kernel character on the displayed relators.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def invariantKernelCharacterRelatorEval
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G)
    (chi : InvariantKernelCharacter P) : Fin r → Multiplicative (ZMod p)
theorem

invariantKernelCharacterRelatorEval_injective

L96 ↗
ClassFieldTower.ProP.invariantKernelCharacterRelatorEval_injective
Documentation

The displayed relators determine every invariant continuous kernel character.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem invariantKernelCharacterRelatorEval_injective
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    Function.Injective (invariantKernelCharacterRelatorEval P)
def

InvariantKernelH1

L141 ↗
ClassFieldTower.ProP.InvariantKernelH1
Documentation

Conjugation-invariant additive degree-one classes on the presentation kernel.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def InvariantKernelH1
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    Submodule (ZMod p)
      (ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker)) where
  carrier := {chi | ∀ (f : sourceData.carrier) (n : P.quotient.toMonoidHom.ker),
    chi (Additive.ofMul (MulAut.conjNormal f n)) = chi (Additive.ofMul n)}
  zero_mem' := by
    change ∀ (f : sourceData.carrier) (n : P.quotient.toMonoidHom.ker),
      (0 : ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker))
          (Additive.ofMul (MulAut.conjNormal f n)) =
        (0 : ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker))
          (Additive.ofMul n)
    intros
    rfl
  add_mem' := by
    intro chi psi hchi hpsi f n
    change chi _ + psi _ = chi _ + psi _
    rw [hchi f n, hpsi f n]
  smul_mem' := by
    intro c chi hchi f n
    let evConj :
        ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker) →+ ZMod p :=
      { toFun := fun eta ↦ eta (Additive.ofMul (MulAut.conjNormal f n))
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    let ev : ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker) →+ ZMod p :=
      { toFun := fun eta ↦ eta (Additive.ofMul n)
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    exact (ZMod.map_smul evConj c chi).trans
      ((congrArg (fun z : ZMod p ↦ c • z) (hchi f n)).trans
        (ZMod.map_smul ev c chi).symm)
def

invariantKernelH1CharacterEquiv

L180 ↗
ClassFieldTower.ProP.invariantKernelH1CharacterEquiv
Documentation

Additive invariant classes and multiplicative invariant characters are canonically equivalent.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def invariantKernelH1CharacterEquiv
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    InvariantKernelH1 P ≃ InvariantKernelCharacter P where
  toFun chi :=
    ⟨characterOfH1 chi.1, fun f n ↦ congrArg Multiplicative.ofAdd (chi.2 f n)⟩
  invFun chi :=
    ⟨h1OfCharacter chi.1, fun f n ↦ congrArg Multiplicative.toAdd (chi.2 f n)⟩
  left_inv chi := by
    apply Subtype.ext
    ext n
    rfl
  right_inv chi := by
    apply Subtype.ext
    ext n
    rfl
def

invariantKernelH1RelatorEval

L201 ↗
ClassFieldTower.ProP.invariantKernelH1RelatorEval
Documentation

Linear evaluation of invariant degree-one classes on the displayed relators.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def invariantKernelH1RelatorEval
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    InvariantKernelH1 P →ₗ[ZMod p] (Fin r → ZMod p) where
  toFun chi i := chi.1 (Additive.ofMul ⟨P.relator i, P.relator_mem_kernel i⟩)
  map_add' _ _ := rfl
  map_smul' c chi := by
    funext i
    let ev : ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker) →+ ZMod p :=
      { toFun := fun eta ↦ eta (Additive.ofMul ⟨P.relator i, P.relator_mem_kernel i⟩)
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    exact ZMod.map_smul ev c chi.1
theorem

invariantKernelH1RelatorEval_injective

L219 ↗
ClassFieldTower.ProP.invariantKernelH1RelatorEval_injective
Documentation

Linear evaluation on the displayed relators is injective.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem invariantKernelH1RelatorEval_injective
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    Function.Injective (invariantKernelH1RelatorEval P)
theorem

invariantKernelH1_finiteDimensional

L233 ↗
ClassFieldTower.ProP.invariantKernelH1_finiteDimensional
Documentation

Invariant kernel classes are finite-dimensional for every finite displayed presentation.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem invariantKernelH1_finiteDimensional
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    FiniteDimensional (ZMod p) (InvariantKernelH1 P)
theorem

finrank_invariantKernelH1_le_relationCard

L244 ↗
ClassFieldTower.ProP.finrank_invariantKernelH1_le_relationCard
Documentation

The displayed relation count bounds the dimension of invariant kernel classes.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance invariantKernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousH1ZModModuleInstance
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finrank_invariantKernelH1_le_relationCard
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (P : FiniteProPPresentation p d r sourceData G) :
    Module.finrank (ZMod p) (InvariantKernelH1 P) ≤ r

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