Module

DiscreteH2ShortComplexComparison.lean

Nyll.GaloisCohomology.ProP.DiscreteH2ShortComplexComparison

9 declarations indexed from sourceView source ↗

Module documentation

The degree-two short complex for a discrete group

The explicit homogeneous/inhomogeneous cochain equivalences commute with the two differentials surrounding degree two. We package them as an isomorphism of short complexes after forgetting topology and restricting scalars from ZMod p to Int.

Imports8

Nyll.GaloisCohomology.ProP.DiscreteH2CochainComparison
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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 by4

abbrev

ordinaryTrivialZModPLifted

L37 ↗

ClassFieldTower.Cohomology.ordinaryTrivialZModPLifted

Documentation

The ordinary trivial representation matching the lifted continuous coefficient carrier.

Source context 6 commands

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

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

Lean source · statement

abbrev ordinaryTrivialZModPLifted : Rep ℤ Q

theorem

dehomogenizeOne_d

L42 ↗

ClassFieldTower.Cohomology.dehomogenizeOne_d

Documentation

Dehomogenization intertwines the degree-one differentials.

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
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 dehomogenizeOne_d
    (c : (trivialZModPCochainsLifted p Q).X 1) :
    dehomogenizeTwo
        ((trivialZModPCochainsLifted p Q).d 1 2 c) =
      groupCohomology.d₁₂ (ordinaryTrivialZModPLifted (p := p) (Q := Q))
        (dehomogenizeOne c)

theorem

dehomogenizeTwo_d

L74 ↗

ClassFieldTower.Cohomology.dehomogenizeTwo_d

Documentation

Dehomogenization intertwines the degree-two differentials.

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
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_d
    (c : (trivialZModPCochainsLifted p Q).X 2) :
    dehomogenizeThree
        ((trivialZModPCochainsLifted p Q).d 2 3 c) =
      groupCohomology.d₂₃ (ordinaryTrivialZModPLifted (p := p) (Q := Q))
        (dehomogenizeTwo c)

abbrev

continuousCochainsToAddCommGrp

L110 ↗

ClassFieldTower.Cohomology.continuousCochainsToAddCommGrp

Documentation

Forget topology and the ZMod p-linear structure, retaining the underlying additive group.

Source context 6 commands

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

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

Lean source · statement

abbrev continuousCochainsToAddCommGrp (p : ℕ) :
    TopModuleCat (ZMod p) ⥤ AddCommGrpCat

abbrev

ordinaryCochainsToAddCommGrp

L116 ↗

ClassFieldTower.Cohomology.ordinaryCochainsToAddCommGrp

Documentation

Forget the Int-linear structure on ordinary group cochains.

Source context 6 commands

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

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

Lean source · statement

abbrev ordinaryCochainsToAddCommGrp : ModuleCat ℤ ⥤ AddCommGrpCat

def

homogeneousOneCochainAddCommGrpIso

L120 ↗

ClassFieldTower.Cohomology.homogeneousOneCochainAddCommGrpIso

Documentation

The degree-one cochain equivalence as an additive-group isomorphism.

Source context 6 commands

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

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

Lean source · statement

def homogeneousOneCochainAddCommGrpIso :
    (continuousCochainsToAddCommGrp p).obj
        ((trivialZModPCochainsLifted p Q).X 1) ≅
      (ordinaryCochainsToAddCommGrp).obj
        (ModuleCat.of ℤ (Q → ULift (ZMod p)))

def

homogeneousTwoCochainAddCommGrpIso

L128 ↗

ClassFieldTower.Cohomology.homogeneousTwoCochainAddCommGrpIso

Documentation

The degree-two cochain equivalence as an additive-group isomorphism.

Source context 6 commands

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

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

Lean source · statement

def homogeneousTwoCochainAddCommGrpIso :
    (continuousCochainsToAddCommGrp p).obj
        ((trivialZModPCochainsLifted p Q).X 2) ≅
      (ordinaryCochainsToAddCommGrp).obj
        (ModuleCat.of ℤ (Q × Q → ULift (ZMod p)))

def

homogeneousThreeCochainAddCommGrpIso

L136 ↗

ClassFieldTower.Cohomology.homogeneousThreeCochainAddCommGrpIso

Documentation

The degree-three cochain equivalence as an additive-group isomorphism.

Source context 6 commands

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

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

Lean source · statement

def homogeneousThreeCochainAddCommGrpIso :
    (continuousCochainsToAddCommGrp p).obj
        ((trivialZModPCochainsLifted p Q).X 3) ≅
      (ordinaryCochainsToAddCommGrp).obj
        (ModuleCat.of ℤ (Q × Q × Q → ULift (ZMod p)))

def

discreteH2ShortComplexIso

L145 ↗

ClassFieldTower.Cohomology.discreteH2ShortComplexIso

Documentation

For a discrete group, the homogeneous continuous degree-two short complex is the ordinary inhomogeneous one after forgetting structure.

Source context 6 commands

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

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

Lean source · statement

def discreteH2ShortComplexIso :
    ((trivialZModPCochainsLifted p Q).sc' 1 2 3).map
        (continuousCochainsToAddCommGrp p) ≅
      (groupCohomology.shortComplexH2
          (ordinaryTrivialZModPLifted (p := p) (Q := Q))).map
        ordinaryCochainsToAddCommGrp

Module documentation

The degree-two short complex for a discrete group

Declarations