Mathlib Map

Theorems · Definition · group theory

TopRep.homogeneousCochains

{k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → CochainComplex (TopModuleCat k) ℕ

The homogeneous cochains of a topological representation.

Defined in
Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
Cited by
13 results in Mathlib
Foundations
Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RingGroupTopologicalSpaceTopologicalSpaceIsTopologicalGroup

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContinuousCohomology.cochainsMap · cited by 8ContinuousCohomology.coch…ContinuousCohomology.cocycles · cited by 5ContinuousCohomology.cocy…continuousCohomology · cited by 5continuousCohomologyContinuousCohomology.cochainsMap_id · cited by 2ContinuousCohomology.coch…ContinuousCohomology.π · cited by 2ContinuousCohomology.πTopRep.homogeneousCochains.d_apply · cited by 2homogeneousCochains.d_app…ContinuousCohomology.cochainsMap_comp · cited by 1ContinuousCohomology.coch…ContinuousCohomology.cochainsMap_f · cited by 1ContinuousCohomology.coch…ContinuousCohomology.π_map · cited by 1ContinuousCohomology.π_mapTopRep.homogeneousCochains.d_eq · cited by 1homogeneousCochains.d_eqContinuousCohomology.cochainsMap_comp_assoc · cited by 0ContinuousCohomology.coch…ContinuousCohomology.cochainsMap_f_hom · cited by 0ContinuousCohomology.coch…ContinuousCohomology.cocyclesMap_id · cited by 0ContinuousCohomology.cocy…ContinuousCohomology.cocycles₀Iso · cited by 0ContinuousCohomology.cocy…ContinuousCohomology.cocycles₀IsoAux · cited by 0ContinuousCohomology.cocy…TopologicalSpace · cited by 24529TopologicalSpaceCategoryTheory.Functor.obj · cited by 19642Functor.objRing · cited by 7463RingGroup · cited by 6238GroupComplexShape.up · cited by 1123ComplexShape.upCochainComplex · cited by 1016CochainComplexIsTopologicalGroup · cited by 469IsTopologicalGroupCategoryTheory.Functor.mapHomologicalComplex · cited by 145Functor.mapHomologicalCom…TopRep · cited by 54TopRepTopModuleCat · cited by 45TopModuleCatTopRep.resolution' · cited by 7TopRep.resolution'TopRep.invariantsFunctor · cited by 3TopRep.invariantsFunctorTopRep.homogeneousCochainsCITED BYCITES

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.