CechNerve

📁 Source: Mathlib/AlgebraicTopology/CechNerve.lean

Statistics

Metric	Count
Definitions augmentedCechConerve, augmentedCechNerve, cechConerve, cechNerve, mapAugmentedCechConerve, mapAugmentedCechNerve, mapCechConerve, mapCechNerve, iso, uniqueToWideCospanNone, wideCospan, limitCone, limitIsoPi, augmentedCechConerve, cechConerve, cechConerveAdjunction, cechConerveEquiv, equivalenceLeftToRight, equivalenceRightToLeft, augmentedCechNerve, cechNerve, cechNerveAdjunction, cechNerveEquiv, equivalenceLeftToRight, equivalenceRightToLeft, cechNerveTerminalFrom	26
Theorems augmentedCechConerve_hom_app, augmentedCechConerve_left, augmentedCechConerve_right, augmentedCechNerve_hom_app, augmentedCechNerve_left, augmentedCechNerve_right, cechConerve_map, cechConerve_obj, cechNerve_map, cechNerve_obj, mapAugmentedCechConerve_left, mapAugmentedCechConerve_right, mapAugmentedCechNerve_left, mapAugmentedCechNerve_right, mapCechConerve_app, mapCechNerve_app, hasLimit_wideCospan, hasWidePullback, hasWidePullback', limitIsoPi_hom_comp_pi, limitIsoPi_hom_comp_pi_assoc, limitIsoPi_inv_comp_pi, limitIsoPi_inv_comp_pi_assoc, augmentedCechConerve_map, augmentedCechConerve_obj, cechConerveEquiv_apply, cechConerveEquiv_symm_apply, cechConerve_map, cechConerve_obj, equivalenceLeftToRight_left, equivalenceLeftToRight_right, equivalenceRightToLeft_left, equivalenceRightToLeft_right_app, augmentedCechNerve_map_left_app, augmentedCechNerve_map_right, augmentedCechNerve_obj_hom_app, augmentedCechNerve_obj_left_map, augmentedCechNerve_obj_left_obj, augmentedCechNerve_obj_right, cechNerveEquiv_apply, cechNerveEquiv_symm_apply, cechNerve_map, cechNerve_obj, equivalenceLeftToRight_left_app, equivalenceLeftToRight_right, equivalenceRightToLeft_left, equivalenceRightToLeft_right	47
Total	73

CategoryTheory

Definitions

Name	Category	Theorems
cechNerveTerminalFrom 📖	CompOp	—

CategoryTheory.Arrow

Definitions

