ModuleContinuousCohomologyRepresentatives.lean
Nyll.GaloisCohomology.Topology.ContinuousCohomologyRepresentatives
2 declarations indexed from sourceView source ↗ Module documentation
Representatives and boundaries in continuous cohomology
The cocycle projection is surjective as a function, and its kernel consists of boundaries. These are statements about the actual topological homology objects, with no exactness assumptions on a coefficient sequence.
Imports2
- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Imported by3
Declarations
ContinuousCohomology.π_surjective
DocumentationEvery continuous cohomology class has a homogeneous cocycle representative.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
namespace ContinuousCohomology
universe u v
variable {R : Type u} [Ring R] [TopologicalSpace R]
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
ContinuousCohomology.exists_boundary_of_π_eq_zero
DocumentationA homogeneous cocycle whose cohomology class is zero is a boundary.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory CategoryTheory.Limits
namespace ContinuousCohomology
universe u v
variable {R : Type u} [Ring R] [TopologicalSpace R]
variable {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]