NerveAdjunction

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

Statistics

Metric	Count
Definitions instReflectiveSSetCatNerveFunctor, fullyFaithfulNerveFunctor₂, functorOfNerveMap, instReflectiveTruncatedOfNatNatCatNerveFunctor₂, nerveAdjunction, fullyfaithful, nerveFunctorCompHoFunctorIso, descOfTruncation, functorEquiv, homToNerveMk, liftOfStrictSegal, app, f₂, naturalityProperty, nerve₂Adj	15
Theorems instIsIsoCatProdComparisonSSetHoFunctorNerve, instIsLeftAdjointSSetCatHoFunctor, isIso_prodComparison, isIso_prodComparison_of_stdSimplex, isIso_prodComparison_stdSimplex, preservesBinaryProduct, preservesBinaryProducts, preservesFiniteProducts, instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf, functorOfNerveMap_map, functorOfNerveMap_nerveFunctor₂_map, functorOfNerveMap_obj, instFaithfulCatTruncatedOfNatNatNerveFunctor₂, instFullCatTruncatedOfNatNatNerveFunctor₂, nerveFunctor₂_map_functorOfNerveMap, isIso_counit, faithful, full, descOfTruncation_comp, descOfTruncation_map_homMk, descOfTruncation_obj_mk, homToNerveMk_app_edge, homToNerveMk_app_one, homToNerveMk_app_zero, homToNerveMk_comp, homToNerveMk_comp_assoc, hδ'₀, hδ'₁, hδ'₂, hσ'₀, hσ'₁, naturalityProperty_eq_top, spineEquiv_f₂_arrow_one, spineEquiv_f₂_arrow_zero, liftOfStrictSegal_app_0, liftOfStrictSegal_app_1	36
Total	51

CategoryTheory

Definitions

Name	Category	Theorems
instReflectiveSSetCatNerveFunctor 📖	CompOp	—
nerveAdjunction 📖	CompOp	1 math math: nerveAdjunction.isIso_counit
nerveFunctorCompHoFunctorIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf 📖	mathematical	—	IsIso SSet SSet.largeCategory Functor.obj Cat Cat.category Functor.comp nerveFunctor SSet.hoFunctor Limits.prod Cat.of Limits.hasLimitOfHasLimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.hasLimitsOfShape_discrete CartesianMonoidalCategory.instHasFiniteProducts Cat.instCartesianMonoidalCategory Finite.of_fintype Limits.fintypeWalkingPair Limits.pair SSet.instCartesianMonoidalCategory Limits.prodComparison	—	IsIso.of_isIso_fac_right Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair Limits.hasLimitOfHasLimitsOfShape Limits.hasLimitsOfShape_discrete CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits Functor.instPreservesLimitsOfSizeOfIsRightAdjoint instIsRightAdjointOfReflective Limits.isIso_prod NatIso.hom_app_isIso IsIso.comp_isIso Limits.instIsIsoProdComparison Limits.prodComparison_natural_of_natTrans