Name	Category	Theorems
augmentedCechConerve 📖	CompOp	12 math math: mapAugmentedCechConerve_right, CategoryTheory.CosimplicialObject.cechConerveEquiv_symm_apply, CategoryTheory.CosimplicialObject.augmentedCechConerve_obj, mapAugmentedCechConerve_left, augmentedCechConerve_right, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_left, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_left, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, CategoryTheory.CosimplicialObject.cechConerveEquiv_apply, augmentedCechConerve_left, augmentedCechConerve_hom_app
augmentedCechNerve 📖	CompOp	13 math math: augmentedCechNerve_hom_app, mapAugmentedCechNerve_left, augmentedCechNerve_left, CategoryTheory.SimplicialObject.equivalenceRightToLeft_right, augmentedCechNerve_right, CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, CategoryTheory.SimplicialObject.cechNerveEquiv_apply, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_map_right, mapAugmentedCechNerve_right, CategoryTheory.SimplicialObject.equivalenceLeftToRight_right
cechConerve 📖	CompOp	6 math math: mapCechConerve_app, augmentedCechConerve_right, cechConerve_map, cechConerve_obj, CategoryTheory.CosimplicialObject.cechConerve_obj, augmentedCechConerve_hom_app
cechNerve 📖	CompOp	11 math math: augmentedCechNerve_hom_app, mapCechNerve_app, AugmentedCechNerve.ExtraDegeneracy.s_comp_base, cechNerve_obj, augmentedCechNerve_left, CategoryTheory.SimplicialObject.cechNerve_obj, AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0, AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ, cechNerve_map, CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app
mapAugmentedCechConerve 📖	CompOp	3 math math: mapAugmentedCechConerve_right, mapAugmentedCechConerve_left, CategoryTheory.CosimplicialObject.augmentedCechConerve_map
mapAugmentedCechNerve 📖	CompOp	2 math math: mapAugmentedCechNerve_left, mapAugmentedCechNerve_right
mapCechConerve 📖	CompOp	3 math math: mapAugmentedCechConerve_right, mapCechConerve_app, CategoryTheory.CosimplicialObject.cechConerve_map
mapCechNerve 📖	CompOp	3 math math: mapCechNerve_app, mapAugmentedCechNerve_left, CategoryTheory.SimplicialObject.cechNerve_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
augmentedCechConerve_hom_app 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const cechConerve augmentedCechConerve CategoryTheory.Limits.WidePushout.head SimplexCategory.len	—	—
augmentedCechConerve_left 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const augmentedCechConerve	—	—
augmentedCechConerve_right 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const augmentedCechConerve cechConerve	—	—
augmentedCechNerve_hom_app 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject cechNerve CategoryTheory.SimplicialObject.const augmentedCechNerve CategoryTheory.Limits.WidePullback.base SimplexCategory.len Opposite.unop	—	—
augmentedCechNerve_left 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const augmentedCechNerve cechNerve	—	—
augmentedCechNerve_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const augmentedCechNerve	—	—
cechConerve_map 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory cechConerve CategoryTheory.Limits.WidePushout.desc SimplexCategory.len CategoryTheory.Limits.widePushout CategoryTheory.Limits.WidePushout.head CategoryTheory.Limits.WidePushout.ι CategoryTheory.Functor.obj DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom	—	—
cechConerve_obj 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory cechConerve CategoryTheory.Limits.widePushout SimplexCategory.len	—	—
cechNerve_map 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory cechNerve CategoryTheory.Limits.WidePullback.lift SimplexCategory.len Opposite.unop CategoryTheory.Limits.widePullback CategoryTheory.Limits.WidePullback.base CategoryTheory.Limits.WidePullback.π DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
cechNerve_obj 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory cechNerve CategoryTheory.Limits.widePullback SimplexCategory.len Opposite.unop	—	—
mapAugmentedCechConerve_left 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const augmentedCechConerve mapAugmentedCechConerve	—	—
mapAugmentedCechConerve_right 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const augmentedCechConerve mapAugmentedCechConerve mapCechConerve	—	—
mapAugmentedCechNerve_left 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const augmentedCechNerve mapAugmentedCechNerve mapCechNerve	—	—
mapAugmentedCechNerve_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const augmentedCechNerve mapAugmentedCechNerve	—	—
mapCechConerve_app 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory cechConerve mapCechConerve CategoryTheory.Limits.WidePushout.desc SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.left CategoryTheory.Limits.WidePushout.head CategoryTheory.CommaMorphism.right CategoryTheory.Limits.WidePushout.ι	—	—
mapCechNerve_app 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory cechNerve mapCechNerve CategoryTheory.Limits.WidePullback.lift SimplexCategory.len Opposite.unop CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.WidePullback.base CategoryTheory.CommaMorphism.right CategoryTheory.Limits.WidePullback.π CategoryTheory.CommaMorphism.left	—	—

CategoryTheory.CechNerveTerminalFrom

Definitions

Name	Category	Theorems
iso 📖	CompOp	—
uniqueToWideCospanNone 📖	CompOp	—
wideCospan 📖	CompOp	5 math math: hasLimit_wideCospan, wideCospan.limitIsoPi_inv_comp_pi, wideCospan.limitIsoPi_hom_comp_pi_assoc, wideCospan.limitIsoPi_inv_comp_pi_assoc, wideCospan.limitIsoPi_hom_comp_pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit_wideCospan 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category wideCospan	—	hasWidePullback
hasWidePullback 📖	mathematical	—	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	nonempty_fintype
hasWidePullback' 📖	mathematical	—	CategoryTheory.Limits.HasWidePullback CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from	—	hasWidePullback

CategoryTheory.CechNerveTerminalFrom.wideCospan

