Module

ContinuousH1CupProductRestriction.lean

Nyll.GaloisCohomology.ProP.ContinuousH1CupProductRestriction

6 declarations indexed from sourceView source ↗

Module documentation

Restriction naturality of the continuous H¹ cup product

The canonical character representatives commute with pullback along a continuous group homomorphism. Consequently their degree-two cup cocycle and cohomology class commute with continuous-cohomology restriction.

Imports1

Nyll.GaloisCohomology.ProP.ContinuousH1CupProduct

Imported by2

instance

continuousH1CupRestrictionModule

L31 ↗

ClassFieldTower.Cohomology.continuousH1CupRestrictionModule

Source context 9 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J))

def

continuousH1ZModRestriction

L38 ↗

ClassFieldTower.Cohomology.continuousH1ZModRestriction

Documentation

Pullback of continuous additive mod-p characters along a continuous group homomorphism.

Source context 10 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
local instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J)) :=
  continuousH1ZModModule

Lean source · statement

def continuousH1ZModRestriction (f : H →ₜ* G) :
    ContinuousH1ZMod (p := p) (G := G) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := H)

theorem

continuousH1ZModRestriction_apply

L62 ↗

ClassFieldTower.Cohomology.continuousH1ZModRestriction_apply

Source context 10 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
local instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousH1ZModRestriction_apply
    (f : H →ₜ* G) (χ : ContinuousH1ZMod (p := p) (G := G)) (h : Additive H) :
    continuousH1ZModRestriction f χ h =
      χ (Additive.ofMul (f (Additive.toMul h)))

theorem

trivialZModPCochainsMapLifted_continuousH1Cup

L70 ↗

ClassFieldTower.Cohomology.trivialZModPCochainsMapLifted_continuousH1Cup

Documentation

Pullback of the explicit cup cochain is the cup cochain of the pulled-back characters.

Source context 10 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
local instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J)) :=
  continuousH1ZModModule

Lean source · statement

theorem trivialZModPCochainsMapLifted_continuousH1Cup
    (f : H →ₜ* G)
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    (((trivialZModPCochainsMapLifted p f).f 2).hom
        (continuousH1CupHomogeneousTwoCochainLifted χ ψ)) =
      continuousH1CupHomogeneousTwoCochainLifted
        (continuousH1ZModRestriction f χ)
        (continuousH1ZModRestriction f ψ)

theorem

trivialZModPCocyclesMapLifted_continuousH1Cup

L95 ↗

ClassFieldTower.Cohomology.trivialZModPCocyclesMapLifted_continuousH1Cup

Documentation

Restriction of the explicit cup cocycle is the cup cocycle of the restricted characters.

Source context 10 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
local instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J)) :=
  continuousH1ZModModule

Lean source · statement

theorem trivialZModPCocyclesMapLifted_continuousH1Cup
    (f : H →ₜ* G)
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    trivialZModPCocyclesMapLifted p f 2
        (continuousH1CupHomogeneousTwoCocycleLifted χ ψ) =
      continuousH1CupHomogeneousTwoCocycleLifted
        (continuousH1ZModRestriction f χ)
        (continuousH1ZModRestriction f ψ)

theorem

continuousCohomologyZModPMapLifted_continuousH1Cup

L119 ↗

ClassFieldTower.Cohomology.continuousCohomologyZModPMapLifted_continuousH1Cup

Documentation

The continuous H¹ × H¹ → H² cup product commutes with restriction.

Source context 10 commands

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

open CategoryTheory TopRep
open ClassFieldTower.ProP
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable {p : ℕ}
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
local instance continuousH1CupRestrictionModule
    {J : Type u} [Group J] [TopologicalSpace J] [IsTopologicalGroup J] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := J)) :=
  continuousH1ZModModule

Lean source · statement

theorem continuousCohomologyZModPMapLifted_continuousH1Cup
    (f : H →ₜ* G)
    (χ ψ : ContinuousH1ZMod (p := p) (G := G)) :
    (continuousCohomologyZModPMapLifted p f 2).hom
        (continuousH1CupProductLifted χ ψ) =
      continuousH1CupProductLifted
        (continuousH1ZModRestriction f χ)
        (continuousH1ZModRestriction f ψ)

Module documentation

Restriction naturality of the continuous H¹ cup product

Declarations

continuousH1CupRestrictionModule

continuousH1ZModRestriction

continuousH1ZModRestriction_apply

trivialZModPCochainsMapLifted_continuousH1Cup

trivialZModPCocyclesMapLifted_continuousH1Cup

continuousCohomologyZModPMapLifted_continuousH1Cup