Cech

📁 Source: Mathlib/CategoryTheory/Sites/SheafCohomology/Cech.lean

Statistics

Metric	Count
Definitions cochainComplexFunctor, cosimplicialObjectFunctor, cechComplexFunctor	3
Theorems cochainComplexFunctor_map_f, cochainComplexFunctor_obj_X, cochainComplexFunctor_obj_d, cosimplicialObjectFunctor_map_app, cosimplicialObjectFunctor_obj_map, cosimplicialObjectFunctor_obj_obj	6
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
cechComplexFunctor 📖	CompOp	—

CategoryTheory.Limits.FormalCoproduct

Definitions

Name	Category	Theorems
cochainComplexFunctor 📖	CompOp	3 math math: cochainComplexFunctor_map_f, cochainComplexFunctor_obj_d, cochainComplexFunctor_obj_X
cosimplicialObjectFunctor 📖	CompOp	5 math math: cosimplicialObjectFunctor_obj_obj, cochainComplexFunctor_map_f, cochainComplexFunctor_obj_d, cosimplicialObjectFunctor_obj_map, cosimplicialObjectFunctor_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cochainComplexFunctor_map_f 📖	mathematical	CategoryTheory.Limits.HasProducts	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CochainComplex HomologicalComplex.instCategory AlgebraicTopology.alternatingCofaceMapComplex CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category cosimplicialObjectFunctor CategoryTheory.Functor.map AddRightCancelSemigroup.toIsRightCancelAdd cochainComplexFunctor CategoryTheory.Limits.Pi.map I SimplexCategory SimplexCategory.smallCategory CategoryTheory.Limits.FormalCoproduct category Opposite.op obj CategoryTheory.NatTrans.app	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainComplexFunctor_obj_X 📖	mathematical	CategoryTheory.Limits.HasProducts	HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CochainComplex HomologicalComplex.instCategory cochainComplexFunctor CategoryTheory.Limits.piObj I SimplexCategory SimplexCategory.smallCategory CategoryTheory.Limits.FormalCoproduct category Opposite.op obj	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainComplexFunctor_obj_d 📖	mathematical	CategoryTheory.Limits.HasProducts	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CochainComplex HomologicalComplex.instCategory cochainComplexFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj I SimplexCategory SimplexCategory.smallCategory CategoryTheory.Limits.FormalCoproduct category Opposite.op obj CategoryTheory.CategoryStruct.comp Finset.sum AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ Fin.fintype SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Monoid.toNatPow Int.instMonoid CategoryTheory.CosimplicialObject.δ CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory cosimplicialObjectFunctor CategoryTheory.eqToHom CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
cosimplicialObjectFunctor_map_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Limits.FormalCoproduct CategoryTheory.Category.opposite category CategoryTheory.Functor.category CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.rightOp evalOp CategoryTheory.Functor.map cosimplicialObjectFunctor CategoryTheory.Limits.Pi.map I Opposite.op obj	—	—
cosimplicialObjectFunctor_obj_map 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory cosimplicialObjectFunctor CategoryTheory.Limits.Pi.lift I CategoryTheory.Limits.FormalCoproduct category Opposite.op obj CategoryTheory.Limits.piObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Hom.f Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Pi.π Hom.φ	—	—
cosimplicialObjectFunctor_obj_obj 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory cosimplicialObjectFunctor CategoryTheory.Limits.piObj I CategoryTheory.Limits.FormalCoproduct category Opposite.op obj	—	—

---

← Back to Index