NYLL
Module

PresentationQuotientEquiv.lean

Nyll.GaloisCohomology.ProP.PresentationQuotientEquiv
2 declarations indexed from sourceView source ↗

Module documentation

Cohomology across a presentation quotient

Continuous group equivalences induce linear equivalences on continuous cohomology. A finite pro-p presentation supplies the required topological first-isomorphism equivalence between the quotient of its free source by the presentation kernel and its target.

Imports3
Imported by7

Declarations

def

continuousCohomologyZModPLiftedLinearEquiv

L35 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPLiftedLinearEquiv
Documentation

A continuous group equivalence induces a linear equivalence on continuous cohomology with lifted trivial ZMod p coefficients.

Source context 9 commands

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

open CategoryTheory
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def continuousCohomologyZModPLiftedLinearEquiv
    (e : H ≃ₜ* G) (n : ℕ) :
    continuousCohomologyZModPLifted p G n ≃ₗ[ZMod p]
      continuousCohomologyZModPLifted p H n
def

quotientKerContinuousMulEquiv

L95 ↗
ClassFieldTower.ProP.FiniteProPPresentation.quotientKerContinuousMulEquiv
Documentation

The topological first-isomorphism equivalence supplied by a finite presentation.

Source context 10 commands

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

open CategoryTheory
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def FiniteProPPresentation.quotientKerContinuousMulEquiv
    (P : FiniteProPPresentation p d r sourceData G) :
    (sourceData.carrier ⧸
      (P.quotient.toMonoidHom.ker : Subgroup sourceData.carrier)) ≃ₜ* G

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