SimplicialNerve

📁 Source: Mathlib/AlgebraicTopology/SimplicialNerve.lean

Statistics

Metric	Count
Definitions SimplicialNerve, SimplicialThickening, I, comp, id, as, compFunctor, functor, functorMap, instCategory, instCategoryHom, instCategoryPath, instCategoryStruct, instSimplicialCategory, orderHom	15
Theorems ext, ext_iff, le, le_right, left, left_le, right, assoc, comp_id, id_comp, compFunctor_obj, comp_I, functor_comp, functor_id, functor_map, functor_obj_as, hom_ext, hom_ext_iff, id_I	19
Total	34

CategoryTheory

Definitions

Name	Category	Theorems
SimplicialNerve 📖	CompOp	—
SimplicialThickening 📖	CompData	7 math math: SimplicialThickening.compFunctor_obj, SimplicialThickening.functor_map, SimplicialThickening.functor_id, SimplicialThickening.functor_obj_as, SimplicialThickening.functor_comp, SimplicialThickening.comp_I, SimplicialThickening.id_I

CategoryTheory.SimplicialThickening

Definitions

Name	Category	Theorems
as 📖	CompOp	5 math math: hom_ext_iff, functor_map, functor_obj_as, comp_I, id_I
compFunctor 📖	CompOp	1 math math: compFunctor_obj
functor 📖	CompOp	4 math math: functor_map, functor_id, functor_obj_as, functor_comp
functorMap 📖	CompOp	1 math math: functor_map
instCategory 📖	CompOp	4 math math: functor_map, functor_id, functor_obj_as, functor_comp
instCategoryHom 📖	CompOp	2 math math: compFunctor_obj, functor_map
instCategoryPath 📖	CompOp	—
instCategoryStruct 📖	CompOp	4 math math: compFunctor_obj, functor_map, comp_I, id_I
instSimplicialCategory 📖	CompOp	4 math math: functor_map, functor_id, functor_obj_as, functor_comp
orderHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Quiver.Hom CategoryTheory.SimplicialThickening CategoryTheory.CategoryStruct.toQuiver instCategoryStruct CategoryTheory.uniformProd instCategoryHom compFunctor CategoryTheory.CategoryStruct.comp	—	—
comp_I 📖	mathematical	—	Path.I as CategoryTheory.CategoryStruct.comp CategoryTheory.SimplicialThickening instCategoryStruct Set Set.instUnion	—	—
functor_comp 📖	mathematical	—	functor OrderHom.comp PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder CategoryTheory.EnrichedFunctor.comp SSet SSet.largeCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.SimplicialThickening CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory instCategory instSimplicialCategory	—	CategoryTheory.EnrichedFunctor.ext SSet.hom_ext CategoryTheory.types_ext CategoryTheory.Functor.ext Set.image_congr CategoryTheory.Category.comp_id hom_ext
functor_id 📖	mathematical	—	functor OrderHom.id PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder CategoryTheory.EnrichedFunctor.id SSet SSet.largeCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.SimplicialThickening CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory instCategory instSimplicialCategory	—	CategoryTheory.EnrichedFunctor.ext SSet.hom_ext CategoryTheory.types_ext CategoryTheory.Functor.ext Set.image_congr Set.image_id' CategoryTheory.Category.comp_id
functor_map 📖	mathematical	—	CategoryTheory.EnrichedFunctor.map SSet SSet.largeCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.SimplicialThickening CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory instCategory instSimplicialCategory functor CategoryTheory.nerveMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instCategoryStruct DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder OrderHom.instFunLike as instCategoryHom functorMap	—	—
functor_obj_as 📖	mathematical	—	as CategoryTheory.EnrichedFunctor.obj SSet SSet.largeCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.SimplicialThickening CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory instCategory instSimplicialCategory functor DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder OrderHom.instFunLike	—	—
hom_ext 📖	—	Set Set.instMembership Path.I as	—	—	Path.ext Set.ext
hom_ext_iff 📖	mathematical	—	Set Set.instMembership Path.I as	—	hom_ext
id_I 📖	mathematical	—	Path.I as CategoryTheory.CategoryStruct.id CategoryTheory.SimplicialThickening instCategoryStruct Set Set.instSingletonSet	—	—

CategoryTheory.SimplicialThickening.Path

Definitions

Name	Category	Theorems
I 📖	CompOp	6 math math: CategoryTheory.SimplicialThickening.hom_ext_iff, ext_iff, right, left, CategoryTheory.SimplicialThickening.comp_I, CategoryTheory.SimplicialThickening.id_I

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	I	—	—	—
ext_iff 📖	mathematical	—	I	—	ext
le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	left_le right
le_right 📖	mathematical	Set Set.instMembership I	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
left 📖	mathematical	—	Set Set.instMembership I	—	—
left_le 📖	mathematical	Set Set.instMembership I	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
right 📖	mathematical	—	Set Set.instMembership I	—	—

CategoryTheory.SimplicialThickening.SimplicialCategory

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: comp_id, assoc, id_comp
id 📖	CompOp	2 math math: comp_id, id_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory Hom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight comp CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	SSet.hom_ext CategoryTheory.types_ext CategoryTheory.Functor.ext CategoryTheory.SimplicialThickening.hom_ext CategoryTheory.Category.assoc
comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory Hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.whiskerLeft id comp CategoryTheory.CategoryStruct.id	—	SSet.hom_ext CategoryTheory.types_ext CategoryTheory.Functor.ext CategoryTheory.SimplicialThickening.hom_ext CategoryTheory.Category.comp_id
id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory Hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.whiskerRight id comp CategoryTheory.CategoryStruct.id	—	SSet.hom_ext CategoryTheory.types_ext CategoryTheory.Functor.ext CategoryTheory.SimplicialThickening.hom_ext CategoryTheory.Category.id_comp

---

← Back to Index