Module

RelationRankH1.lean

Nyll.GaloisCohomology.ProP.RelationRankH1

4 declarations indexed from sourceView source ↗

Module documentation

Relation rank and invariant kernel H1

For a finite minimal pro-p presentation realizing the least relation count, relative Nakayama characters separate each displayed relator from the closed normal closure of the others. After normalization, their invariant degree-one classes map to the coordinate basis. Consequently, relator evaluation is surjective and the invariant kernel H1 dimension equals the displayed relation count.

Imports3

Imported by2

theorem

exists_invariantKernelH1_relatorEval_eq_single_of_relationCard_minimal

L37 ↗

ClassFieldTower.ProP.exists_invariantKernelH1_relatorEval_eq_single_of_relationCard_minimal

Documentation

Every coordinate vector is the relator evaluation of an invariant kernel class when the displayed relation count is minimal.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem exists_invariantKernelH1_relatorEval_eq_single_of_relationCard_minimal
    {d n : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (hG : HasFiniteMinimalPresentation p G)
    (P : FiniteProPPresentation p d (n + 1) sourceData G)
    (hP : P.IsMinimal)
    (hcard : minimalRelationRank p G hG = n + 1)
    (i : Fin (n + 1)) :
    ∃ eta : InvariantKernelH1 P,
      invariantKernelH1RelatorEval P eta = Pi.single i 1

theorem

invariantKernelH1RelatorEval_surjective_of_relationCard_minimal

L134 ↗

ClassFieldTower.ProP.invariantKernelH1RelatorEval_surjective_of_relationCard_minimal

Documentation

Relator evaluation is onto for a nonempty finite minimal presentation realizing the least relation count.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem invariantKernelH1RelatorEval_surjective_of_relationCard_minimal
    {d n : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (hG : HasFiniteMinimalPresentation p G)
    (P : FiniteProPPresentation p d (n + 1) sourceData G)
    (hP : P.IsMinimal)
    (hcard : minimalRelationRank p G hG = n + 1) :
    Function.Surjective (invariantKernelH1RelatorEval P)

theorem

relationCard_le_finrank_invariantKernelH1_of_minimal

L163 ↗

ClassFieldTower.ProP.relationCard_le_finrank_invariantKernelH1_of_minimal

Documentation

The displayed relation count is at most the dimension of invariant kernel H1 when the presentation realizes the least relation count.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem relationCard_le_finrank_invariantKernelH1_of_minimal
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (hG : HasFiniteMinimalPresentation p G)
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal)
    (hcard : minimalRelationRank p G hG = r) :
    r ≤ Module.finrank (ZMod p) (InvariantKernelH1 P)

theorem

finrank_invariantKernelH1_eq_relationCard_of_minimal

L185 ↗

ClassFieldTower.ProP.finrank_invariantKernelH1_eq_relationCard_of_minimal

Documentation

For a finite minimal presentation realizing the least relation count, the invariant kernel H1 dimension is exactly the number of displayed relators.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem finrank_invariantKernelH1_eq_relationCard_of_minimal
    {d r : ℕ}
    {sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p)}
    (hG : HasFiniteMinimalPresentation p G)
    (P : FiniteProPPresentation p d r sourceData G)
    (hP : P.IsMinimal)
    (hcard : minimalRelationRank p G hG = r) :
    Module.finrank (ZMod p) (InvariantKernelH1 P) = r

Module documentation

Relation rank and invariant kernel H1

Declarations

exists_invariantKernelH1_relatorEval_eq_single_of_relationCard_minimal

invariantKernelH1RelatorEval_surjective_of_relationCard_minimal

relationCard_le_finrank_invariantKernelH1_of_minimal

finrank_invariantKernelH1_eq_relationCard_of_minimal