NYLL
Module

ContinuousTransgressionPrimitive.lean

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

Module documentation

Primitives for continuous inflation--transgression exactness

This file extracts the normalized degree-one primitive of an inflated degree-two cocycle and uses its restriction to the open normal subgroup to reconstruct the invariant continuous character occurring in transgression.

Imports9
  • Nyll.GaloisCohomology.ProP.InflationTransgressionRange
  • Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
  • Mathlib.RepresentationTheory.Continuous.Basic
  • Mathlib.RepresentationTheory.Continuous.TopRep
  • Mathlib.Topology.ContinuousMap.Algebra
  • Mathlib.Topology.ContinuousMap.Basic
  • Mathlib.Topology.ContinuousMap.Defs
  • Mathlib.Algebra.Group.Defs
  • Mathlib.Algebra.Group.Basic
Imported by2

Declarations

def

normalizedInflationPrimitiveValue

L43 ↗
ClassFieldTower.Cohomology.normalizedInflationPrimitiveValue
Documentation

Normalize a homogeneous degree-one cochain at the identity.

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
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]
Lean source · full declaration
def normalizedInflationPrimitiveValue
    (c : (trivialZModPCochainsLifted p G).X 1) :
    C(G, ULift.{u} (ZMod p)) where
  toFun g := c.1 1 g - c.1 1 1
  continuous_toFun := (c.1 1).continuous.sub continuous_const
theorem

normalizedInflationPrimitiveValue_one

L51 ↗
ClassFieldTower.Cohomology.normalizedInflationPrimitiveValue_one
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 normalizedInflationPrimitiveValue_one
    (c : (trivialZModPCochainsLifted p G).X 1) :
    normalizedInflationPrimitiveValue c 1 = 0
theorem

normalizedInflationPrimitive_boundary

L57 ↗
ClassFieldTower.Cohomology.normalizedInflationPrimitive_boundary
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 normalizedInflationPrimitive_boundary
    (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)))
    (g h : G) :
    normalizedInflationPrimitiveValue c h -
        normalizedInflationPrimitiveValue c (g * h) +
          normalizedInflationPrimitiveValue c g =
      normalizedCocycle z
        (OpenNormalSubgroupInClass.quotientProj U g)
        (OpenNormalSubgroupInClass.quotientProj U h)
def

invariantContinuousH1OfInflationPrimitive

L140 ↗
ClassFieldTower.Cohomology.invariantContinuousH1OfInflationPrimitive
Documentation

Restrict the negative normalized primitive to the open normal subgroup. The boundary identity makes it a continuous character, and makes that character invariant under ambient conjugation.

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
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]
Lean source · statement
def 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))) :
    InvariantContinuousH1 U
def

inflationPrimitiveQuotientCorrection

L231 ↗
ClassFieldTower.Cohomology.inflationPrimitiveQuotientCorrection
Documentation

The quotient correction obtained by evaluating the normalized primitive on chosen quotient representatives.

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
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]
Lean source · full declaration
def inflationPrimitiveQuotientCorrection
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (c : (trivialZModPCochainsLifted p G).X 1) :
    C(G ⧸ (U.1 : Subgroup G), ULift.{u} (ZMod p)) where
  toFun q := normalizedInflationPrimitiveValue c (Quotient.out q) -
    normalizedInflationPrimitiveValue c
      (Quotient.out (1 : G ⧸ (U.1 : Subgroup G)))
  continuous_toFun := continuous_of_discreteTopology
theorem

reconstructed_transgressionFactor

L241 ↗
ClassFieldTower.Cohomology.reconstructed_transgressionFactor
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 reconstructed_transgressionFactor
    (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)))
    (q r : G ⧸ (U.1 : Subgroup G)) :
    ULift.up (transgressionFactor (U.1 : Subgroup G)
        (characterOfH1
          (invariantContinuousH1OfInflationPrimitive U z c hc).1).toMonoidHom q r) =
      normalizedCocycle z q r -
        normalizedInflationPrimitiveValue c (Quotient.out q) -
        normalizedInflationPrimitiveValue c (Quotient.out r) +
        normalizedInflationPrimitiveValue c (Quotient.out (q * r))

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