NYLL
Module

ContinuousH1CocycleSurjectivity.lean

Nyll.GaloisCohomology.Topology.ContinuousH1CocycleSurjectivity
2 declarations indexed from sourceView source ↗

Module documentation

Cocycle lifting implies surjectivity on actual continuous H¹

Imports1
Imported by2

Declarations

theorem

homogeneous_oneCocycle_eq_difference

L19 ↗
ContinuousCohomology.homogeneous_oneCocycle_eq_difference
Source context 4 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem homogeneous_oneCocycle_eq_difference
    (X : TopRep.{u} ℤ G) (z : cocycles X 1) (g h : G) :
    ((homogeneousCochains X).iCycles 1 z).1 g h =
      (crossedHomOfCocycle X z).toFun h - (crossedHomOfCocycle X z).toFun g
theorem

map_surjective_of_crossedHom_lifting

L36 ↗
ContinuousCohomology.map_surjective_of_crossedHom_lifting
Documentation

Exact lifting of all continuous crossed homomorphisms gives a surjection on H¹.

Source context 4 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem map_surjective_of_crossedHom_lifting
    (X Y : TopRep.{u} ℤ G)
    (f : TopRep.res (ContinuousMonoidHom.id G) X ⟶ Y)
    (hlift : ∀ c : CrossedHom Y, ∃ d : CrossedHom X,
      ∀ g : G, f.hom (d.toFun g) = c.toFun g) :
    Function.Surjective (map (ContinuousMonoidHom.id G) f 1).hom

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