NYLL
Module

PresentationH2LowerBound.lean

Nyll.GaloisCohomology.ProP.PresentationH2LowerBound
5 declarations indexed from sourceView source ↗

Module documentation

Relation rank as a lower bound for presentation target H²

For a minimal pro-p presentation realizing the least relation count, normalized invariant kernel characters descend to a common finite stage. Their inflated transgression classes are linearly independent: a vanishing combination extends continuously to the free source, where minimality forces its restriction to the presentation kernel to vanish. The presentation quotient equivalence then transports the resulting dimension bound to the target group.

Imports8
Imported by2

Declarations

instance

presentationH2LowerCanonicalZModAddCommGroup

L39 ↗
ClassFieldTower.ProP.presentationH2LowerCanonicalZModAddCommGroup
Source context 7 commands

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

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

lowerBoundStageTargetTopology

L44 ↗
ClassFieldTower.ProP.lowerBoundStageTargetTopology
Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2LowerCanonicalZModAddCommGroup : 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 lowerBoundStageTargetTopology
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
instance

lowerBoundStageTargetDiscrete

L50 ↗
ClassFieldTower.ProP.lowerBoundStageTargetDiscrete
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2LowerCanonicalZModAddCommGroup : 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 lowerBoundStageTargetTopology
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
Lean source · statement
instance lowerBoundStageTargetDiscrete
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
theorem

presentation_relationCard_succ_le_finrank_h2

L59 ↗
ClassFieldTower.ProP.presentation_relationCard_succ_le_finrank_h2
Documentation

A nonempty relation family realizing the least relation count gives independent target H² classes.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2LowerCanonicalZModAddCommGroup : 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 lowerBoundStageTargetTopology
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance lowerBoundStageTargetDiscrete
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem presentation_relationCard_succ_le_finrank_h2
    {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)
    [FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p G 2)] :
    n + 1 ≤ Module.finrank (ZMod p)
      (continuousCohomologyZModPLifted p G 2)
theorem

presentation_relationCard_le_finrank_h2

L195 ↗
ClassFieldTower.ProP.presentation_relationCard_le_finrank_h2
Documentation

A finite minimal presentation realizing the least relation count supplies that many linearly independent degree-two continuous cohomology classes.

Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2LowerCanonicalZModAddCommGroup : 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 lowerBoundStageTargetTopology
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance lowerBoundStageTargetDiscrete
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem presentation_relationCard_le_finrank_h2
    {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)
    [FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p G 2)] :
    r ≤ Module.finrank (ZMod p)
      (continuousCohomologyZModPLifted p G 2)

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