Coskeletal

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

Statistics

Metric	Count
Definitions IsCoskeletal, isUniversalOfIsRightKanExtension, rightExtensionInclusion, isoCoskOfIsCoskeletal	4
Theorems isRightKanExtension, rightExtensionInclusion_hom_app, rightExtensionInclusion_left, rightExtensionInclusion_right_as, instIsIsoAppUnitTruncatedCoskAdj, isCoskeletal_iff, isCoskeletal_iff_isIso, isoCoskOfIsCoskeletal_hom	8
Total	12

CategoryTheory.SimplicialObject

Definitions

Name	Category	Theorems
IsCoskeletal 📖	CompData	5 math math: CategoryTheory.Nerve.instIsCoskeletalNerveOfNatNat, SSet.StrictSegal.isCoskeletal, isCoskeletal_iff, SSet.StrictSegal.isCoskeletal', isCoskeletal_iff_isIso
isoCoskOfIsCoskeletal 📖	CompOp	1 math math: isoCoskOfIsCoskeletal_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoAppUnitTruncatedCoskAdj 📖	mathematical	CategoryTheory.Functor.HasRightKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion	CategoryTheory.IsIso CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp Truncated instCategoryTruncated truncation Truncated.cosk CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit coskAdj	—	isCoskeletal_iff_isIso
isCoskeletal_iff 📖	mathematical	—	IsCoskeletal CategoryTheory.Functor.IsRightKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	—
isCoskeletal_iff_isIso 📖	mathematical	CategoryTheory.Functor.HasRightKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion	IsCoskeletal CategoryTheory.IsIso CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp Truncated instCategoryTruncated truncation Truncated.cosk CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit coskAdj	—	isCoskeletal_iff CategoryTheory.Functor.isRightKanExtension_iff_isIso CategoryTheory.Adjunction.left_triangle_components instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation
isoCoskOfIsCoskeletal_hom 📖	mathematical	CategoryTheory.Functor.HasRightKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion	CategoryTheory.Iso.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.obj cosk isoCoskOfIsCoskeletal CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp Truncated instCategoryTruncated truncation Truncated.cosk CategoryTheory.Adjunction.unit coskAdj	—	—

CategoryTheory.SimplicialObject.IsCoskeletal

Definitions

Name	Category	Theorems
isUniversalOfIsRightKanExtension 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRightKanExtension 📖	mathematical	—	CategoryTheory.Functor.IsRightKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	—	—

CategoryTheory.SimplicialObject.Truncated

Definitions

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

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.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 CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.unop	—	—
rightExtensionInclusion_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory 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.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