Definitions

Name	Category	Theorems
limitCone 📖	CompOp	—
limitIsoPi 📖	CompOp	4 math math: limitIsoPi_inv_comp_pi, limitIsoPi_hom_comp_pi_assoc, limitIsoPi_inv_comp_pi_assoc, limitIsoPi_hom_comp_pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
limitIsoPi_hom_comp_pi 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.CechNerveTerminalFrom.wideCospan CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Limits.piObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Discrete.functor CategoryTheory.Iso.hom limitIsoPi CategoryTheory.Limits.Pi.π CategoryTheory.Limits.WidePullback.π CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from	—	CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete limitIsoPi_inv_comp_pi CategoryTheory.Iso.hom_inv_id_assoc
limitIsoPi_hom_comp_pi_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.CechNerveTerminalFrom.wideCospan CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Limits.piObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Discrete.functor CategoryTheory.Iso.hom limitIsoPi CategoryTheory.Limits.Pi.π CategoryTheory.Limits.WidePullback.π CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from	—	CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoPi_hom_comp_pi
limitIsoPi_inv_comp_pi 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Discrete.functor CategoryTheory.Limits.limit CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.CechNerveTerminalFrom.wideCospan CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Iso.inv limitIsoPi CategoryTheory.Limits.WidePullback.π CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.Limits.Pi.π	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan
limitIsoPi_inv_comp_pi_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.piObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Discrete.functor CategoryTheory.Limits.limit CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.CechNerveTerminalFrom.wideCospan CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Iso.inv limitIsoPi CategoryTheory.Limits.WidePullback.π CategoryTheory.Limits.terminal CategoryTheory.Limits.terminal.from CategoryTheory.Limits.Pi.π	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CechNerveTerminalFrom.hasLimit_wideCospan CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitIsoPi_inv_comp_pi

CategoryTheory.CosimplicialObject

Definitions

Name	Category	Theorems
augmentedCechConerve 📖	CompOp	2 math math: augmentedCechConerve_obj, augmentedCechConerve_map
cechConerve 📖	CompOp	2 math math: cechConerve_map, cechConerve_obj
cechConerveAdjunction 📖	CompOp	—
cechConerveEquiv 📖	CompOp	2 math math: cechConerveEquiv_symm_apply, cechConerveEquiv_apply
equivalenceLeftToRight 📖	CompOp	3 math math: equivalenceLeftToRight_left, equivalenceLeftToRight_right, cechConerveEquiv_apply
equivalenceRightToLeft 📖	CompOp	3 math math: cechConerveEquiv_symm_apply, equivalenceRightToLeft_right_app, equivalenceRightToLeft_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
augmentedCechConerve_map 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechConerve CategoryTheory.Arrow.mapAugmentedCechConerve	—	—
augmentedCechConerve_obj 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechConerve CategoryTheory.Arrow.augmentedCechConerve	—	—
cechConerveEquiv_apply 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	DFunLike.coe Equiv Quiver.Hom Augmented CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Arrow.augmentedCechConerve CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Augmented.toArrow EquivLike.toFunLike Equiv.instEquivLike cechConerveEquiv equivalenceLeftToRight	—	—
cechConerveEquiv_symm_apply 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Arrow CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Augmented instCategoryAugmented Augmented.toArrow CategoryTheory.Arrow.augmentedCechConerve EquivLike.toFunLike Equiv.instEquivLike Equiv.symm cechConerveEquiv equivalenceRightToLeft	—	—
cechConerve_map 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.CosimplicialObject instCategory cechConerve CategoryTheory.Arrow.mapCechConerve	—	—
cechConerve_obj 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.CosimplicialObject instCategory cechConerve CategoryTheory.Arrow.cechConerve	—	—
equivalenceLeftToRight_left 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow equivalenceLeftToRight CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Arrow.augmentedCechConerve	—	—
equivalenceLeftToRight_right 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow equivalenceLeftToRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.widePushout SimplexCategory.len SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Limits.WidePushout.ι SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat CategoryTheory.NatTrans.app CategoryTheory.Arrow.augmentedCechConerve	—	—
equivalenceRightToLeft_left 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Arrow.augmentedCechConerve equivalenceRightToLeft CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow	—	—
equivalenceRightToLeft_right_app 📖	mathematical	CategoryTheory.Limits.HasWidePushout CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Arrow.augmentedCechConerve CategoryTheory.CommaMorphism.right equivalenceRightToLeft CategoryTheory.Limits.WidePushout.desc SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.left Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow CategoryTheory.Functor.map SimplexCategory.const	—	—

