NYLL
Module

PresentationH2UpperBound.lean

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

Module documentation

The presentation upper bound for degree-two continuous cohomology

If the extracted kernel character vanishes, the normalized free-source primitive descends along the presentation quotient. Its homogeneous lift is a target primitive, proving injectivity into the invariant kernel character space and hence the displayed relation-cardinality bound.

Imports7
  • Nyll.GaloisCohomology.ProP.PresentationH2KernelCharacter
  • Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
  • Mathlib.RepresentationTheory.Continuous.Basic
  • Mathlib.RepresentationTheory.Continuous.TopRep
  • Mathlib.Topology.ContinuousMap.Algebra
  • Mathlib.Topology.ContinuousMap.Basic
  • Mathlib.Topology.ContinuousMap.Defs
Imported by2

Declarations

instance

presentationUpperContinuousH1Module

L43 ↗
ClassFieldTower.ProP.presentationUpperContinuousH1Module
Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H))
def

presentationNormalizedPrimitiveContinuousMap

L51 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationNormalizedPrimitiveContinuousMap
Documentation

The normalized primitive as a continuous map on the free source.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · full declaration
def presentationNormalizedPrimitiveContinuousMap
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    C(sourceData.carrier, ZMod p) where
  toFun := presentationNormalizedPrimitiveValue P x
  continuous_toFun :=
    ((ContinuousLinearEquiv.ulift :
      ULift.{u} (ZMod p) ≃L[ZMod p] ZMod p).continuous).comp <|
      (((presentationPrimitive P x).1 1).continuous).sub continuous_const
theorem

presentationNormalizedPrimitive_factors

L61 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationNormalizedPrimitive_factors
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationNormalizedPrimitive_factors
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0) :
    Function.FactorsThrough (presentationNormalizedPrimitiveContinuousMap P x) P.quotient
def

presentationDescendedNormalizedPrimitive

L88 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedNormalizedPrimitive
Documentation

Descend a normalized primitive whose kernel character vanishes to the presentation target.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
def presentationDescendedNormalizedPrimitive
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0) : C(G, ZMod p)
theorem

presentationDescendedNormalizedPrimitive_comp

L102 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedNormalizedPrimitive_comp
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationDescendedNormalizedPrimitive_comp
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0)
    (f : sourceData.carrier) :
    presentationDescendedNormalizedPrimitive P x hx (P.quotient f) =
      presentationNormalizedPrimitiveValue P x f
def

presentationDescendedPrimitive

L121 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedPrimitive
Documentation

The homogeneous target primitive reconstructed from the descended normalized value.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
def presentationDescendedPrimitive
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0) :
    (Cohomology.trivialZModPCochainsLifted p G).X 1
theorem

presentationDescendedPrimitive_apply

L147 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedPrimitive_apply
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationDescendedPrimitive_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0)
    (g h : G) :
    (presentationDescendedPrimitive P x hx).1 g h =
      ULift.up ((presentationPrimitive P x).1 1 1).down +
        ULift.up (presentationDescendedNormalizedPrimitive P x hx (g⁻¹ * h))
theorem

presentationDescendedPrimitive_pullback_apply

L157 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedPrimitive_pullback_apply
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationDescendedPrimitive_pullback_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0)
    (f g : sourceData.carrier) :
    (presentationDescendedPrimitive P x hx).1 (P.quotient f) (P.quotient g) =
      (presentationPrimitive P x).1 f g
theorem

presentationDescendedPrimitive_boundary

L193 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationDescendedPrimitive_boundary
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationDescendedPrimitive_boundary
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0) :
    ((Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom
        (presentationDescendedPrimitive P x hx) =
      ((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom
        (targetCocycleSection x)
theorem

eq_zero_of_presentationH2ToInvariantKernelH1_eq_zero

L221 ↗
ClassFieldTower.ProP.PresentationH2Aux.eq_zero_of_presentationH2ToInvariantKernelH1_eq_zero
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem eq_zero_of_presentationH2ToInvariantKernelH1_eq_zero
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (hx : presentationH2ToInvariantKernelH1 P x = 0) : x = 0
theorem

presentationH2ToInvariantKernelH1_injective

L248 ↗
ClassFieldTower.ProP.presentationH2ToInvariantKernelH1_injective
Documentation

The presentation kernel character remembers every degree-two target class.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem presentationH2ToInvariantKernelH1_injective
    (P : FiniteProPPresentation p d r sourceData G) :
    Function.Injective (presentationH2ToInvariantKernelH1 P)
theorem

presentationH2_finiteDimensional

L258 ↗
ClassFieldTower.ProP.presentationH2_finiteDimensional
Documentation

Degree-two continuous cohomology is finite-dimensional for a finite presentation target.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem presentationH2_finiteDimensional
    (P : FiniteProPPresentation p d r sourceData G) :
    FiniteDimensional (ZMod p)
      (Cohomology.continuousCohomologyZModPLifted p G 2)
theorem

finrank_continuousCohomologyZModPLifted_degree_two_le_relationCard

L268 ↗
ClassFieldTower.ProP.finrank_continuousCohomologyZModPLifted_degree_two_le_relationCard
Documentation

The degree-two mod-p cohomology rank is at most the displayed relation count.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open ProCGroups
open PresentationH2Aux
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]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
local instance presentationUpperContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finrank_continuousCohomologyZModPLifted_degree_two_le_relationCard
    (P : FiniteProPPresentation p d r sourceData G) :
    Module.finrank (ZMod p)
        (Cohomology.continuousCohomologyZModPLifted p G 2) ≤ r

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