CategoryTheory.hoFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoCatProdComparisonSSetHoFunctorNerve 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.hoFunctor CategoryTheory.Limits.prod CategoryTheory.nerve CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts SSet.instCartesianMonoidalCategory Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Cat.instCartesianMonoidalCategory CategoryTheory.Limits.prodComparison	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.IsIso.of_isIso_fac_left CategoryTheory.Limits.instHasBinaryProductObjOfPreservesLimitDiscreteWalkingPairPair CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.instIsRightAdjointOfReflective CategoryTheory.Functor.map_isIso CategoryTheory.Limits.instIsIsoProdComparison CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf CategoryTheory.Limits.prodComparison_comp CategoryTheory.IsIso.of_isIso_fac_right CategoryTheory.isIso_of_fully_faithful CategoryTheory.nerveFunctor.full CategoryTheory.nerveFunctor.faithful
instIsLeftAdjointSSetCatHoFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint SSet SSet.largeCategory CategoryTheory.Cat CategoryTheory.Cat.category SSet.hoFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
isIso_prodComparison 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.hoFunctor CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts SSet.instCartesianMonoidalCategory Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Cat.instCartesianMonoidalCategory CategoryTheory.Limits.prodComparison	—	isIso_prodComparison_of_stdSimplex CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.prod.hom_ext CategoryTheory.Cat.ext CategoryTheory.Limits.prodComparison_fst CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prodComparison_snd CategoryTheory.Limits.limit.lift_π isIso_prodComparison_stdSimplex CategoryTheory.IsIso.comp_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_hom
isIso_prodComparison_of_stdSimplex 📖	—	CategoryTheory.IsIso CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.hoFunctor CategoryTheory.Limits.prod SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts SSet.instCartesianMonoidalCategory Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Cat.instCartesianMonoidalCategory CategoryTheory.Limits.prodComparison	—	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor instIsLeftAdjointSSetCatHoFunctor
isIso_prodComparison_stdSimplex 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.hoFunctor CategoryTheory.Limits.prod SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts SSet.instCartesianMonoidalCategory Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Cat.instCartesianMonoidalCategory CategoryTheory.Limits.prodComparison	—	CategoryTheory.IsIso.of_isIso_fac_right CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.Limits.isIso_prod CategoryTheory.Functor.map_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.IsIso.comp_isIso instIsIsoCatProdComparisonSSetHoFunctorNerve CategoryTheory.Limits.prodComparison_natural
preservesBinaryProduct 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit SSet SSet.largeCategory CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair SSet.hoFunctor	—	CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype isIso_prodComparison
preservesBinaryProducts 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape SSet SSet.largeCategory CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory SSet.hoFunctor	—	CategoryTheory.Limits.preservesLimit_of_iso_diagram preservesBinaryProduct
preservesFiniteProducts 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts SSet SSet.largeCategory CategoryTheory.Cat CategoryTheory.Cat.category SSet.hoFunctor	—	CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal preservesBinaryProducts SSet.hoFunctor.preservesTerminal' CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts

CategoryTheory.nerve

Definitions

Name	Category	Theorems
fullyFaithfulNerveFunctor₂ 📖	CompOp	—
functorOfNerveMap 📖	CompOp	4 math math: functorOfNerveMap_map, functorOfNerveMap_nerveFunctor₂_map, functorOfNerveMap_obj, nerveFunctor₂_map_functorOfNerveMap
instReflectiveTruncatedOfNatNatCatNerveFunctor₂ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorOfNerveMap_map 📖	mathematical	—	CategoryTheory.Functor.map functorOfNerveMap DFunLike.coe Equiv SSet.Edge CategoryTheory.nerve CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.Nerve.nerveFunctor₂ Opposite.op CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.ComposableArrows EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.nerveEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homEquiv SSet.Truncated.Edge.map SSet SSet.largeCategory SSet.truncation SSet.Edge.toTruncated edgeMk	—	—
functorOfNerveMap_nerveFunctor₂_map 📖	mathematical	—	functorOfNerveMap CategoryTheory.Functor.map SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.nerveFunctor CategoryTheory.Cat.of CategoryTheory.nerveMap CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str	—	CategoryTheory.Functor.ext
functorOfNerveMap_obj 📖	mathematical	—	CategoryTheory.Functor.obj functorOfNerveMap DFunLike.coe Equiv CategoryTheory.ComposableArrows CategoryTheory.Cat.str CategoryTheory.Cat.of EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.nerveEquiv CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.Nerve.nerveFunctor₂ Opposite.op CategoryTheory.Bundled.α CategoryTheory.Category Equiv.symm	—	—
instFaithfulCatTruncatedOfNatNatNerveFunctor₂ 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.Nerve.nerveFunctor₂	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullCatTruncatedOfNatNatNerveFunctor₂ 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.Nerve.nerveFunctor₂	—	CategoryTheory.Functor.FullyFaithful.full
nerveFunctor₂_map_functorOfNerveMap 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat CategoryTheory.Cat.category SSet.Truncated SSet.Truncated.largeCategory CategoryTheory.Nerve.nerveFunctor₂ CategoryTheory.Cat.of CategoryTheory.Functor.toCatHom functorOfNerveMap	—	SSet.Truncated.IsStrictSegal.hom_ext CategoryTheory.Nerve.instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂ CategoryTheory.ComposableArrows.mk₁_surjective CategoryTheory.nerveMap_app_mk₁ mk₁_homEquiv_apply CategoryTheory.ComposableArrows.mk₁_hom

