NYLL
Module

FreeProPH2Cocycle.lean

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

Module documentation

Normalized cocycles and primitives for free pro-p degree-two cohomology

This helper leaf converts homogeneous degree-two cocycles with lifted trivial ZMod p coefficients into normalized inhomogeneous cocycles and constructs the homogeneous degree-one primitive associated to a continuous coboundary.

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

abbrev

A

L39 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.A
Documentation

The universe-lifted coefficient module used by the cocycle formulas.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
abbrev A (p : ℕ)
def

cocycleValue

L41 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.cocycleValue
Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
def cocycleValue
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (x₀ x₁ x₂ : F) : A p
def

normalizedCocycle

L48 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle
Documentation

The normalized inhomogeneous cocycle associated to a homogeneous degree-two cocycle.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
def normalizedCocycle
    (z : Cohomology.trivialZModPCocyclesLifted p F 2) (g h : F) : A p
theorem

normalizedCocycle_continuous

L53 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_continuous
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · full declaration
theorem normalizedCocycle_continuous
    [LocallyCompactSpace F]
    (z : Cohomology.trivialZModPCocyclesLifted p F 2) :
    Continuous fun gh : F × F => normalizedCocycle z gh.1 gh.2 := by
  let X := Cohomology.trivialZModPLifted p F
  let z₀ := ((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z
  change (TopRep.resolutionX X 3).ρ.invariants at z₀
  let zfun : C(F, C(F, C(F, A p))) := z₀.1
  change Continuous fun gh : F × F => zfun 1 gh.1 (gh.1 * gh.2) - zfun 1 1 1
  fun_prop
theorem

homogeneousCocycleEquation

L65 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousCocycleEquation
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem homogeneousCocycleEquation
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (x₀ x₁ x₂ x₃ : F) :
    (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1 x₁ x₂ x₃ -
        (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1 x₀ x₂ x₃ +
        (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1 x₀ x₁ x₃ -
      (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1 x₀ x₁ x₂ = 0
theorem

homogeneousCocycle_leftInvariant

L89 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousCocycle_leftInvariant
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem homogeneousCocycle_leftInvariant
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (g x₀ x₁ x₂ : F) :
    (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1
        (g * x₀) (g * x₁) (g * x₂) =
      (((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z).1
        x₀ x₁ x₂
theorem

normalizedCocycle_cocycle

L106 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_cocycle
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem normalizedCocycle_cocycle
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (g h k : F) :
    normalizedCocycle z g h + normalizedCocycle z (g * h) k =
      normalizedCocycle z h k + normalizedCocycle z g (h * k)
theorem

normalizedCocycle_one_left

L138 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_one_left
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem normalizedCocycle_one_left
    (z : Cohomology.trivialZModPCocyclesLifted p F 2) (h : F) :
    normalizedCocycle z 1 h = 0
theorem

normalizedCocycle_one_right

L149 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.normalizedCocycle_one_right
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem normalizedCocycle_one_right
    (z : Cohomology.trivialZModPCocyclesLifted p F 2) (g : F) :
    normalizedCocycle z g 1 = 0
theorem

homogeneousCocycle_eq_normalized

L159 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousCocycle_eq_normalized
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem homogeneousCocycle_eq_normalized
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (x₀ x₁ x₂ : F) :
    cocycleValue z x₀ x₁ x₂ = cocycleValue z 1 1 1 +
        normalizedCocycle z (x₀⁻¹ * x₁) (x₁⁻¹ * x₂)
def

homogeneousPrimitive

L174 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousPrimitive
Documentation

The homogeneous degree-one cochain associated to a continuous primitive of the normalized cocycle.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
def homogeneousPrimitive
    [LocallyCompactSpace F]
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (b : C(F, A p)) :
    (Cohomology.trivialZModPCochainsLifted p F).X 1
theorem

homogeneousPrimitive_apply

L196 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousPrimitive_apply
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem homogeneousPrimitive_apply
    [LocallyCompactSpace F]
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (b : C(F, A p)) (x y : F) :
    (((homogeneousPrimitive z b).1 : C(F, C(F, A p))) x y) =
      cocycleValue z 1 1 1 - b (x⁻¹ * y)
theorem

homogeneousPrimitive_boundary

L205 ↗
ClassFieldTower.ProP.FreeProPH2Cocycle.homogeneousPrimitive_boundary
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
namespace FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [Fact p.Prime] in
Lean source · statement
theorem homogeneousPrimitive_boundary
    [LocallyCompactSpace F]
    (z : Cohomology.trivialZModPCocyclesLifted p F 2)
    (b : C(F, A p))
    (hb : ∀ g h, b (g * h) = b g + b h + normalizedCocycle z g h) :
    ((Cohomology.trivialZModPCochainsLifted p F).d 1 2).hom
        (homogeneousPrimitive z b) =
      ((Cohomology.trivialZModPCochainsLifted p F).iCycles 2).hom z

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