CategoryTheory.SimplicialObject

Definitions

Name	Category	Theorems
augmentedCechNerve 📖	CompOp	6 math math: augmentedCechNerve_obj_right, augmentedCechNerve_map_left_app, augmentedCechNerve_obj_left_map, augmentedCechNerve_obj_left_obj, augmentedCechNerve_obj_hom_app, augmentedCechNerve_map_right
cechNerve 📖	CompOp	2 math math: cechNerve_obj, cechNerve_map
cechNerveAdjunction 📖	CompOp	—
cechNerveEquiv 📖	CompOp	2 math math: cechNerveEquiv_symm_apply, cechNerveEquiv_apply
equivalenceLeftToRight 📖	CompOp	3 math math: cechNerveEquiv_apply, equivalenceLeftToRight_left_app, equivalenceLeftToRight_right
equivalenceRightToLeft 📖	CompOp	3 math math: equivalenceRightToLeft_right, cechNerveEquiv_symm_apply, equivalenceRightToLeft_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
augmentedCechNerve_map_left_app 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Arrow.cechNerve CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve CategoryTheory.Limits.WidePullback.lift SimplexCategory.len Opposite.unop CategoryTheory.Limits.widePullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.WidePullback.base CategoryTheory.CommaMorphism.right CategoryTheory.Limits.WidePullback.π	—	—
augmentedCechNerve_map_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve	—	—
augmentedCechNerve_obj_hom_app 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Arrow.cechNerve const CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve CategoryTheory.Limits.WidePullback.base SimplexCategory.len Opposite.unop	—	—
augmentedCechNerve_obj_left_map 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve CategoryTheory.Limits.WidePullback.lift SimplexCategory.len Opposite.unop CategoryTheory.Limits.widePullback CategoryTheory.Limits.WidePullback.base CategoryTheory.Limits.WidePullback.π DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
augmentedCechNerve_obj_left_obj 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve CategoryTheory.Limits.widePullback SimplexCategory.len Opposite.unop	—	—
augmentedCechNerve_obj_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented instCategoryAugmented augmentedCechNerve	—	—
cechNerveEquiv_apply 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Arrow CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Augmented instCategoryAugmented Augmented.toArrow CategoryTheory.Arrow.augmentedCechNerve EquivLike.toFunLike Equiv.instEquivLike cechNerveEquiv equivalenceLeftToRight	—	—
cechNerveEquiv_symm_apply 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	DFunLike.coe Equiv Quiver.Hom Augmented CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Arrow.augmentedCechNerve CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj Augmented.toArrow EquivLike.toFunLike Equiv.instEquivLike Equiv.symm cechNerveEquiv equivalenceRightToLeft	—	—
cechNerve_map 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject cechNerve CategoryTheory.Arrow.mapCechNerve	—	—
cechNerve_obj 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject cechNerve CategoryTheory.Arrow.cechNerve	—	—
equivalenceLeftToRight_left_app 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve CategoryTheory.CommaMorphism.left equivalenceLeftToRight CategoryTheory.Limits.WidePullback.lift SimplexCategory.len Opposite.unop CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver SimplexCategory.const	—	—
equivalenceLeftToRight_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve equivalenceLeftToRight CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow	—	—
equivalenceRightToLeft_left 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow equivalenceRightToLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Limits.WidePullback.π SimplexCategory.len Opposite.unop SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	—	—
equivalenceRightToLeft_right 📖	mathematical	CategoryTheory.Limits.HasWidePullback CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.obj Augmented instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow Augmented.toArrow equivalenceRightToLeft CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject const CategoryTheory.Arrow.augmentedCechNerve	—	—

---

← Back to Index