CategoryTheory.nerveAdjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_counit 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.category CategoryTheory.Functor.comp SSet SSet.largeCategory CategoryTheory.nerveFunctor SSet.hoFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.nerveAdjunction	—	CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful CategoryTheory.nerveFunctor.full CategoryTheory.nerveFunctor.faithful

CategoryTheory.nerveFunctor

Definitions

Name	Category	Theorems
fullyfaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Cat CategoryTheory.Cat.category SSet SSet.largeCategory CategoryTheory.nerveFunctor	—	CategoryTheory.Functor.Faithful.of_iso CategoryTheory.Functor.Faithful.comp CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂ SSet.Truncated.cosk.faithful
full 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Cat CategoryTheory.Cat.category SSet SSet.largeCategory CategoryTheory.nerveFunctor	—	CategoryTheory.Functor.Full.of_iso CategoryTheory.Functor.Full.comp CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂ SSet.Truncated.cosk.full

SSet.Truncated

Definitions

Name	Category	Theorems
liftOfStrictSegal 📖	CompOp	2 math math: liftOfStrictSegal_app_0, liftOfStrictSegal_app_1
nerve₂Adj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftOfStrictSegal_app_0 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ SimplexCategory.Truncated.σ₂	CategoryTheory.NatTrans.app liftOfStrictSegal	—	—
liftOfStrictSegal_app_1 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ SimplexCategory.Truncated.σ₂	CategoryTheory.NatTrans.app liftOfStrictSegal	—	—

SSet.Truncated.HomotopyCategory

Definitions

Name	Category	Theorems
descOfTruncation 📖	CompOp	3 math math: descOfTruncation_comp, descOfTruncation_map_homMk, descOfTruncation_obj_mk
functorEquiv 📖	CompOp	—
homToNerveMk 📖	CompOp	5 math math: homToNerveMk_app_one, homToNerveMk_app_edge, homToNerveMk_app_zero, homToNerveMk_comp, homToNerveMk_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descOfTruncation_comp 📖	mathematical	—	descOfTruncation CategoryTheory.CategoryStruct.comp SSet.Truncated CategoryTheory.Category.toCategoryStruct SSet.Truncated.largeCategory CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.truncation CategoryTheory.nerve CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory SSet.Truncated.mapHomotopyCategory	—	functor_ext descOfTruncation_map_homMk CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp EquivLike.toEmbeddingLike
descOfTruncation_map_homMk 📖	mathematical	—	CategoryTheory.Functor.map SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory descOfTruncation homMk DFunLike.coe Equiv SSet.Edge CategoryTheory.nerve CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.nerveEquiv CategoryTheory.nerve.homEquiv SSet.Truncated.Edge.map	—	CategoryTheory.Category.id_comp
descOfTruncation_obj_mk 📖	mathematical	—	CategoryTheory.Functor.obj SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory descOfTruncation DFunLike.coe Equiv CategoryTheory.ComposableArrows EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.nerveEquiv CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation CategoryTheory.nerve Opposite.op	—	—
homToNerveMk_app_edge 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation CategoryTheory.nerve homToNerveMk Opposite.op SSet.Truncated.Edge.edge CategoryTheory.ComposableArrows.mk₁ SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.map homMk	—	homToNerveMk_app_one Equiv.injective congr_arrowMk_homMk
homToNerveMk_app_one 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation CategoryTheory.nerve homToNerveMk Opposite.op CategoryTheory.ComposableArrows.mk₁ SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.map CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ homMk SSet.Truncated.Edge.mk'	—	—
homToNerveMk_app_zero 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.Truncated SSet.Truncated.largeCategory SSet.truncation CategoryTheory.nerve homToNerveMk Opposite.op DFunLike.coe Equiv CategoryTheory.ComposableArrows EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.nerveEquiv SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory	—	—
homToNerveMk_comp 📖	mathematical	—	homToNerveMk CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.CategoryStruct.comp SSet.Truncated CategoryTheory.Category.toCategoryStruct SSet.Truncated.largeCategory CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.truncation CategoryTheory.nerve CategoryTheory.Functor.map CategoryTheory.nerveMap	—	SSet.Truncated.IsStrictSegal.hom_ext SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal CategoryTheory.Nerve.isStrictSegal SSet.Truncated.Edge.exists_of_simplex homToNerveMk_app_edge CategoryTheory.ComposableArrows.ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
homToNerveMk_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet.Truncated CategoryTheory.Category.toCategoryStruct SSet.Truncated.largeCategory CategoryTheory.Functor.obj SSet SSet.largeCategory SSet.truncation CategoryTheory.nerve homToNerveMk CategoryTheory.Functor.comp SSet.Truncated.HomotopyCategory SSet.Truncated.instCategoryHomotopyCategory CategoryTheory.Functor.map CategoryTheory.nerveMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homToNerveMk_comp

