Module

FiniteCohomology.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.FiniteCohomology

2 declarations indexed from sourceView source ↗

Module documentation

Concrete finite cocycles and the actual continuous H¹ reduction

Imports3

Imported by3

def

finiteCocycleCrossedHom

L20 ↗

Yamaguchi26AbfaithfulGalois.finiteCocycleCrossedHom

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
variable {ℓ : ℕ} [Fact ℓ.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def finiteCocycleCrossedHom (θ : Orientation ℓ G) (H : Subgroup G)
    (n : ℕ) (c : FiniteCocycle θ H n) :
    ContinuousCohomology.CrossedHom (finiteOrientationTopRep θ H n) where
  toFun := fun g => ULift.up (c.toFun g)
  continuous_toFun := continuous_uliftUp.comp c.continuous_toFun
  map_mul := by
    intro g h
    rw [finiteOrientationTopRep_action]
    exact ULift.ext (c.cocycle g h)

theorem

finiteCocycle_lift_mod_one_of_h1

L32 ↗

Yamaguchi26AbfaithfulGalois.finiteCocycle_lift_mod_one_of_h1

Documentation

Surjectivity on the genuine H¹ map gives exact lifts of finite cocycles modulo ℓ; the lifted cohomology class is corrected by a principal cocycle.