NYLL
Module

FiniteTransgression.lean

Nyll.GaloisCohomology.ProP.FiniteTransgression
15 declarations indexed from sourceView source ↗

Module documentation

Finite transgression factor sets

An ambient-conjugation-invariant ZMod p character on a normal subgroup determines the usual factor-set homogeneous two-cocycle on the discrete quotient, and hence a continuous degree-two cohomology class with universe-lifted trivial coefficients.

Imports4
Imported by5

Declarations

instance

quotientTopology

L32 ↗
ClassFieldTower.Cohomology.quotientTopology
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N)
instance

quotientDiscrete

L33 ↗
ClassFieldTower.Cohomology.quotientDiscrete
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
Lean source · statement
instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N)
def

quotientSectionFactor

L37 ↗
ClassFieldTower.Cohomology.quotientSectionFactor
Documentation

The factor of the chosen quotient representatives.

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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def quotientSectionFactor (N : Subgroup P) [N.Normal]
    (q r : P ⧸ N) : N
theorem

quotientSectionFactor_apply

L44 ↗
ClassFieldTower.Cohomology.quotientSectionFactor_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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionFactor_apply (N : Subgroup P) [N.Normal]
    (q r : P ⧸ N) :
    (quotientSectionFactor N q r : P) =
      Quotient.out q * Quotient.out r * (Quotient.out (q * r))⁻¹
theorem

quotientSectionFactor_cocycle_identity

L50 ↗
ClassFieldTower.Cohomology.quotientSectionFactor_cocycle_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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem quotientSectionFactor_cocycle_identity (N : Subgroup P) [N.Normal]
    (q r s : P ⧸ N) :
    quotientSectionFactor N q r * quotientSectionFactor N (q * r) s =
      MulAut.conjNormal (Quotient.out q) (quotientSectionFactor N r s) *
        quotientSectionFactor N q (r * s)
def

transgressionFactor

L60 ↗
ClassFieldTower.Cohomology.transgressionFactor
Documentation

The additive factor set obtained by evaluating an invariant 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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def transgressionFactor (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (q r : P ⧸ N) : ZMod p
theorem

transgressionFactor_cocycle

L65 ↗
ClassFieldTower.Cohomology.transgressionFactor_cocycle
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionFactor_cocycle
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n)
    (q r s : P ⧸ N) :
    transgressionFactor N χ r s - transgressionFactor N χ (q * r) s +
        transgressionFactor N χ q (r * s) - transgressionFactor N χ q r = 0
def

transgressionHomogeneousCochain

L88 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCochain
Documentation

The homogeneous degree-two cochain associated to a finite 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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def transgressionHomogeneousCochain
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p))) :
    (TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).X 2
theorem

transgressionHomogeneousCochain_apply

L118 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCochain_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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCochain_apply
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (a b c : P ⧸ N) :
    (transgressionHomogeneousCochain N χ).1 a b c =
      ULift.up (transgressionFactor N χ (a⁻¹ * b) (b⁻¹ * c))
theorem

transgressionHomogeneousCochain_mem_cycles

L126 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCochain_mem_cycles
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem transgressionHomogeneousCochain_mem_cycles
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n) :
    ((TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).d 2 3).hom
        (transgressionHomogeneousCochain N χ) = 0
def

homogeneousCocycleOfElement

L164 ↗
ClassFieldTower.Cohomology.homogeneousCocycleOfElement
Documentation

Construct a continuous homogeneous cocycle from an element killed by the next differential.

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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def homogeneousCocycleOfElement
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ)
    (x : (TopRep.homogeneousCochains A).X n)
    (hx : ((TopRep.homogeneousCochains A).d n (n + 1)).hom x = 0) :
    ContinuousCohomology.cocycles A n
theorem

iCycles_homogeneousCocycleOfElement

L190 ↗
ClassFieldTower.Cohomology.iCycles_homogeneousCocycleOfElement
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem iCycles_homogeneousCocycleOfElement
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ)
    (x : (TopRep.homogeneousCochains A).X n)
    (hx : ((TopRep.homogeneousCochains A).d n (n + 1)).hom x = 0) :
    (TopRep.homogeneousCochains A).iCycles n
        (homogeneousCocycleOfElement A n x hx) = x
def

transgressionHomogeneousCocycle

L227 ↗
ClassFieldTower.Cohomology.transgressionHomogeneousCocycle
Documentation

The factor-set cochain as a continuous homogeneous degree-two cocycle.

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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def transgressionHomogeneousCocycle
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n) :
    ContinuousCohomology.cocycles
      (trivialZModPLifted (p := p) (P ⧸ N)) 2
theorem

iCycles_transgressionHomogeneousCocycle

L238 ↗
ClassFieldTower.Cohomology.iCycles_transgressionHomogeneousCocycle
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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
theorem iCycles_transgressionHomogeneousCocycle
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n) :
    (TopRep.homogeneousCochains
      (trivialZModPLifted (p := p) (P ⧸ N))).iCycles 2
        (transgressionHomogeneousCocycle N χ hχ) =
      transgressionHomogeneousCochain N χ
def

finiteTransgressionClass

L249 ↗
ClassFieldTower.Cohomology.finiteTransgressionClass
Documentation

The continuous degree-two class of the finite 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 quotientTopology (N : Subgroup P) : TopologicalSpace (P ⧸ N) := ⊥
local instance quotientDiscrete (N : Subgroup P) : DiscreteTopology (P ⧸ N) :=
  discreteTopology_bot _
Lean source · statement
def finiteTransgressionClass
    (N : Subgroup P) [N.Normal]
    (χ : MonoidHom N (Multiplicative (ZMod p)))
    (hχ : ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n) :
    continuousCohomology 2 (trivialZModPLifted (p := p) (P ⧸ N))

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