Basic

📁 Source: Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

Statistics

Metric	Count
Definitions I, Iobj, complex, d, functor, const, continuousCohomologyZeroIso, homogeneousCochains, invariants, kerHomogeneousCochainsZeroEquiv, continuousCohomology	11
Theorems I_map_hom, I_obj_V_carrier, I_obj_V_isAddCommGroup, I_obj_V_isModule, I_obj_V_topologicalSpace, I_obj_ρ_apply, Iobj_ρ_apply, d_comp_d, d_comp_d_assoc, d_succ, d_zero, const_app_hom, instAdditiveActionTopModuleCatI, instAdditiveActionTopModuleCatInvariants, instLinearActionTopModuleCatI, instLinearActionTopModuleCatInvariants	16
Total	27

ContinuousCohomology

Definitions

Name	Category	Theorems
I 📖	CompOp	10 math math: I_obj_V_isAddCommGroup, I_obj_V_carrier, I_obj_ρ_apply, I_obj_V_isModule, I_map_hom, instLinearActionTopModuleCatI, I_obj_V_topologicalSpace, MultiInd.d_succ, const_app_hom, instAdditiveActionTopModuleCatI
Iobj 📖	CompOp	2 math math: Iobj_ρ_apply, I_map_hom
const 📖	CompOp	3 math math: MultiInd.d_succ, const_app_hom, MultiInd.d_zero
continuousCohomologyZeroIso 📖	CompOp	—
homogeneousCochains 📖	CompOp	—
invariants 📖	CompOp	2 math math: instLinearActionTopModuleCatInvariants, instAdditiveActionTopModuleCatInvariants
kerHomogeneousCochainsZeroEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
I_map_hom 📖	mathematical	—	Action.Hom.hom TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Iobj CategoryTheory.Functor.map Action Action.instCategory I TopModuleCat.ofHom ContinuousMap ModuleCat.carrier TopModuleCat.toModuleCat Action.V TopModuleCat.instTopologicalSpaceCarrier ContinuousMap.instAddCommGroupContinuousMap ModuleCat.isAddCommGroup ContinuousMap.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ContinuousMap.compactOpen ContinuousLinearMap.compLeftContinuous TopModuleCat.Hom.hom	—	—
I_obj_V_carrier 📖	mathematical	—	ModuleCat.carrier CommRing.toRing TopModuleCat.toModuleCat Action.V TopModuleCat TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory I ContinuousMap TopModuleCat.instTopologicalSpaceCarrier	—	—
I_obj_V_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup CommRing.toRing TopModuleCat.toModuleCat Action.V TopModuleCat TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory I ContinuousMap.instAddCommGroupContinuousMap ModuleCat.carrier TopModuleCat.instTopologicalSpaceCarrier	—	—
I_obj_V_isModule 📖	mathematical	—	ModuleCat.isModule CommRing.toRing TopModuleCat.toModuleCat Action.V TopModuleCat TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory I ContinuousMap.module ModuleCat.carrier TopModuleCat.instTopologicalSpaceCarrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup	—	—
I_obj_V_topologicalSpace 📖	mathematical	—	TopModuleCat.topologicalSpace CommRing.toRing Action.V TopModuleCat TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory I ContinuousMap.compactOpen ModuleCat.carrier TopModuleCat.toModuleCat TopModuleCat.instTopologicalSpaceCarrier	—	—
I_obj_ρ_apply 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End TopModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct TopModuleCat.instCategory TopModuleCat.of ContinuousMap ModuleCat.carrier TopModuleCat.toModuleCat Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid TopModuleCat.instTopologicalSpaceCarrier ContinuousMap.instAddCommGroupContinuousMap ModuleCat.isAddCommGroup ContinuousMap.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ContinuousMap.compactOpen MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ CategoryTheory.Functor.obj Action Action.instCategory I TopModuleCat.ofHom RingHom.id Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousMap.comp toContinuousMap ContinuousLinearMap TopModuleCat.topologicalSpace ContinuousLinearMap.funLike TopModuleCat.Hom.hom Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.instContinuousMapClass Homeomorph.mulLeft IsTopologicalGroup.toContinuousMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
Iobj_ρ_apply 📖	mathematical	—	DFunLike.coe ModuleCat.carrier CommRing.toRing TopModuleCat.toModuleCat Action.V TopModuleCat TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Iobj ContinuousMap.instFunLike TopModuleCat.instTopologicalSpaceCarrier ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring TopModuleCat.topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike TopModuleCat.Hom.hom MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
const_app_hom 📖	mathematical	—	Action.Hom.hom TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Functor.obj Action Action.instCategory CategoryTheory.Functor.id I CategoryTheory.NatTrans.app const TopModuleCat.ofHom ModuleCat.carrier ContinuousMap TopModuleCat.toModuleCat Action.V TopModuleCat.instTopologicalSpaceCarrier ModuleCat.isAddCommGroup ModuleCat.isModule TopModuleCat.topologicalSpace ContinuousMap.instAddCommGroupContinuousMap ContinuousMap.module Ring.toSemiring AddCommGroup.toAddCommMonoid ContinuousMap.compactOpen ContinuousLinearMap.const	—	—
instAdditiveActionTopModuleCatI 📖	mathematical	—	CategoryTheory.Functor.Additive Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.instPreadditive TopModuleCat.instPreadditive I	—	—
instAdditiveActionTopModuleCatInvariants 📖	mathematical	—	CategoryTheory.Functor.Additive Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.instPreadditive TopModuleCat.instPreadditive invariants	—	—
instLinearActionTopModuleCatI 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.instPreadditive TopModuleCat.instPreadditive Action.instLinear TopModuleCat.instLinear I	—	—
instLinearActionTopModuleCatInvariants 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Action.instPreadditive TopModuleCat.instPreadditive Action.instLinear TopModuleCat.instLinear invariants	—	—

ContinuousCohomology.MultiInd

Definitions

Name	Category	Theorems
complex 📖	CompOp	—
d 📖	CompOp	4 math math: d_comp_d_assoc, d_comp_d, d_succ, d_zero
functor 📖	CompOp	3 math math: d_comp_d_assoc, d_comp_d, d_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor Action.instPreadditive TopModuleCat.instPreadditive	—	d_succ CategoryTheory.Preadditive.comp_sub sub_eq_zero CategoryTheory.Preadditive.sub_comp CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Functor.whiskerRight_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive ContinuousCohomology.instAdditiveActionTopModuleCatI sub_zero
d_comp_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.instZeroHomFunctor Action.instPreadditive TopModuleCat.instPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_d
d_succ 📖	mathematical	—	d Quiver.Hom CategoryTheory.Functor Action TopModuleCat CommRing.toRing TopModuleCat.instCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp functor CategoryTheory.Functor.id ContinuousCohomology.I SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive Action.instPreadditive TopModuleCat.instPreadditive CategoryTheory.Functor.whiskerLeft ContinuousCohomology.const CategoryTheory.Functor.whiskerRight	—	—
d_zero 📖	mathematical	—	d ContinuousCohomology.const	—	—

(root)

Definitions

Name	Category	Theorems
continuousCohomology 📖	CompOp	—

---

← Back to Index