NYLL
Module

InflationTransgressionRange.lean

Nyll.GaloisCohomology.ProP.InflationTransgressionRange
6 declarations indexed from sourceView source ↗

Module documentation

Continuous transgression is killed by degree-two inflation

For an open normal subgroup, every continuous transgression class lies in the kernel of degree-two inflation. The proof uses an explicit continuous homogeneous primitive after inflation.

Imports2
Imported by2

Declarations

def

degreeTwoInflationLinearMap

L35 ↗
ClassFieldTower.Cohomology.degreeTwoInflationLinearMap
Documentation

Degree-two inflation from an open finite quotient.

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
open ClassFieldTower.ProP
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 degreeTwoInflationLinearMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2 →ₗ[ZMod p]
      continuousCohomologyZModPLifted p G 2
def

quotientSectionResidueContinuousMap

L43 ↗
ClassFieldTower.Cohomology.quotientSectionResidueContinuousMap
Documentation

The kernel residue is continuous when the normal subgroup is open.

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
open ClassFieldTower.ProP
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 · full declaration
def quotientSectionResidueContinuousMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    C(G, (U.1 : Subgroup G)) where
  toFun := quotientSectionResidue (U.1 : Subgroup G)
  continuous_toFun := by
    apply Continuous.subtype_mk
    change Continuous (fun g : G ↦
      g * (Quotient.out (OpenNormalSubgroupInClass.quotientProj U g))⁻¹)
    exact continuous_id.mul
      ((continuous_of_discreteTopology.comp
        (OpenNormalSubgroupInClass.quotientProj U).continuous_toFun).inv)
def

continuousResidueValue

L56 ↗
ClassFieldTower.Cohomology.continuousResidueValue
Documentation

The inhomogeneous residue value of a continuous invariant character.

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
open ClassFieldTower.ProP
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 · full declaration
def continuousResidueValue
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) : C(G, ZMod p) where
  toFun g := chi.1 (Additive.ofMul (quotientSectionResidue (U.1 : Subgroup G) g))
  continuous_toFun := chi.1.continuous_toFun.comp
    (quotientSectionResidueContinuousMap U).continuous_toFun
def

continuousTransgressionInflationPrimitive

L64 ↗
ClassFieldTower.Cohomology.continuousTransgressionInflationPrimitive
Documentation

A homogeneous primitive for the inflation of a transgression cocycle.

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
open ClassFieldTower.ProP
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 continuousTransgressionInflationPrimitive
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    (trivialZModPCochainsLifted p G).X 1
theorem

continuousTransgressionInflationPrimitive_boundary

L83 ↗
ClassFieldTower.Cohomology.continuousTransgressionInflationPrimitive_boundary
Source context 11 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
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 continuousTransgressionInflationPrimitive_boundary
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    ((trivialZModPCochainsLifted p G).d 1 2).hom
        (continuousTransgressionInflationPrimitive U chi) =
      (((trivialZModPCochainsMapLifted p
        (OpenNormalSubgroupInClass.quotientProj U)).f 2).hom
          (continuousTransgressionHomogeneousCochain U chi))
theorem

degreeTwoInflation_continuousTransgression_eq_zero

L120 ↗
ClassFieldTower.Cohomology.degreeTwoInflation_continuousTransgression_eq_zero
Documentation

Every continuous transgression class dies under degree-two inflation.

Source context 11 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
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 degreeTwoInflation_continuousTransgression_eq_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    degreeTwoInflationLinearMap U (continuousTransgressionLinearMap U chi) = 0

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