Module

ProfiniteIntegerH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.ProfiniteIntegerH2

5 declarations indexed from sourceView source ↗

Module documentation

Degree-two cohomology of the profinite integers

The rank-one free-profinite property of ZHat splits the compact profinite central extension attached to every continuous homogeneous two-cocycle. The section supplies an explicit degree-one primitive, so continuous degree-two cohomology with trivial lifted ZMod p coefficients vanishes.

Imports4

Imported by2

theorem

exists_continuous_section_of_surjective

L34 ↗

ClassFieldTower.Cohomology.ProfiniteInteger.exists_continuous_section_of_surjective

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem exists_continuous_section_of_surjective
    {E : Type} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
    [CompactSpace E] [T2Space E] [TotallyDisconnectedSpace E]
    (hE : HasOpenNormalBasisInClass FiniteGroupClass.allFinite E)
    (q : E →ₜ* ClassFormation.ZHatMul) (hq : Function.Surjective q) :
    ∃ s : ClassFormation.ZHatMul →ₜ* E,
      q.comp s = ContinuousMonoidHom.id ClassFormation.ZHatMul

theorem

normalizedCocycle_is_continuous_coboundary

L57 ↗

ClassFieldTower.Cohomology.ProfiniteInteger.normalizedCocycle_is_continuous_coboundary

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem normalizedCocycle_is_continuous_coboundary
    (z : trivialZModPCocyclesLifted p ClassFormation.ZHatMul 2) :
    ∃ b : C(ClassFormation.ZHatMul, A p), ∀ g h,
      b (g * h) = b g + b h + normalizedCocycle z g h

theorem

degree_two_π_apply_eq_zero

L118 ↗

ClassFieldTower.Cohomology.ProfiniteInteger.degree_two_π_apply_eq_zero

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degree_two_π_apply_eq_zero
    (z : trivialZModPCocyclesLifted p ClassFormation.ZHatMul 2) :
    ContinuousCohomology.π (trivialZModPLifted p ClassFormation.ZHatMul) 2 z = 0

theorem

degree_two_π_eq_zero

L138 ↗

ClassFieldTower.Cohomology.ProfiniteInteger.degree_two_π_eq_zero

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degree_two_π_eq_zero :
    ContinuousCohomology.π (trivialZModPLifted p ClassFormation.ZHatMul) 2 = 0

theorem

degree_two_subsingleton

L144 ↗

ClassFieldTower.Cohomology.ProfiniteInteger.degree_two_subsingleton

Documentation

Continuous H²(ZHat, ZMod p) with trivial lifted coefficients vanishes.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
noncomputable section
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem degree_two_subsingleton :
    Subsingleton (continuousCohomologyZModPLifted p ClassFormation.ZHatMul 2)

Module documentation

Degree-two cohomology of the profinite integers

Declarations

exists_continuous_section_of_surjective

normalizedCocycle_is_continuous_coboundary

degree_two_π_apply_eq_zero

degree_two_π_eq_zero

degree_two_subsingleton