Documentation Verification Report

Coskeletal

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

Statistics

Metric	Count
Definitions `cosk₂Iso`, `nerveFunctor₂`, `isPointwiseRightKanExtension`, `isPointwiseRightKanExtensionAt`, `strArrowMk₂`, `rightExtensionInclusion`	6
Theorems `instIsCoskeletalNerveOfNatNat`, `instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂`, `isCoskeletal`, `isCoskeletal'`, `fac_aux₁`, `fac_aux₂`, `fac_aux₃`, `isRightKanExtension`, `rightExtensionInclusion_hom_app`, `rightExtensionInclusion_left`, `rightExtensionInclusion_right_as`	11
Total	17

CategoryTheory.Nerve

Definitions

Name	Category	Theorems
`cosk₂Iso` 📖	CompOp	—
`nerveFunctor₂` 📖	CompOp	11 math math: `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map`, `CategoryTheory.nerve.instFullCatTruncatedOfNatNatNerveFunctor₂`, `CategoryTheory.nerve.functorOfNerveMap_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj`, `instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂`, `SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map`, `SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map`, `CategoryTheory.nerve.functorOfNerveMap_obj`, `CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap`, `CategoryTheory.nerve.instFaithfulCatTruncatedOfNatNatNerveFunctor₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCoskeletalNerveOfNatNat` 📖	mathematical	—	`CategoryTheory.SimplicialObject.IsCoskeletal` `CategoryTheory.types` `CategoryTheory.nerve`	—	`SSet.StrictSegal.isCoskeletal'` `isStrictSegal`
`instIsStrictSegalObjCatTruncatedOfNatNatNerveFunctor₂` 📖	mathematical	—	`SSet.Truncated.IsStrictSegal` `CategoryTheory.Functor.obj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `SSet.Truncated` `SSet.Truncated.largeCategory` `nerveFunctor₂`	—	`SSet.StrictSegal.instIsStrictSegalObjTruncatedHAddNatOfNatTruncationOfIsStrictSegal` `isStrictSegal`

SSet.StrictSegal

Definitions

Name	Category	Theorems
`isPointwiseRightKanExtension` 📖	CompOp	—
`isPointwiseRightKanExtensionAt` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoskeletal` 📖	mathematical	—	`CategoryTheory.SimplicialObject.IsCoskeletal` `CategoryTheory.types`	—	`isRightKanExtension`
`isCoskeletal'` 📖	mathematical	—	`CategoryTheory.SimplicialObject.IsCoskeletal` `CategoryTheory.types`	—	`isCoskeletal`
`isRightKanExtension` 📖	mathematical	—	`CategoryTheory.Functor.IsRightKanExtension` `Opposite` `SimplexCategory.Truncated` `SimplexCategory` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.Functor.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension`

SSet.StrictSegal.isPointwiseRightKanExtensionAt

Definitions

Name	Category	Theorems
`strArrowMk₂` 📖	CompOp	3 math math: `fac_aux₂`, `fac_aux₃`, `fac_aux₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac_aux₁` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.mkOfSucc` `lift` `CategoryTheory.NatTrans.app` `CategoryTheory.StructuredArrow` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.StructuredArrow.proj` `CategoryTheory.Limits.Cone.π` `strArrowMk₂`	—	`Fin.castSucc_le_succ` `SSet.StrictSegal.spineToSimplex_arrow`
`fac_aux₂` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SimplexCategory.mkOfLe` `lift` `CategoryTheory.NatTrans.app` `CategoryTheory.StructuredArrow` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.StructuredArrow.proj` `CategoryTheory.Limits.Cone.π` `strArrowMk₂`	—	`le_refl` `SimplexCategory.Hom.ext_one_left` `CategoryTheory.NatTrans.naturality` `CategoryTheory.op_comp` `CategoryTheory.Functor.map_comp` `Fin.castSucc_le_succ` `lift.eq_1` `SSet.StrictSegal.spineToSimplex_vertex` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `SimplexCategory.Hom.ext` `OrderHom.ext` `Fintype.complete` `fac_aux₁` `SSet.StrictSegal.spineInjective` `SSet.Path.ext'` `SSet.StrictSegal.spineToSimplex_spine_apply` `SSet.StrictSegal.spine_spineToSimplex_apply` `SSet.spine_arrow` `CategoryTheory.FunctorToTypes.map_comp_apply` `CategoryTheory.Limits.Cone.w` `CategoryTheory.StructuredArrow.w`
`fac_aux₃` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `lift` `CategoryTheory.NatTrans.app` `CategoryTheory.StructuredArrow` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.StructuredArrow.proj` `CategoryTheory.Limits.Cone.π` `strArrowMk₂`	—	`OrderHom.monotone` `SimplexCategory.Hom.ext_one_left` `fac_aux₂`

SSet.Truncated

Definitions

Name	Category	Theorems
`rightExtensionInclusion` 📖	CompOp	3 math math: `rightExtensionInclusion_right_as`, `rightExtensionInclusion_left`, `rightExtensionInclusion_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rightExtensionInclusion_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `SimplexCategory.Truncated` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory` `SimplexCategory.smallCategory` `SimplexCategory.len` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.Comma.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.fromPUnit` `rightExtensionInclusion`	—	—
`rightExtensionInclusion_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.Functor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.comp` `rightExtensionInclusion`	—	—
`rightExtensionInclusion_right_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `CategoryTheory.Comma.right` `CategoryTheory.Functor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `SimplexCategory.Truncated` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SimplexCategory.len` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.op` `SimplexCategory.Truncated.inclusion` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.comp` `rightExtensionInclusion`	—	—

---

← Back to Index