SSet.Truncated.liftOfStrictSegal

Definitions

Name	Category	Theorems
app 📖	CompOp	—
f₂ 📖	CompOp	7 math math: hδ'₂, hσ'₀, hδ'₁, hδ'₀, hσ'₁, spineEquiv_f₂_arrow_one, spineEquiv_f₂_arrow_zero
naturalityProperty 📖	CompOp	1 math math: naturalityProperty_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hδ'₀ 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂	f₂	—	spineEquiv_f₂_arrow_one SimplexCategory.mkOfSucc_one_eq_δ
hδ'₁ 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂	f₂	—	hδ'₂ hδ'₀
hδ'₂ 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂	f₂	—	spineEquiv_f₂_arrow_zero SimplexCategory.mkOfSucc_zero_eq_δ
hσ'₀ 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ SimplexCategory.Truncated.σ₂	f₂	—	Equiv.injective SSet.Truncated.Path.ext' Fintype.complete spineEquiv_f₂_arrow_zero CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero SimplexCategory.mkOfSucc_zero_eq_δ spineEquiv_f₂_arrow_one SimplexCategory.Truncated.δ₂_zero_comp_σ₂_zero CategoryTheory.FunctorToTypes.map_id_apply SimplexCategory.mkOfSucc_one_eq_δ
hσ'₁ 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ SimplexCategory.Truncated.σ₂	f₂	—	Equiv.injective SSet.Truncated.Path.ext' Fintype.complete spineEquiv_f₂_arrow_zero SimplexCategory.Truncated.δ₂_two_comp_σ₂_one CategoryTheory.FunctorToTypes.map_id_apply SimplexCategory.mkOfSucc_zero_eq_δ spineEquiv_f₂_arrow_one CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one SimplexCategory.mkOfSucc_one_eq_δ
naturalityProperty_eq_top 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂ SimplexCategory.Truncated.σ₂	naturalityProperty Top.top CategoryTheory.MorphismProperty BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	SimplexCategory.Truncated.morphismProperty_eq_top CategoryTheory.MorphismProperty.IsMultiplicative.unop CategoryTheory.MorphismProperty.IsMultiplicative.naturalityProperty Fintype.complete CategoryTheory.types_ext hδ'₀ hδ'₁ hδ'₂ hσ'₀ hσ'₁
spineEquiv_f₂_arrow_one 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂	SSet.Truncated.Path.arrow DFunLike.coe Equiv CategoryTheory.Functor.obj SSet.Truncated.Path EquivLike.toFunLike Equiv.instEquivLike SSet.Truncated.StrictSegal.spineEquiv f₂	—	Equiv.apply_symm_apply SimplexCategory.mkOfSucc_eq_id CategoryTheory.FunctorToTypes.map_id_apply Matrix.cons_val_fin_one
spineEquiv_f₂_arrow_zero 📖	mathematical	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.types Opposite.op CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.Truncated.δ₂	SSet.Truncated.Path.arrow DFunLike.coe Equiv CategoryTheory.Functor.obj SSet.Truncated.Path EquivLike.toFunLike Equiv.instEquivLike SSet.Truncated.StrictSegal.spineEquiv f₂	—	Equiv.apply_symm_apply SimplexCategory.mkOfSucc_eq_id CategoryTheory.FunctorToTypes.map_id_apply

---

← Back to Index