Module

InflationTransgressionExact.lean

Nyll.GaloisCohomology.ProP.InflationTransgressionExact

4 declarations indexed from sourceView source ↗

Module documentation

Continuous inflation--transgression exactness in degree two

For an open normal subgroup, continuous transgression has range exactly the kernel of degree-two inflation. The reverse inclusion is proved at cochain level by restricting a continuous primitive of the inflated cocycle.

Imports1

Nyll.GaloisCohomology.ProP.ContinuousTransgressionPrimitive

Imported by3

theorem

normalizedCocycle_sub

L35 ↗

ClassFieldTower.Cohomology.normalizedCocycle_sub

Source context 12 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
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
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 normalizedCocycle_sub
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (z w : trivialZModPCocyclesLifted p H 2) (g h : H) :
    normalizedCocycle (z - w) g h =
      normalizedCocycle z g h - normalizedCocycle w g h

theorem

normalizedCocycle_continuousTransgression

L57 ↗

ClassFieldTower.Cohomology.normalizedCocycle_continuousTransgression

Source context 12 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
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
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 normalizedCocycle_continuousTransgression
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U)
    (q r : G ⧸ (U.1 : Subgroup G)) :
    normalizedCocycle (continuousTransgressionHomogeneousCocycle U chi) q r =
      ULift.up (transgressionFactor (U.1 : Subgroup G)
        (characterOfH1 chi.1).toMonoidHom q r) -
      ULift.up (transgressionFactor (U.1 : Subgroup G)
        (characterOfH1 chi.1).toMonoidHom 1 1)

theorem

continuousTransgressionClass_invariantContinuousH1OfInflationPrimitive

L86 ↗

ClassFieldTower.Cohomology.continuousTransgressionClass_invariantContinuousH1OfInflationPrimitive

Documentation

A reconstructed invariant character transgresses to the original quotient cocycle class.

Source context 12 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
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
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 continuousTransgressionClass_invariantContinuousH1OfInflationPrimitive
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (z : trivialZModPCocyclesLifted p (G ⧸ (U.1 : Subgroup G)) 2)
    (c : (trivialZModPCochainsLifted p G).X 1)
    (hc : ((trivialZModPCochainsLifted p G).d 1 2).hom c =
      (((trivialZModPCochainsMapLifted p
        (OpenNormalSubgroupInClass.quotientProj U)).f 2).hom
          (((trivialZModPCochainsLifted p
            (G ⧸ (U.1 : Subgroup G))).iCycles 2).hom z))) :
    continuousTransgressionClass U
        (invariantContinuousH1OfInflationPrimitive U z c hc) =
      ContinuousCohomology.π
        (trivialZModPLifted p (G ⧸ (U.1 : Subgroup G))) 2 z

theorem

continuousTransgression_range_eq_degreeTwoInflation_ker

L161 ↗

ClassFieldTower.Cohomology.continuousTransgression_range_eq_degreeTwoInflation_ker

Documentation

Continuous Hochschild--Serre exactness at degree two for an open normal subgroup.

Source context 12 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
open ClassFieldTower.ProP
open ClassFieldTower.ProP.FreeProPH2Cocycle
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 continuousTransgression_range_eq_degreeTwoInflation_ker
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    LinearMap.range (continuousTransgressionLinearMap U) =
      LinearMap.ker (degreeTwoInflationLinearMap U)

Module documentation

Continuous inflation--transgression exactness in degree two

Declarations

normalizedCocycle_sub

normalizedCocycle_continuousTransgression

continuousTransgressionClass_invariantContinuousH1OfInflationPrimitive

continuousTransgression_range_eq_degreeTwoInflation_ker