NYLL
Module

ContinuousH1CupProduct.lean

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

Module documentation

The continuous cup product of two trivial mod-p characters

This file packages the explicit canonical character cup cocycle as a degree-two continuous cohomology class and as a bilinear map.

Imports2
Imported by3

Declarations

instance

continuousH1CupProductContinuousSMulULiftZMod

L30 ↗
ClassFieldTower.Cohomology.continuousH1CupProductContinuousSMulULiftZMod
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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p))
instance

continuousH1CupProductModule

L34 ↗
ClassFieldTower.Cohomology.continuousH1CupProductModule
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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

continuousH1CupHomogeneousTwoCocycleLifted

L40 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCocycleLifted
Documentation

The degree-two cocycle represented by the canonical character cup cochain.

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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1CupHomogeneousTwoCocycleLifted
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    trivialZModPCocyclesLifted p G 2
theorem

iCycles_continuousH1CupHomogeneousTwoCocycleLifted

L48 ↗
ClassFieldTower.Cohomology.iCycles_continuousH1CupHomogeneousTwoCocycleLifted
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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem iCycles_continuousH1CupHomogeneousTwoCocycleLifted
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    (trivialZModPCochainsLifted p G).iCycles 2
        (continuousH1CupHomogeneousTwoCocycleLifted χ ψ) =
      continuousH1CupHomogeneousTwoCochainLifted χ ψ
theorem

continuousH1CupHomogeneousTwoCocycleLifted_add_left

L55 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCocycleLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCocycleLifted_add_left
    (χ χ' ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCocycleLifted (χ + χ') ψ =
      continuousH1CupHomogeneousTwoCocycleLifted χ ψ +
        continuousH1CupHomogeneousTwoCocycleLifted χ' ψ
theorem

continuousH1CupHomogeneousTwoCocycleLifted_add_right

L67 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCocycleLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCocycleLifted_add_right
    (χ ψ ψ' : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCocycleLifted χ (ψ + ψ') =
      continuousH1CupHomogeneousTwoCocycleLifted χ ψ +
        continuousH1CupHomogeneousTwoCocycleLifted χ ψ'
theorem

continuousH1CupHomogeneousTwoCocycleLifted_smul_left

L79 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCocycleLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCocycleLifted_smul_left
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCocycleLifted (a • χ) ψ =
      a • continuousH1CupHomogeneousTwoCocycleLifted χ ψ
theorem

continuousH1CupHomogeneousTwoCocycleLifted_smul_right

L89 ↗
ClassFieldTower.Cohomology.continuousH1CupHomogeneousTwoCocycleLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupHomogeneousTwoCocycleLifted_smul_right
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupHomogeneousTwoCocycleLifted χ (a • ψ) =
      a • continuousH1CupHomogeneousTwoCocycleLifted χ ψ
def

continuousH1CupClassLifted

L101 ↗
ClassFieldTower.Cohomology.continuousH1CupClassLifted
Documentation

The degree-two continuous cohomology class of the canonical character cup cocycle.

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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1CupClassLifted
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousCohomologyZModPLifted p G 2
theorem

continuousH1CupClassLifted_add_left

L107 ↗
ClassFieldTower.Cohomology.continuousH1CupClassLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupClassLifted_add_left
    (χ χ' ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupClassLifted (χ + χ') ψ =
      continuousH1CupClassLifted χ ψ + continuousH1CupClassLifted χ' ψ
theorem

continuousH1CupClassLifted_add_right

L120 ↗
ClassFieldTower.Cohomology.continuousH1CupClassLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupClassLifted_add_right
    (χ ψ ψ' : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupClassLifted χ (ψ + ψ') =
      continuousH1CupClassLifted χ ψ + continuousH1CupClassLifted χ ψ'
theorem

continuousH1CupClassLifted_smul_left

L133 ↗
ClassFieldTower.Cohomology.continuousH1CupClassLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupClassLifted_smul_left
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupClassLifted (a • χ) ψ =
      a • continuousH1CupClassLifted χ ψ
theorem

continuousH1CupClassLifted_smul_right

L144 ↗
ClassFieldTower.Cohomology.continuousH1CupClassLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupClassLifted_smul_right
    (a : ZMod p) (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupClassLifted χ (a • ψ) =
      a • continuousH1CupClassLifted χ ψ
def

continuousH1CupProductLifted

L157 ↗
ClassFieldTower.Cohomology.continuousH1CupProductLifted
Documentation

The continuous cup product of two trivial mod-p degree-one classes, curried as a bilinear map into lifted degree-two cohomology.

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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1CupProductLifted :
    ContinuousH1ZMod (p := p) (G := G) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := G) →ₗ[ZMod p]
        continuousCohomologyZModPLifted p G 2
theorem

continuousH1CupProductLifted_apply

L175 ↗
ClassFieldTower.Cohomology.continuousH1CupProductLifted_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 continuousH1CupProductContinuousSMulULiftZMod :
    ContinuousSMul (ZMod p) (ULift.{u} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
local instance continuousH1CupProductModule :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1CupProductLifted_apply
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    continuousH1CupProductLifted χ ψ =
      continuousH1CupClassLifted χ ψ

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