Module

InflationTransgressionQuotient.lean

Nyll.GaloisCohomology.ProP.InflationTransgressionQuotient

3 declarations indexed from sourceView source ↗

Module documentation

Quotient presentation of a degree-two inflation range

The inflation--transgression kernel calculation identifies finite-stage degree-two cohomology modulo continuous transgression with the corresponding range in ambient degree-two cohomology.

Imports2

Nyll.GaloisCohomology.ProP.InflationTransgressionExact
Mathlib.LinearAlgebra.Isomorphisms

Imported by1

Nyll.GaloisCohomology.ProP.All

def

degreeTwoQuotientTransgressionEquivInflationRange

L34 ↗

ClassFieldTower.Cohomology.degreeTwoQuotientTransgressionEquivInflationRange

Documentation

The first isomorphism theorem for degree-two inflation, with its kernel rewritten as the range of continuous transgression.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

def degreeTwoQuotientTransgressionEquivInflationRange
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    (continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2 ⧸
        LinearMap.range (continuousTransgressionLinearMap U)) ≃ₗ[ZMod p]
      degreeTwoInflationRange (p := p) U

theorem

degreeTwoQuotientTransgressionEquivInflationRange_apply_mk

L45 ↗

ClassFieldTower.Cohomology.degreeTwoQuotientTransgressionEquivInflationRange_apply_mk

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem degreeTwoQuotientTransgressionEquivInflationRange_apply_mk
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (x : continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2) :
    degreeTwoQuotientTransgressionEquivInflationRange U
        (Submodule.Quotient.mk x) =
      ⟨degreeTwoInflationLinearMap U x,
        LinearMap.mem_range_self (degreeTwoInflationLinearMap U) x⟩

theorem

finrank_degreeTwoQuotientTransgression_eq_inflationRange

L57 ↗

ClassFieldTower.Cohomology.finrank_degreeTwoQuotientTransgression_eq_inflationRange

Documentation

Finite-stage degree-two cohomology modulo continuous transgression and its ambient inflation range have equal ZMod p-dimension.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem finrank_degreeTwoQuotientTransgression_eq_inflationRange
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    Module.finrank (ZMod p)
        (continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2 ⧸
          LinearMap.range (continuousTransgressionLinearMap U)) =
      Module.finrank (ZMod p) (degreeTwoInflationRange (p := p) U)

Module documentation

Quotient presentation of a degree-two inflation range

Declarations

degreeTwoQuotientTransgressionEquivInflationRange

degreeTwoQuotientTransgressionEquivInflationRange_apply_mk

finrank_degreeTwoQuotientTransgression_eq_inflationRange