Module

DiscreteH2Comparison.lean

Nyll.GaloisCohomology.ProP.DiscreteH2Comparison

11 declarations indexed from sourceView source ↗

Module documentation

Continuous and ordinary degree-two cohomology of a discrete group

For a discrete group in the base universe, the explicit homogeneous and inhomogeneous comparison induces an additive equivalence in degree two. The ordinary coefficient object is exactly the trivial Int-representation on ULift (ZMod p) used by finite Kummer coefficient change.

Imports3

Nyll.GaloisCohomology.ProP.ContinuousH1CupProduct
Nyll.GaloisCohomology.ProP.DiscreteH2ShortComplexComparison
Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Imported by5

def

discreteH2MappedShortComplexIso

L33 ↗

ClassFieldTower.Cohomology.discreteH2MappedShortComplexIso

Documentation

The comparison short-complex isomorphism, with the canonical sc 2 ≅ sc' 1 2 3 identification included.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def discreteH2MappedShortComplexIso :
    ((trivialZModPCochainsLifted p Q).sc 2).map
        (continuousCochainsToAddCommGrp p) ≅
      (groupCohomology.shortComplexH2
          (ordinaryTrivialZModPLifted (p := p) (Q := Q))).map
        ordinaryCochainsToAddCommGrp

def

discreteContinuousH2AddCommGrpIso

L46 ↗

ClassFieldTower.Cohomology.discreteContinuousH2AddCommGrpIso

Documentation

The canonical additive-group isomorphism from lifted continuous degree-two cohomology to ordinary degree-two group cohomology.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def discreteContinuousH2AddCommGrpIso :
    (continuousCochainsToAddCommGrp p).obj
        (continuousCohomologyZModPLifted p Q 2) ≅
      ordinaryCochainsToAddCommGrp.obj
        (groupCohomology
          (ordinaryTrivialZModPLifted (p := p) (Q := Q)) 2)

def

discreteContinuousH2AddEquiv

L72 ↗

ClassFieldTower.Cohomology.discreteContinuousH2AddEquiv

Documentation

Continuous homogeneous and ordinary inhomogeneous degree-two cohomology are additively equivalent for a discrete group.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def discreteContinuousH2AddEquiv :
    continuousCohomologyZModPLifted p Q 2 ≃+
      groupCohomology
        (ordinaryTrivialZModPLifted (p := p) (Q := Q)) 2

def

ordinaryH1CupTwoCochain

L79 ↗

ClassFieldTower.Cohomology.ordinaryH1CupTwoCochain

Documentation

The inhomogeneous cochain obtained from the canonical character cup.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def ordinaryH1CupTwoCochain
    (chi psi : ContinuousH1ZMod (p := p) (G := Q)) :
    Q × Q → ULift (ZMod p)

theorem

dehomogenizeTwo_continuousH1Cup

L88 ↗

ClassFieldTower.Cohomology.dehomogenizeTwo_continuousH1Cup

Documentation

The explicit homogeneous cup cochain dehomogenizes to the standard inhomogeneous cup formula.

Source context 8 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
omit [DiscreteTopology Q] in

Lean source · statement

theorem dehomogenizeTwo_continuousH1Cup
    (chi psi : ContinuousH1ZMod (p := p) (G := Q)) :
    dehomogenizeTwo
        (continuousH1CupHomogeneousTwoCochainLifted chi psi) =
      ordinaryH1CupTwoCochain chi psi

def

ordinaryH1CupTwoCocycle

L104 ↗

ClassFieldTower.Cohomology.ordinaryH1CupTwoCocycle

Documentation

The ordinary inhomogeneous two-cocycle represented by the canonical character cup formula.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def ordinaryH1CupTwoCocycle
    (chi psi : ContinuousH1ZMod (p := p) (G := Q)) :
    groupCohomology.cocycles₂
      (ordinaryTrivialZModPLifted (p := p) (Q := Q))

def

ordinaryH1CupClass

L117 ↗

ClassFieldTower.Cohomology.ordinaryH1CupClass

