NYLL
Module

FiniteStageTransgressionKernel.lean

Nyll.GaloisCohomology.ProP.FiniteStageTransgressionKernel
8 declarations indexed from sourceView source ↗

Module documentation

Kernel exactness for inflated finite-stage transgression

A primitive for a vanishing inflated class is corrected by finite-stage quotient-section residues. The resulting coboundary datum gives a continuous ambient character extending the original invariant kernel character.

Imports1
Imported by3

Declarations

instance

finiteStageKernelTargetTopology

L32 ↗
ClassFieldTower.ProP.finiteStageKernelTargetTopology
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
instance

finiteStageKernelTargetDiscrete

L38 ↗
ClassFieldTower.ProP.finiteStageKernelTargetDiscrete
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
Lean source · statement
instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U)
theorem

finiteStageQuotientMap_out

L45 ↗
ClassFieldTower.ProP.finiteStageQuotientMap_out
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem finiteStageQuotientMap_out
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (q : F ⧸ (R : Subgroup F)) :
    QuotientGroup.mk' (finiteStageImage R U)
        (OpenNormalSubgroup.quotientProj U.1 (Quotient.out q)) =
      finiteStageQuotientMap R U q
def

finiteStageSectionResidueValue

L61 ↗
ClassFieldTower.ProP.finiteStageSectionResidueValue
Documentation

The additive character value of the finite-stage residue of a chosen quotient section.

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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
def finiteStageSectionResidueValue
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (χbar : MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)))
    (q : F ⧸ (R : Subgroup F)) : ZMod p
theorem

quotientSectionResidue_finiteStage_out_mul

L69 ↗
ClassFieldTower.ProP.quotientSectionResidue_finiteStage_out_mul
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionResidue_finiteStage_out_mul
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (q r : F ⧸ (R : Subgroup F)) :
    quotientSectionResidue (finiteStageImage R U)
        (OpenNormalSubgroup.quotientProj U.1 (Quotient.out q) *
          OpenNormalSubgroup.quotientProj U.1 (Quotient.out r)) =
      finiteStageImageMap R U (quotientSectionFactor (R : Subgroup F) q r) *
        quotientSectionResidue (finiteStageImage R U)
          (OpenNormalSubgroup.quotientProj U.1 (Quotient.out (q * r)))
theorem

quotientSectionResidue_finiteStage_decomposition

L87 ↗
ClassFieldTower.ProP.quotientSectionResidue_finiteStage_decomposition
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionResidue_finiteStage_decomposition
    (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F)
    (g : F) :
    quotientSectionResidue (finiteStageImage R U)
        (OpenNormalSubgroup.quotientProj U.1 g) =
      finiteStageImageMap R U
          (quotientSectionResidue (R : Subgroup F) g) *
        quotientSectionResidue (finiteStageImage R U)
          (OpenNormalSubgroup.quotientProj U.1
            (Quotient.out (QuotientGroup.mk' (R : Subgroup F) g)))
theorem

transgressionFactor_eq_inflated_add_residue_boundary

L108 ↗
ClassFieldTower.ProP.transgressionFactor_eq_inflated_add_residue_boundary
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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    DiscreteTopology
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionFactor_eq_inflated_add_residue_boundary
    (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)
    (χ : R →ₜ* Multiplicative (ZMod p))
    (hpull : χbar.comp (finiteStageImageMap R U) = χ.toMonoidHom)
    (q r : F ⧸ (R : Subgroup F)) :
    transgressionFactor (R : Subgroup F) χ.toMonoidHom q r =
      transgressionFactor (finiteStageImage R U) χbar
          (finiteStageQuotientMap R U q) (finiteStageQuotientMap R U r) +
        (finiteStageSectionResidueValue R U χbar r -
          finiteStageSectionResidueValue R U χbar (q * r) +
            finiteStageSectionResidueValue R U χbar q)
theorem

exists_continuous_extension_of_inflatedFiniteTransgressionClass_eq_zero

L163 ↗
ClassFieldTower.ProP.exists_continuous_extension_of_inflatedFiniteTransgressionClass_eq_zero
Documentation

Vanishing of the inflated finite-stage transgression class produces a continuous ambient character extending the original pullback character.

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 finiteStageKernelTargetTopology
    (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    TopologicalSpace
      ((F ⧸ (U.1 : Subgroup F)) ⧸ finiteStageImage R U) := ⊥
local instance finiteStageKernelTargetDiscrete
    (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_continuous_extension_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)
    (χ : R →ₜ* Multiplicative (ZMod p))
    (hχ : ∀ (f : F) (r : R), χ (MulAut.conjNormal f r) = χ r)
    (hpull : χbar.comp (finiteStageImageMap R U) = χ.toMonoidHom)
    (hzero : inflatedFiniteTransgressionClass R U χbar hχbar = 0) :
    ∃ ψ : F →ₜ* Multiplicative (ZMod p),
      ψ.comp (subgroupInclusion (R : Subgroup F)) = χ

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