NYLL
Module

DiscreteH2Representatives.lean

Nyll.GaloisCohomology.ProP.DiscreteH2Representatives
4 declarations indexed from sourceView source ↗

Module documentation

Discrete degree-two comparison on arbitrary representatives

The existing comparison is evaluated on every lifted homogeneous two-cocycle. The representative is its actual dehomogenization, with no cup-product or normalization restriction and no extra comparison assumption.

Imports9
Imported by2

Declarations

theorem

mapHomologyIso_homologyπ

L31 ↗
ClassFieldTower.Cohomology.mapHomologyIso_homologyπ
Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits TopRep
namespace ClassFieldTower.Cohomology
noncomputable section
Lean source · statement
theorem mapHomologyIso_homologyπ
    {C : Type*} [Category C] [HasZeroMorphisms C]
    (S : ShortComplex C) (F : C ⥤ AddCommGrpCat) [F.PreservesZeroMorphisms]
    [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] :
    (S.map F).homologyπ ≫ (S.mapHomologyIso F).hom =
      (S.mapCyclesIso F).hom ≫ F.map S.homologyπ
theorem

mapHomologyIso_homologyπ_inv_apply

L50 ↗
ClassFieldTower.Cohomology.mapHomologyIso_homologyπ_inv_apply
Source context 3 commands

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

open CategoryTheory CategoryTheory.Limits TopRep
namespace ClassFieldTower.Cohomology
noncomputable section
Lean source · statement
theorem mapHomologyIso_homologyπ_inv_apply
    {C : Type*} [Category C] [HasZeroMorphisms C]
    (S : ShortComplex C) (F : C ⥤ AddCommGrpCat) [F.PreservesZeroMorphisms]
    [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S]
    (z : F.obj S.cycles) :
    (S.mapHomologyIso F).inv (F.map S.homologyπ z) =
      (S.map F).homologyπ ((S.mapCyclesIso F).inv z)
def

dehomogenizedTwoCocycle

L69 ↗
ClassFieldTower.Cohomology.dehomogenizedTwoCocycle
Documentation

The ordinary two-cocycle obtained by dehomogenizing an actual lifted homogeneous two-cocycle.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits TopRep
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def dehomogenizedTwoCocycle (z : trivialZModPCocyclesLifted p Q 2) :
    groupCohomology.cocycles₂ (ordinaryTrivialZModPLifted (p := p) (Q := Q))
theorem

discreteContinuousH2AddEquiv_π

L82 ↗
ClassFieldTower.Cohomology.discreteContinuousH2AddEquiv_π
Documentation

The discrete comparison evaluates an arbitrary continuous class represented by a lifted homogeneous two-cocycle as its ordinary dehomogenized class.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits TopRep
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
theorem discreteContinuousH2AddEquiv_π
    (z₀ : trivialZModPCocyclesLifted p Q 2) :
    discreteContinuousH2AddEquiv
      (ContinuousCohomology.π (trivialZModPLifted p Q) 2 z₀) =
    groupCohomology.H2π (ordinaryTrivialZModPLifted (p := p) (Q := Q))
      (dehomogenizedTwoCocycle z₀)

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