Documentation

The ordinary degree-two class represented by the canonical character cup formula.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

def ordinaryH1CupClass
    (chi psi : ContinuousH1ZMod (p := p) (G := Q)) :
    groupCohomology
      (ordinaryTrivialZModPLifted (p := p) (Q := Q)) 2

theorem

discreteH2ShortComplexIso_homologyπ

L127 ↗

ClassFieldTower.Cohomology.discreteH2ShortComplexIso_homologyπ

Documentation

The short-complex comparison carries a homology class represented by a homogeneous cycle to the class of its dehomogenized ordinary cycle.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

theorem discreteH2ShortComplexIso_homologyπ :
    (((trivialZModPCochainsLifted p Q).sc' 1 2 3).map
        (continuousCochainsToAddCommGrp p)).homologyπ ≫
      (ShortComplex.homologyMapIso
        (discreteH2ShortComplexIso (p := p) (Q := Q))).hom =
    ShortComplex.cyclesMap
        (discreteH2ShortComplexIso (p := p) (Q := Q)).hom ≫
      ((groupCohomology.shortComplexH2
          (ordinaryTrivialZModPLifted (p := p) (Q := Q))).map
        ordinaryCochainsToAddCommGrp).homologyπ

theorem

discreteH2MappedShortComplexIso_homologyπ_apply

L140 ↗

ClassFieldTower.Cohomology.discreteH2MappedShortComplexIso_homologyπ_apply

Documentation

The mapped short-complex comparison sends a continuous class to its mapped cycle class.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

theorem discreteH2MappedShortComplexIso_homologyπ_apply
    (z : (((trivialZModPCochainsLifted p Q).sc 2).map
      (continuousCochainsToAddCommGrp p)).cycles) :
    (ShortComplex.homologyMapIso
        (discreteH2MappedShortComplexIso (p := p) (Q := Q))).hom
        (((((trivialZModPCochainsLifted p Q).sc 2).map
          (continuousCochainsToAddCommGrp p)).homologyπ) z) =
      (((groupCohomology.shortComplexH2
          (ordinaryTrivialZModPLifted (p := p) (Q := Q))).map
        ordinaryCochainsToAddCommGrp).homologyπ)
        ((ShortComplex.cyclesMap
          (discreteH2MappedShortComplexIso (p := p) (Q := Q)).hom) z)

theorem

discreteH2MappedShortComplexIso_cyclesMap_cochain

L156 ↗

ClassFieldTower.Cohomology.discreteH2MappedShortComplexIso_cyclesMap_cochain

Documentation

The mapped representative is the dehomogenized ordinary two-cochain.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

theorem discreteH2MappedShortComplexIso_cyclesMap_cochain
    (z : (((trivialZModPCochainsLifted p Q).sc 2).map
      (continuousCochainsToAddCommGrp p)).cycles) :
    (((groupCohomology.shortComplexH2
        (ordinaryTrivialZModPLifted (p := p) (Q := Q))).map
      ordinaryCochainsToAddCommGrp).iCycles)
        ((ShortComplex.cyclesMap
          (discreteH2MappedShortComplexIso (p := p) (Q := Q)).hom) z) =
      dehomogenizeTwo
        (((((trivialZModPCochainsLifted p Q).sc 2).map
          (continuousCochainsToAddCommGrp p)).iCycles) z)

theorem

discreteContinuousH2AddEquiv_continuousH1Cup

L177 ↗

ClassFieldTower.Cohomology.discreteContinuousH2AddEquiv_continuousH1Cup

Documentation

The discrete comparison sends the continuous cup to the ordinary cup class.

Source context 7 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]

Lean source · statement

theorem discreteContinuousH2AddEquiv_continuousH1Cup
    (chi psi : ContinuousH1ZMod (p := p) (G := Q)) :
    discreteContinuousH2AddEquiv (continuousH1CupProductLifted chi psi) =
      ordinaryH1CupClass chi psi

Module documentation

Continuous and ordinary degree-two cohomology of a discrete group

Declarations