NYLL
Module

ContinuousH1CupCochain.lean

Nyll.GaloisCohomology.ProP.ContinuousH1CupCochain
9 declarations indexed from sourceView source ↗

Module documentation

The continuous cup product of two trivial mod-p characters

For continuous additive ZMod p-characters, the canonical homogeneous representatives give the degree-two cochain

(g, h, k) ↦ χ(g⁻¹h) * ψ(h⁻¹k).

This file constructs that cochain directly and proves its cocycle equation. No choice of cocycle representatives is involved.

Imports2
Imported by2

Declarations

instance

continuousH1CupContinuousSMulULiftZMod

L35 ↗
ClassFieldTower.Cohomology.continuousH1CupContinuousSMulULiftZMod
Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p))
instance

continuousH1CupModule

L39 ↗
ClassFieldTower.Cohomology.continuousH1CupModule
Source context 9 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

continuousH1CupHomogeneousTwoCochainLifted

L45 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted
Documentation

The homogeneous degree-two cochain underlying the cup of two canonical continuous degree-one character cocycles.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1CupHomogeneousTwoCochainLifted
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    (trivialZModPCochainsLifted p G).X 2
theorem

continuousH1CupHomogeneousTwoCochainLifted_apply

L79 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_apply
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_apply
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) (g h k : G) :
    (continuousH1CupHomogeneousTwoCochainLifted χ ψ).1 g h k =
      ULift.up
        (χ (Additive.ofMul (g⁻¹ * h)) *
          ψ (Additive.ofMul (h⁻¹ * k)))
theorem

continuousH1CupHomogeneousTwoCochainLifted_mem_cycles

L89 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_mem_cycles
Documentation

The canonical degree-two cup cochain satisfies the homogeneous cocycle equation.

Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_mem_cycles
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    ((trivialZModPCochainsLifted p G).d 2 3).hom
        (continuousH1CupHomogeneousTwoCochainLifted χ ψ) = 0
theorem

continuousH1CupHomogeneousTwoCochainLifted_add_left

L138 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_add_left
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_add_left
    (χ χ' ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCochainLifted (χ + χ') ψ =
      continuousH1CupHomogeneousTwoCochainLifted χ ψ +
        continuousH1CupHomogeneousTwoCochainLifted χ' ψ
theorem

continuousH1CupHomogeneousTwoCochainLifted_add_right

L163 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_add_right
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_add_right
    (χ ψ ψ' : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCochainLifted χ (ψ + ψ') =
      continuousH1CupHomogeneousTwoCochainLifted χ ψ +
        continuousH1CupHomogeneousTwoCochainLifted χ ψ'
theorem

continuousH1CupHomogeneousTwoCochainLifted_smul_left

L188 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_smul_left
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_smul_left
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCochainLifted (a • χ) ψ =
      a • continuousH1CupHomogeneousTwoCochainLifted χ ψ
theorem

continuousH1CupHomogeneousTwoCochainLifted_smul_right

L215 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCochainLifted_smul_right
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open ClassFieldTower.ProP
open scoped Topology
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousH1CupContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCochainLifted_smul_right
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCochainLifted χ (a • ψ) =
      a • continuousH1CupHomogeneousTwoCochainLifted χ ψ

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