NYLL
Module

FiniteTransgressionKernel.lean

Nyll.GaloisCohomology.ProP.FiniteTransgressionKernel
13 declarations indexed from sourceView source ↗

Module documentation

Kernel exactness for finite transgression

If the explicit factor-set class of an invariant character vanishes, an elementwise boundary calculation constructs an extension of that character to the ambient group. This is the kernel half of the low-degree transgression exact sequence needed for relation-rank comparison.

Imports7
  • Nyll.GaloisCohomology.ProP.FiniteTransgression
  • 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 by5

Declarations

instance

kernelQuotientTopology

L35 ↗
ClassFieldTower.Cohomology.kernelQuotientTopology
Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
Lean source · statement
instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N)
instance

kernelQuotientDiscrete

L36 ↗
ClassFieldTower.Cohomology.kernelQuotientDiscrete
Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
Lean source · statement
instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N)
def

quotientSectionResidue

L40 ↗
ClassFieldTower.Cohomology.quotientSectionResidue
Documentation

The kernel residue left after removing the chosen quotient representative.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def quotientSectionResidue (N : Subgroup P) [N.Normal]
    (g : P) : N
theorem

quotientSectionResidue_apply

L47 ↗
ClassFieldTower.Cohomology.quotientSectionResidue_apply
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionResidue_apply (N : Subgroup P) [N.Normal]
    (g : P) :
    (quotientSectionResidue N g : P) =
      g * (Quotient.out (QuotientGroup.mk' N g : P ⧸ N))⁻¹
theorem

quotientSectionResidue_mul_identity

L54 ↗
ClassFieldTower.Cohomology.quotientSectionResidue_mul_identity
Documentation

Multiplication of residues differs by conjugation and the quotient factor set.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionResidue_mul_identity (N : Subgroup P) [N.Normal]
    (g h : P) :
    quotientSectionResidue N g *
          MulAut.conjNormal
            (Quotient.out (QuotientGroup.mk' N g : P ⧸ N))
            (quotientSectionResidue N h) *
        quotientSectionFactor N (QuotientGroup.mk' N g) (QuotientGroup.mk' N h) =
      quotientSectionResidue N (g * h)
theorem

character_quotientSectionResidue_mul

L67 ↗
ClassFieldTower.Cohomology.character_quotientSectionResidue_mul
Documentation

Applying an invariant character to the residue multiplication identity.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem character_quotientSectionResidue_mul
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n)
    (g h : P) :
    (χ (quotientSectionResidue N (g * h))).toAdd =
      (χ (quotientSectionResidue N g)).toAdd +
        (χ (quotientSectionResidue N h)).toAdd +
          transgressionFactor N χ (QuotientGroup.mk' N g) (QuotientGroup.mk' N h)
def

transgressionKernelExtension

L85 ↗
ClassFieldTower.Cohomology.transgressionKernelExtension
Documentation

An invariant kernel character extends whenever its factor set is a coboundary.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · full declaration
def transgressionKernelExtension
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n)
    (b : P ⧸ N → ZMod p)
    (hb : ∀ q r,
      b r - b (q * r) + b q = transgressionFactor N χ q r) :
    MonoidHom P (Multiplicative (ZMod p)) where
  toFun g := Multiplicative.ofAdd
    ((χ (quotientSectionResidue N g)).toAdd + b (QuotientGroup.mk' N g))
  map_one' := by
    change Multiplicative.ofAdd
      ((χ (quotientSectionResidue N 1)).toAdd + b 1) = 1
    have hres : quotientSectionResidue N 1 =
        (quotientSectionFactor N 1 1)⁻¹ := by
      apply Subtype.ext
      simp [quotientSectionResidue, quotientSectionFactor]
    have hb11 := hb 1 1
    simp only [one_mul, sub_self, zero_add] at hb11
    rw [hres, map_inv]
    change Multiplicative.ofAdd
      (-(χ (quotientSectionFactor N 1 1)).toAdd + b 1) = 1
    rw [hb11]
    simp [transgressionFactor]
  map_mul' g h := by
    change (χ (quotientSectionResidue N (g * h))).toAdd +
        b (QuotientGroup.mk' N (g * h)) =
      ((χ (quotientSectionResidue N g)).toAdd + b (QuotientGroup.mk' N g)) +
        ((χ (quotientSectionResidue N h)).toAdd + b (QuotientGroup.mk' N h))
    rw [character_quotientSectionResidue_mul N χ hχ]
    have hmk : QuotientGroup.mk' N (g * h) =
        QuotientGroup.mk' N g * QuotientGroup.mk' N h :=
      map_mul (QuotientGroup.mk' N) g h
    rw [hmk]
    have hbgh := hb (QuotientGroup.mk' N g) (QuotientGroup.mk' N h)
    calc
      (χ (quotientSectionResidue N g)).toAdd +
            (χ (quotientSectionResidue N h)).toAdd +
            transgressionFactor N χ (QuotientGroup.mk' N g) (QuotientGroup.mk' N h) +
          b (QuotientGroup.mk' N g * QuotientGroup.mk' N h) =
        (χ (quotientSectionResidue N g)).toAdd +
          b (QuotientGroup.mk' N g) +
          ((χ (quotientSectionResidue N h)).toAdd +
            b (QuotientGroup.mk' N h)) := by
              rw [← hbgh]
              abel
theorem

transgressionKernelExtension_restrict

L133 ↗
ClassFieldTower.Cohomology.transgressionKernelExtension_restrict
Documentation

The coboundary extension restricts to the original kernel character.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionKernelExtension_restrict
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n)
    (b : P ⧸ N → ZMod p)
    (hb : ∀ q r,
      b r - b (q * r) + b q = transgressionFactor N χ q r) :
    (transgressionKernelExtension N χ hχ b hb).comp N.subtype = χ
def

homogeneousOneCochainNormalizedValue

L166 ↗
ClassFieldTower.Cohomology.homogeneousOneCochainNormalizedValue
Documentation

The normalized inhomogeneous value of a homogeneous degree-one cochain.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def homogeneousOneCochainNormalizedValue
    (N : Subgroup P) [N.Normal]
    (c : (TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).X 1)
    (q : P ⧸ N) : ZMod p
theorem

homogeneousOneCochain_invariant

L174 ↗
ClassFieldTower.Cohomology.homogeneousOneCochain_invariant
Documentation

Homogeneous degree-one cochains are invariant under simultaneous left translation.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem homogeneousOneCochain_invariant
    (N : Subgroup P) [N.Normal]
    (c : (TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).X 1)
    (a q r : P ⧸ N) :
    c.1 (a⁻¹ * q) (a⁻¹ * r) = c.1 q r
theorem

homogeneousOneCochainNormalizedValue_primitive

L189 ↗
ClassFieldTower.Cohomology.homogeneousOneCochainNormalizedValue_primitive
Documentation

A homogeneous primitive of the factor cochain yields its inhomogeneous coboundary formula.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem homogeneousOneCochainNormalizedValue_primitive
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (c : (TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).X 1)
    (hc : ((TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).d 1 2).hom c =
        transgressionHomogeneousCochain N χ)
    (q r : P ⧸ N) :
    homogeneousOneCochainNormalizedValue N c r -
        homogeneousOneCochainNormalizedValue N c (q * r) +
          homogeneousOneCochainNormalizedValue N c q =
      transgressionFactor N χ q r
theorem

exists_boundary_of_homologyπ_apply_eq_zero

L238 ↗
ClassFieldTower.Cohomology.exists_boundary_of_homologyπ_apply_eq_zero
Documentation

Extract an elementwise boundary from a cocycle whose homology class vanishes.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem exists_boundary_of_homologyπ_apply_eq_zero
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ)
    (z : ContinuousCohomology.cocycles A (n + 1))
    (hz : ContinuousCohomology.π A (n + 1) z = 0) :
    ∃ c : (TopRep.homogeneousCochains A).X n,
      ((TopRep.homogeneousCochains A).d n (n + 1)).hom c =
        ((TopRep.homogeneousCochains A).iCycles (n + 1)).hom z
theorem

exists_extension_of_finiteTransgressionClass_eq_zero

L263 ↗
ClassFieldTower.Cohomology.exists_extension_of_finiteTransgressionClass_eq_zero
Documentation

Vanishing of the finite factor-set class forces the invariant kernel character to extend.

Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {P : Type u} [Group P]
local instance kernelQuotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance kernelQuotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem exists_extension_of_finiteTransgressionClass_eq_zero
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n)
    (hzero : finiteTransgressionClass N χ hχ = 0) :
    ∃ ψ : MonoidHom P (Multiplicative (ZMod p)), ψ.comp N.subtype = χ

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