Nerve

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

Statistics

Metric	Count
Definitions `instCategoryObjOppositeSimplexCategoryNerve`, `nerve`, `edgeMk`, `homEquiv`, `representableBy`, `nerveEquiv`, `nerveFunctor`, `nerveMap`	8
Theorems `edgeMk_edge`, `edgeMk_id`, `edgeMk_surjective`, `ext_of_isThin`, `ext_of_isThin_iff`, `homEquiv_apply`, `homEquiv_comp`, `homEquiv_edgeMk`, `homEquiv_edgeMk_map_nerveMap`, `homEquiv_id`, `homEquiv_symm_apply`, `left_edge`, `mk₁_homEquiv_apply`, `nonempty_compStruct_iff`, `right_edge`, `δ_obj`, `δ₀_eq`, `δ₀_mk₂_eq`, `δ₁_mk₂_eq`, `δ₂_mk₂_eq`, `δ₂_two`, `δ₂_zero`, `σ_obj`, `σ_zero_nerveEquiv_symm`, `σ₀_mk₀_eq`, `nerveFunctor_map`, `nerveFunctor_obj`, `nerveMap_app`, `nerveMap_app_mk₀`, `nerveMap_app_mk₁`, `nerve_map`, `nerve_obj`	32
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
`instCategoryObjOppositeSimplexCategoryNerve` 📖	CompOp	—
`nerve` 📖	CompOp	56 math math: `SSet.OneTruncation₂.nerveEquiv_apply`, `nerve.edgeMk_edge`, `nerve.σ_obj`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `Nerve.instIsCoskeletalNerveOfNatNat`, `SSet.Truncated.HomotopyCategory.descOfTruncation_comp`, `nerve.δ₂_zero`, `SSet.OneTruncation₂.nerveHomEquiv_id`, `nerve.functorOfNerveMap_map`, `nerve.homEquiv_edgeMk_map_nerveMap`, `Nerve.isStrictSegal`, `nerve.homEquiv_apply`, `nerve.edgeMk_id`, `nerve.right_edge`, `nerve.homEquiv_edgeMk`, `nerve.nonempty_compStruct_iff`, `PartialOrder.mem_nerve_degenerate_of_eq`, `PartialOrder.mem_nerve_nonDegenerate_iff_injective`, `nerve.homEquiv_comp`, `nerve.left_edge`, `nerve.mk₁_homEquiv_apply`, `nerveMap_app_mk₁`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `SSet.OneTruncation₂.nerveEquiv_symm_apply_map`, `SSet.stdSimplex.isoNerve_hom_app_apply`, `PartialOrder.mem_range_nerve_σ_iff`, `nerve.homEquiv_id`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `nerve.δ₁_mk₂_eq`, `PartialOrder.mem_nerve_nonDegenerate_iff_strictMono`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_one`, `Nerve.quasicategory`, `nerve.σ₀_mk₀_eq`, `nerve_map`, `nerve.δ_obj`, `nerve.δ₂_mk₂_eq`, `nerve_obj`, `nerve.σ_zero_nerveEquiv_symm`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `SSet.OneTruncation₂.nerveEquiv_symm_apply_obj`, `hoFunctor.instIsIsoCatProdComparisonSSetHoFunctorNerve`, `nerveFunctor_obj`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero`, `SSet.Truncated.HomotopyCategory.homToNerveMk_comp`, `nerveMap_app`, `nerve.δ₀_eq`, `nerve.δ₀_mk₂_eq`, `SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk`, `nerveMap_app_mk₀`, `SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc`, `nerve.δ₂_two`, `nerve.edgeMk_surjective`, `SSet.stdSimplex.isoNerve_inv_app_apply`, `nerve.homEquiv_symm_apply`
`nerveEquiv` 📖	CompOp	19 math math: `nerve.edgeMk_edge`, `nerve.functorOfNerveMap_map`, `nerve.homEquiv_edgeMk_map_nerveMap`, `nerve.homEquiv_apply`, `nerve.edgeMk_id`, `nerve.right_edge`, `nerve.homEquiv_edgeMk`, `nerve.nonempty_compStruct_iff`, `nerve.homEquiv_comp`, `nerve.left_edge`, `nerve.mk₁_homEquiv_apply`, `nerve.homEquiv_id`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `nerve.σ_zero_nerveEquiv_symm`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero`, `nerve.functorOfNerveMap_obj`, `SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk`, `nerve.edgeMk_surjective`, `nerve.homEquiv_symm_apply`
`nerveFunctor` 📖	CompOp	7 math math: `nerveFunctor.faithful`, `nerveFunctor_map`, `nerveFunctor.full`, `nerve.functorOfNerveMap_nerveFunctor₂_map`, `nerveFunctor_obj`, `instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf`, `nerveAdjunction.isIso_counit`
`nerveMap` 📖	CompOp	9 math math: `nerve.homEquiv_edgeMk_map_nerveMap`, `nerveMap_app_mk₁`, `SimplicialThickening.functor_map`, `nerveFunctor_map`, `nerve.functorOfNerveMap_nerveFunctor₂_map`, `SSet.Truncated.HomotopyCategory.homToNerveMk_comp`, `nerveMap_app`, `nerveMap_app_mk₀`, `SSet.Truncated.HomotopyCategory.homToNerveMk_comp_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nerveFunctor_map` 📖	mathematical	—	`Functor.map` `Cat` `Cat.category` `SSet` `SSet.largeCategory` `nerveFunctor` `nerveMap` `Bundled.α` `Category` `Cat.str` `Cat.Hom.toFunctor`	—	—
`nerveFunctor_obj` 📖	mathematical	—	`Functor.obj` `Cat` `Cat.category` `SSet` `SSet.largeCategory` `nerveFunctor` `nerve` `Bundled.α` `Category` `Cat.str`	—	—
`nerveMap_app` 📖	mathematical	—	`NatTrans.app` `Opposite` `SimplexCategory` `Category.opposite` `SimplexCategory.smallCategory` `types` `nerve` `nerveMap` `Functor.obj` `ComposableArrows` `SimplexCategory.len` `Opposite.unop` `Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Functor.mapComposableArrows`	—	—
`nerveMap_app_mk₀` 📖	mathematical	—	`NatTrans.app` `Opposite` `SimplexCategory` `Category.opposite` `SimplexCategory.smallCategory` `types` `nerve` `nerveMap` `Opposite.op` `ComposableArrows.mk₀` `Functor.obj`	—	`ComposableArrows.ext₀`
`nerveMap_app_mk₁` 📖	mathematical	—	`NatTrans.app` `Opposite` `SimplexCategory` `Category.opposite` `SimplexCategory.smallCategory` `types` `nerve` `nerveMap` `Opposite.op` `ComposableArrows.mk₁` `Functor.obj` `Functor.map`	—	`ComposableArrows.ext₁` `Category.comp_id` `Category.id_comp`
`nerve_map` 📖	mathematical	—	`Functor.map` `Opposite` `SimplexCategory` `Category.opposite` `SimplexCategory.smallCategory` `types` `nerve` `ComposableArrows.whiskerLeft` `SimplexCategory.len` `Opposite.unop` `Cat.Hom.toFunctor` `Functor.obj` `Cat` `Cat.category` `SimplexCategory.toCat` `Quiver.Hom.unop` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	—
`nerve_obj` 📖	mathematical	—	`Functor.obj` `Opposite` `SimplexCategory` `Category.opposite` `SimplexCategory.smallCategory` `types` `nerve` `ComposableArrows` `SimplexCategory.len` `Opposite.unop`	—	—

CategoryTheory.nerve

Definitions

Name	Category	Theorems
`edgeMk` 📖	CompOp	7 math math: `edgeMk_edge`, `functorOfNerveMap_map`, `homEquiv_edgeMk_map_nerveMap`, `edgeMk_id`, `homEquiv_edgeMk`, `nonempty_compStruct_iff`, `edgeMk_surjective`
`homEquiv` 📖	CompOp	9 math math: `functorOfNerveMap_map`, `homEquiv_edgeMk_map_nerveMap`, `homEquiv_apply`, `homEquiv_edgeMk`, `homEquiv_comp`, `mk₁_homEquiv_apply`, `homEquiv_id`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `homEquiv_symm_apply`
`representableBy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edgeMk_edge` 📖	mathematical	—	`SSet.Edge.edge` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `edgeMk` `CategoryTheory.ComposableArrows.mk₁`	—	—
`edgeMk_id` 📖	mathematical	—	`edgeMk` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `SSet.Edge.id` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv`	—	`SSet.Edge.ext` `CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`edgeMk_surjective` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SSet.Edge` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `edgeMk`	—	`Equiv.apply_symm_apply` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `SSet.Edge.ext` `CategoryTheory.ComposableArrows.ext₁` `right_edge`
`ext_of_isThin` 📖	—	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	—	`CategoryTheory.ComposableArrows.ext`
`ext_of_isThin_iff` 📖	mathematical	`Quiver.IsThin` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.obj` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder`	—	`ext_of_isThin`
`homEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SSet.Edge` `CategoryTheory.nerve` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ComposableArrows.left` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite.op` `SSet.Edge.edge` `CategoryTheory.eqToHom` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom`	—	—
`homEquiv_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv` `SSet.Edge` `CategoryTheory.nerve` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `homEquiv`	—	`Equiv.surjective` `edgeMk_surjective` `homEquiv_edgeMk` `nonempty_compStruct_iff`
`homEquiv_edgeMk` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SSet.Edge` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homEquiv` `edgeMk`	—	`Equiv.injective` `Equiv.symm_apply_apply`
`homEquiv_edgeMk_map_nerveMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SSet.Edge` `CategoryTheory.nerve` `CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.nerveMap` `Opposite.op` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homEquiv` `SSet.Edge.map` `edgeMk` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homEquiv_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SSet.Edge` `CategoryTheory.nerve` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv` `homEquiv` `SSet.Edge.id` `CategoryTheory.CategoryStruct.id`	—	`Equiv.surjective` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv` `SSet.Edge` `CategoryTheory.nerve` `Equiv.symm` `homEquiv` `CategoryTheory.ComposableArrows.mk₁`	—	—
`left_edge` 📖	mathematical	—	`CategoryTheory.ComposableArrows.left` `SSet.Edge.edge` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv`	—	`SSet.Edge.src_eq`
`mk₁_homEquiv_apply` 📖	mathematical	—	`CategoryTheory.ComposableArrows.mk₁` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv` `SSet.Edge` `CategoryTheory.nerve` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `homEquiv` `CategoryTheory.ComposableArrows.left` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite.op` `SSet.Edge.edge` `CategoryTheory.ComposableArrows.right` `CategoryTheory.ComposableArrows.hom`	—	`CategoryTheory.ComposableArrows.mk₁_eqToHom_comp` `CategoryTheory.ComposableArrows.mk₁_comp_eqToHom`
`nonempty_compStruct_iff` 📖	mathematical	—	`SSet.Edge.CompStruct` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `edgeMk` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `Equiv.injective` `SSet.Edge.CompStruct.d₁` `SSet.Edge.CompStruct.d₀` `SSet.Edge.CompStruct.d₂` `CategoryTheory.ComposableArrows.ext₂_of_arrow` `δ₂_two` `δ₂_zero`
`right_edge` 📖	mathematical	—	`CategoryTheory.ComposableArrows.right` `SSet.Edge.edge` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.nerveEquiv`	—	`SSet.Edge.tgt_eq`
`δ_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `Fin.succAbove`	—	—
`δ₀_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.δ₀`	—	—
`δ₀_mk₂_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.ComposableArrows.mk₁`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`δ₁_mk₂_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`δ₂_mk₂_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.ComposableArrows.mk₁`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`δ₂_two` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.ComposableArrows.map'`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`δ₂_zero` 📖	mathematical	—	`CategoryTheory.SimplicialObject.δ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.ComposableArrows.map'`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`σ_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `SimplexCategory.len` `Opposite.unop` `SimplexCategory` `Opposite.op` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `CategoryTheory.nerve` `Fin.predAbove`	—	—
`σ_zero_nerveEquiv_symm` 📖	mathematical	—	`CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `CategoryTheory.nerve` `DFunLike.coe` `Equiv` `CategoryTheory.ComposableArrows` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.nerveEquiv` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id`
`σ₀_mk₀_eq` 📖	mathematical	—	`CategoryTheory.SimplicialObject.σ` `CategoryTheory.types` `CategoryTheory.nerve` `CategoryTheory.ComposableArrows.mk₀` `CategoryTheory.ComposableArrows.mk₁` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.ComposableArrows.ext₁` `CategoryTheory.Category.comp_id`

---

← Back to Index