NYLL
Module

FiniteStageTransgressionPrimitive.lean

Nyll.GaloisCohomology.ProP.FiniteStageTransgressionPrimitive
7 declarations indexed from sourceView source ↗

Module documentation

Primitives for inflated finite-stage transgression

If an inflated finite-stage transgression class vanishes, its explicit homogeneous cocycle is a boundary. This file extracts a degree-one primitive and records its normalized coboundary identity. The residue correction and continuous kernel extension are built in the downstream kernel module.

Imports7
  • Nyll.GaloisCohomology.ProP.FiniteStageTransgression
  • 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
Imported by2

Declarations

instance

finiteStagePrimitiveTargetTopology

L39 ↗
ClassFieldTower.ProP.finiteStagePrimitiveTargetTopology
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
instance

finiteStagePrimitiveTargetDiscrete

L45 ↗
ClassFieldTower.ProP.finiteStagePrimitiveTargetDiscrete
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
Lean source · statement
instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
theorem

inflatedTransgressionCochain_apply

L52 ↗
ClassFieldTower.ProP.inflatedTransgressionCochain_apply
Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem inflatedTransgressionCochain_apply
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χbar : MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)))
    (a b c : F ⧸ (R : Subgroup F)) :
    (((trivialZModPCochainsMapLifted p (finiteStageQuotientMap R U)).f 2).hom
      (transgressionHomogeneousCochain (finiteStageImage R U) χbar)).1 a b c =
        ULift.up (transgressionFactor (finiteStageImage R U) χbar
          (finiteStageQuotientMap R U (a⁻¹ * b))
          (finiteStageQuotientMap R U (b⁻¹ * c)))
def

inflatedPrimitiveValue

L70 ↗
ClassFieldTower.ProP.inflatedPrimitiveValue
Documentation

The normalized value of a degree-one cochain on the original quotient.

Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
def inflatedPrimitiveValue
    (R : ClosedSubgroup F) [R.Normal]
    (c : (trivialZModPCochainsLifted p (F ⧸ (R : Subgroup F))).X 1)
    (q : F ⧸ (R : Subgroup F)) : ZMod p
theorem

inflatedHomogeneousOneCochain_invariant

L77 ↗
ClassFieldTower.ProP.inflatedHomogeneousOneCochain_invariant
Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
omit [Fact p.Prime] in
Lean source · statement
theorem inflatedHomogeneousOneCochain_invariant
    (R : ClosedSubgroup F) [R.Normal]
    (c : (trivialZModPCochainsLifted p (F ⧸ (R : Subgroup F))).X 1)
    (a q r : F ⧸ (R : Subgroup F)) :
    c.1 (a⁻¹ * q) (a⁻¹ * r) = c.1 q r
theorem

homogeneousOneCochainNormalizedValue_inflated_primitive

L90 ↗
ClassFieldTower.ProP.homogeneousOneCochainNormalizedValue_inflated_primitive
Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem homogeneousOneCochainNormalizedValue_inflated_primitive
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χbar : MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)))
    (c : (trivialZModPCochainsLifted p (F ⧸ (R : Subgroup F))).X 1)
    (hc : ((trivialZModPCochainsLifted p
      (F ⧸ (R : Subgroup F))).d 1 2).hom c =
        (((trivialZModPCochainsMapLifted p (finiteStageQuotientMap R U)).f 2).hom
          (transgressionHomogeneousCochain (finiteStageImage R U) χbar)))
    (q r : F ⧸ (R : Subgroup F)) :
    inflatedPrimitiveValue R c r -
        inflatedPrimitiveValue R c (q * r) +
          inflatedPrimitiveValue R c q =
      transgressionFactor (finiteStageImage R U) χbar
        (finiteStageQuotientMap R U q) (finiteStageQuotientMap R U r)
theorem

exists_primitive_of_inflatedFiniteTransgressionClass_eq_zero

L149 ↗
ClassFieldTower.ProP.exists_primitive_of_inflatedFiniteTransgressionClass_eq_zero
Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
open ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
local instance finiteStagePrimitiveTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStagePrimitiveTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem exists_primitive_of_inflatedFiniteTransgressionClass_eq_zero
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χbar : MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)))
    (hχbar : ∀ (g : F ⧸ (U.1 : Subgroup F)) (n : finiteStageImage R U),
      χbar (MulAut.conjNormal g n) = χbar n)
    (hzero : inflatedFiniteTransgressionClass R U χbar hχbar = 0) :
    ∃ c : (trivialZModPCochainsLifted p (F ⧸ (R : Subgroup F))).X 1,
      ((trivialZModPCochainsLifted p (F ⧸ (R : Subgroup F))).d 1 2).hom c =
        (((trivialZModPCochainsMapLifted p (finiteStageQuotientMap R U)).f 2).hom
          (transgressionHomogeneousCochain (finiteStageImage R U) χbar))

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