Module

H2CocycleExtensionSplitting.lean

Nyll.GaloisCohomology.ProP.H2CocycleExtensionSplitting

9 declarations indexed from sourceView source ↗

Module documentation

Splitting a cocycle extension whose degree-two class vanishes

A homogeneous degree-one boundary is converted to a normalized continuous inhomogeneous primitive. That primitive gives an explicit continuous group section of the associated degree-two cocycle extension. In particular, a cocycle with zero homology class has a continuous splitting.

Imports8

Nyll.GaloisCohomology.ProP.H2CentralExtensionClass
Nyll.GaloisCohomology.ProP.FiniteTransgressionKernel
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 by4

theorem

homogeneousOneCochain_leftInvariant

L42 ↗

ClassFieldTower.ProP.homogeneousOneCochain_leftInvariant

Documentation

A homogeneous degree-one cochain is invariant under simultaneous left translation.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact p.Prime] in

Lean source · statement

theorem homogeneousOneCochain_leftInvariant
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1)
    (a x y : G) :
    c.1 (a⁻¹ * x) (a⁻¹ * y) = c.1 x y

def

normalizedPrimitiveValue

L58 ↗

ClassFieldTower.ProP.normalizedPrimitiveValue

Documentation

The normalized inhomogeneous primitive extracted from a homogeneous degree-one cochain.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def normalizedPrimitiveValue
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1) :
    C(G, FreeProPH2Cocycle.A p)

theorem

normalizedPrimitiveValue_apply

L68 ↗

ClassFieldTower.ProP.normalizedPrimitiveValue_apply

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem normalizedPrimitiveValue_apply
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1)
    (g : G) :
    normalizedPrimitiveValue z c g =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 1 1 1 -
        c.1 1 g

theorem

normalizedPrimitiveValue_mul

L79 ↗

ClassFieldTower.ProP.normalizedPrimitiveValue_mul

Documentation

A homogeneous boundary gives the multiplication formula needed for a section of the associated cocycle extension.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem normalizedPrimitiveValue_mul
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1)
    (hc : ((Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom c =
      ((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z)
    (g h : G) :
    normalizedPrimitiveValue z c (g * h) =
      normalizedPrimitiveValue z c g + normalizedPrimitiveValue z c h +
        normalizedCocycle z g h

def

sectionOfBoundary

L117 ↗

ClassFieldTower.ProP.H2CocycleExtension.sectionOfBoundary

Documentation

A chosen homogeneous primitive gives a continuous section of its cocycle extension.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def H2CocycleExtension.sectionOfBoundary
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1)
    (hc : ((Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom c =
      ((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z) :
    G →ₜ* H2CocycleExtension z where
  toFun g := ⟨normalizedPrimitiveValue z c g, g⟩
  map_one' := by
    apply H2CocycleExtension.ext
    · change normalizedPrimitiveValue z c 1 = 0
      have hb := normalizedPrimitiveValue_mul z c hc 1 1
      rw [one_mul, normalizedCocycle_one_left] at hb
      apply add_left_cancel (a := normalizedPrimitiveValue z c 1)
      calc
        normalizedPrimitiveValue z c 1 + normalizedPrimitiveValue z c 1 =
            normalizedPrimitiveValue z c 1 + normalizedPrimitiveValue z c 1 + 0 :=
          (add_zero _).symm
        _ = normalizedPrimitiveValue z c 1 := hb.symm
        _ = normalizedPrimitiveValue z c 1 + 0 := (add_zero _).symm
    · rfl
  map_mul' g h := by
    apply H2CocycleExtension.ext
    · exact normalizedPrimitiveValue_mul z c hc g h
    · rfl
  continuous_toFun := by
    rw [continuous_induced_rng]
    exact (normalizedPrimitiveValue z c).continuous.prodMk continuous_id

theorem

projection_comp_sectionOfBoundary

L147 ↗

ClassFieldTower.ProP.H2CocycleExtension.projection_comp_sectionOfBoundary

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem H2CocycleExtension.projection_comp_sectionOfBoundary
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (c : (Cohomology.trivialZModPCochainsLifted p G).X 1)
    (hc : ((Cohomology.trivialZModPCochainsLifted p G).d 1 2).hom c =
      ((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z) :
    (H2CocycleExtension.projection z).comp
        (H2CocycleExtension.sectionOfBoundary z c hc) =
      ContinuousMonoidHom.id G

theorem

exists_section_of_π_eq_zero

L159 ↗

ClassFieldTower.ProP.H2CocycleExtension.exists_section_of_π_eq_zero

Documentation

A degree-two cocycle with zero homology class has a continuous splitting.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem H2CocycleExtension.exists_section_of_π_eq_zero
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (hz : ContinuousCohomology.π
      (Cohomology.trivialZModPLifted p G) 2 z = 0) :
    ∃ s : G →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s =
        ContinuousMonoidHom.id G

theorem

π_eq_zero_of_section

L174 ↗

ClassFieldTower.ProP.H2CocycleExtension.π_eq_zero_of_section

Documentation

Conversely, a continuous section of a cocycle extension makes the represented degree-two class vanish.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem H2CocycleExtension.π_eq_zero_of_section
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (s : G →ₜ* H2CocycleExtension z)
    (hs : (H2CocycleExtension.projection z).comp s =
      ContinuousMonoidHom.id G) :
    ContinuousCohomology.π
      (Cohomology.trivialZModPLifted p G) 2 z = 0

theorem

exists_section_iff_π_eq_zero

L216 ↗

ClassFieldTower.ProP.H2CocycleExtension.exists_section_iff_π_eq_zero

Documentation

A degree-two cocycle extension splits continuously exactly when its represented class vanishes.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation
open FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem H2CocycleExtension.exists_section_iff_π_eq_zero
    [LocallyCompactSpace G]
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) :
    (∃ s : G →ₜ* H2CocycleExtension z,
      (H2CocycleExtension.projection z).comp s =
        ContinuousMonoidHom.id G) ↔
      ContinuousCohomology.π
        (Cohomology.trivialZModPLifted p G) 2 z = 0

Module documentation

Splitting a cocycle extension whose degree-two class vanishes

Declarations