Module

ContinuousCrossedHom.lean

Nyll.GaloisCohomology.Topology.ContinuousCrossedHom

13 declarations indexed from sourceView source ↗

Module documentation

Continuous crossed homomorphisms and homogeneous one-cocycles

Imports1

Nyll.GaloisCohomology.Topology.ContinuousCohomologyRepresentatives

Imported by2

structure

CrossedHom

L21 ↗

ContinuousCohomology.CrossedHom

Documentation

A continuous crossed homomorphism for a topological integral representation.

Source context 5 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

structure CrossedHom (X : TopRep.{u} ℤ G) where
  /-- The function giving the crossed-homomorphism values. -/
  toFun : G → X
  /-- Continuity of the crossed-homomorphism value function. -/
  continuous_toFun : Continuous toFun
  /-- The crossed-homomorphism identity for the given representation action. -/
  map_mul : ∀ g h, toFun (g * h) = toFun g + X.ρ g (toFun h)

theorem

map_one

L34 ↗

ContinuousCohomology.CrossedHom.map_one

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem map_one (c : CrossedHom X) : c.toFun 1 = 0

def

homogeneous

L40 ↗

ContinuousCohomology.CrossedHom.homogeneous

Documentation

The homogeneous cocycle is the difference of the two inhomogeneous values.

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}

Lean source · statement

def homogeneous (c : CrossedHom X) : (homogeneousCochains X).X 1

theorem

homogeneous_apply

L56 ↗

ContinuousCohomology.CrossedHom.homogeneous_apply

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}

Lean source · statement

theorem homogeneous_apply (c : CrossedHom X) (g h : G) :
    c.homogeneous.1 g h = c.toFun h - c.toFun g

theorem

homogeneous_mem_cycles

L59 ↗

ContinuousCohomology.CrossedHom.homogeneous_mem_cycles

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}

Lean source · statement

theorem homogeneous_mem_cycles (c : CrossedHom X) :
    ((homogeneousCochains X).d 1 2).hom c.homogeneous = 0

instance

(anonymous instance)

L73 ↗

Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}

Lean source · statement

instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R)

def

scalarLine

L76 ↗

ContinuousCohomology.CrossedHom.scalarLine

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
local instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R) := ⟨continuous_of_discreteTopology⟩

Lean source · statement

def scalarLine {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R]
    {M : TopModuleCat.{u} R} (x : M) :
    TopModuleCat.of R (ULift.{u} R) ⟶ M

theorem

scalarLine_one

L86 ↗

ContinuousCohomology.CrossedHom.scalarLine_one

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
local instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R) := ⟨continuous_of_discreteTopology⟩

Lean source · statement

theorem scalarLine_one {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R]
    {M : TopModuleCat.{u} R} (x : M) : scalarLine x (ULift.up 1) = x

theorem

scalarLine_comp_eq_zero

L90 ↗

ContinuousCohomology.CrossedHom.scalarLine_comp_eq_zero

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
local instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R) := ⟨continuous_of_discreteTopology⟩

Lean source · statement

theorem scalarLine_comp_eq_zero
    {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R]
    {M N : TopModuleCat.{u} R} (x : M) (f : M ⟶ N) (hx : f.hom x = 0) :
    scalarLine x ≫ f = 0

def

toCocycle

L99 ↗

ContinuousCohomology.CrossedHom.toCocycle

Documentation

A crossed homomorphism determines an actual homogeneous one-cocycle.

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
local instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R) := ⟨continuous_of_discreteTopology⟩

Lean source · statement

def toCocycle (c : CrossedHom X) : cocycles X 1

theorem

iCycles_toCocycle

L105 ↗

ContinuousCohomology.CrossedHom.iCycles_toCocycle

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace CrossedHom
variable {X : TopRep.{u} ℤ G}
local instance {R : Type} [Ring R] [TopologicalSpace R] [DiscreteTopology R] :
    ContinuousSMul R (ULift.{u} R) := ⟨continuous_of_discreteTopology⟩

Lean source · statement

theorem iCycles_toCocycle (c : CrossedHom X) :
    (homogeneousCochains X).iCycles 1 c.toCocycle = c.homogeneous

def

crossedHomOfCocycle

L116 ↗

ContinuousCohomology.crossedHomOfCocycle

Documentation

Dehomogenization of a homogeneous one-cocycle.

Source context 5 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def crossedHomOfCocycle (X : TopRep.{u} ℤ G) (z : cocycles X 1) :
    CrossedHom X

theorem

crossedHomOfCocycle_toCocycle

L140 ↗

ContinuousCohomology.crossedHomOfCocycle_toCocycle

Source context 5 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ContinuousCohomology
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem crossedHomOfCocycle_toCocycle (X : TopRep.{u} ℤ G) (c : CrossedHom X) (g : G) :
    (crossedHomOfCocycle X c.toCocycle).toFun g = c.toFun g

Module documentation

Continuous crossed homomorphisms and homogeneous one-cocycles

Declarations