Basic

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

Statistics

Metric	Count
Definitions CosimplicialObject, const, drop, leftOp, leftOpRightOpIso, point, toArrow, whiskering, whiskeringObj, mkNotation, trunc, whiskering, augment, const, eqToIso, instCategory, instCategoryAugmented, instCategoryTruncated, truncation, truncationCompTrunc, whiskering, δ, σ, const, drop, point, rightOp, rightOpLeftOpIso, toArrow, whiskering, whiskeringObj, cosk, fullyFaithful, reflective, mkNotation, sk, fullyFaithful, coreflective, trunc, whiskering, augment, const, cosk, coskAdj, diagonal, eqToIso, instCategoryAugmented, instCategoryTruncated, sk, skAdj, truncation, truncationCompTrunc, whiskering, δ, σ, cosimplicialSimplicialEquiv, cosimplicialToSimplicialAugmented, instCategorySimplicialObject, simplicialCosimplicialAugmentedEquiv, simplicialCosimplicialEquiv, simplicialToCosimplicialAugmented, «term_^⦋_⦌», «term__⦋_⦌»	63
Theorems const_map_left, const_map_right, const_obj_hom, const_obj_left, const_obj_right, drop_map, drop_obj, hom_ext, hom_ext_iff, leftOpRightOpIso_hom_left, leftOpRightOpIso_hom_right_app, leftOpRightOpIso_inv_left, leftOpRightOpIso_inv_right_app, leftOp_hom_app, leftOp_left_map, leftOp_left_obj, leftOp_right, point_map, point_obj, toArrow_map_left, toArrow_map_right, toArrow_obj_hom, toArrow_obj_left, toArrow_obj_right, whiskering_map_app_left, whiskering_map_app_right, whiskering_obj, instHasColimits, instHasColimitsOfShape, instHasLimits, instHasLimitsOfShape, whiskering_map_app_app, whiskering_obj_map_app, whiskering_obj_obj_map, whiskering_obj_obj_obj, augment_hom_app, augment_hom_zero, augment_left, augment_right, comp_app, comp_left, comp_right_app, eqToIso_refl, hom_ext, hom_ext_iff, id_app, id_left, id_right_app, instHasColimits, instHasColimitsOfShape, instHasLimits, instHasLimitsOfShape, whiskering_map_app_app, whiskering_obj_map_app, whiskering_obj_obj_map, whiskering_obj_obj_obj, δ_comp_δ, δ_comp_δ', δ_comp_δ'', δ_comp_δ''_assoc, δ_comp_δ'_assoc, δ_comp_δ_assoc, δ_comp_δ_self, δ_comp_δ_self', δ_comp_δ_self'_assoc, δ_comp_δ_self_assoc, δ_comp_σ_of_gt, δ_comp_σ_of_gt', δ_comp_σ_of_gt'_assoc, δ_comp_σ_of_gt_assoc, δ_comp_σ_of_le, δ_comp_σ_of_le_assoc, δ_comp_σ_self, δ_comp_σ_self', δ_comp_σ_self'_assoc, δ_comp_σ_self_assoc, δ_comp_σ_succ, δ_comp_σ_succ', δ_comp_σ_succ'_assoc, δ_comp_σ_succ_assoc, δ_naturality, δ_naturality_assoc, σ_comp_σ, σ_comp_σ_assoc, σ_naturality, σ_naturality_assoc, const_map_left, const_map_right, const_obj_hom, const_obj_left, const_obj_right, drop_map, drop_obj, hom_ext, hom_ext_iff, point_map, point_obj, rightOpLeftOpIso_hom_left_app, rightOpLeftOpIso_hom_right, rightOpLeftOpIso_inv_left_app, rightOpLeftOpIso_inv_right, rightOp_hom_app, rightOp_left, rightOp_right_map, rightOp_right_obj, toArrow_map_left, toArrow_map_right, toArrow_obj_hom, toArrow_obj_left, toArrow_obj_right, whiskering_map_app_left, whiskering_map_app_right, whiskering_obj, w₀, w₀_assoc, faithful, full, cosk_reflective, instHasColimits, instHasColimitsOfShape, instHasLimits, instHasLimitsOfShape, faithful, full, sk_coreflective, trunc_map_app, trunc_obj_map, trunc_obj_obj, whiskering_map_app_app, whiskering_obj_map_app, whiskering_obj_obj_map, whiskering_obj_obj_obj, augment_hom_app, augment_hom_zero, augment_left, augment_right, comp_left_app, comp_right, eqToIso_refl, hom_ext, hom_ext_iff, id_left_app, id_right, instHasColimits, instHasColimitsOfShape, instHasLimits, instHasLimitsOfShape, instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, whiskering_map_app_app, whiskering_obj_map_app, whiskering_obj_obj_map, whiskering_obj_obj_obj, δ_comp_δ, δ_comp_δ', δ_comp_δ'', δ_comp_δ''_assoc, δ_comp_δ'_assoc, δ_comp_δ_assoc, δ_comp_δ_self, δ_comp_δ_self', δ_comp_δ_self'_assoc, δ_comp_δ_self_assoc, δ_comp_σ_of_gt, δ_comp_σ_of_gt', δ_comp_σ_of_gt'_assoc, δ_comp_σ_of_gt_assoc, δ_comp_σ_of_le, δ_comp_σ_of_le_assoc, δ_comp_σ_self, δ_comp_σ_self', δ_comp_σ_self'_assoc, δ_comp_σ_self_assoc, δ_comp_σ_succ, δ_comp_σ_succ', δ_comp_σ_succ'_assoc, δ_comp_σ_succ_assoc, δ_def, δ_naturality, δ_naturality_assoc, σ_comp_σ, σ_comp_σ_assoc, σ_def, σ_naturality, σ_naturality_assoc, comp_app, cosimplicialSimplicialEquiv_counitIso_hom_app_app, cosimplicialSimplicialEquiv_counitIso_inv_app_app, cosimplicialSimplicialEquiv_functor_map_app, cosimplicialSimplicialEquiv_functor_obj_map, cosimplicialSimplicialEquiv_functor_obj_obj, cosimplicialSimplicialEquiv_inverse_map, cosimplicialSimplicialEquiv_inverse_obj, cosimplicialSimplicialEquiv_unitIso_hom_app, cosimplicialSimplicialEquiv_unitIso_inv_app, cosimplicialToSimplicialAugmented_map, cosimplicialToSimplicialAugmented_obj, id_app, simplicialCosimplicialAugmentedEquiv_functor, simplicialCosimplicialAugmentedEquiv_inverse, simplicialCosimplicialEquiv_counitIso_hom_app_app, simplicialCosimplicialEquiv_counitIso_inv_app_app, simplicialCosimplicialEquiv_functor_map_app, simplicialCosimplicialEquiv_functor_obj_map, simplicialCosimplicialEquiv_functor_obj_obj, simplicialCosimplicialEquiv_inverse_map, simplicialCosimplicialEquiv_inverse_obj, simplicialCosimplicialEquiv_unitIso_hom_app, simplicialCosimplicialEquiv_unitIso_inv_app, simplicialToCosimplicialAugmented_map_left, simplicialToCosimplicialAugmented_map_right, simplicialToCosimplicialAugmented_obj	212
Total	275

CategoryTheory

Definitions

Name	Category	Theorems
CosimplicialObject 📖	CompOp	90 math math: CosimplicialObject.Augmented.leftOpRightOpIso_hom_left, CosimplicialObject.whiskering_obj_obj_obj, CosimplicialObject.comp_app, CosimplicialObject.id_right_app, CosimplicialObject.instHasColimitsOfShape, Idempotents.instIsIdempotentCompleteCosimplicialObject, CosimplicialObject.augment_right, Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj, cosimplicialSimplicialEquiv_counitIso_hom_app_app, CosimplicialObject.Augmented.leftOp_right, simplicialCosimplicialEquiv_counitIso_inv_app_app, simplicialCosimplicialEquiv_inverse_map, Arrow.mapAugmentedCechConerve_right, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, CosimplicialObject.augment_hom_app, Limits.FormalCoproduct.cochainComplexFunctor_map_f, CosimplicialObject.Augmented.const_obj_right, CosimplicialObject.instHasColimits, CosimplicialObject.id_app, CosimplicialObject.instHasLimitsOfShape, CosimplicialObject.comp_right_app, simplicialToCosimplicialAugmented_map_left, CosimplicialObject.Augmented.leftOpRightOpIso_inv_left, cosimplicialSimplicialEquiv_functor_obj_obj, simplicialCosimplicialEquiv_unitIso_hom_app, CosimplicialObject.Augmented.whiskering_map_app_left, simplicialCosimplicialEquiv_counitIso_hom_app_app, CosimplicialObject.Augmented.leftOp_left_map, cosimplicialSimplicialEquiv_inverse_obj, CosimplicialObject.Augmented.drop_obj, SimplicialObject.Augmented.rightOp_right_map, CosimplicialObject.Augmented.toArrow_map_right, CosimplicialObject.Augmented.const_map_right, cosimplicialSimplicialEquiv_functor_map_app, cosimplicialSimplicialEquiv_counitIso_inv_app_app, CosimplicialObject.Augmented.toArrow_map_left, Limits.FormalCoproduct.cochainComplexFunctor_obj_d, Arrow.mapAugmentedCechConerve_left, SimplicialObject.Augmented.rightOp_right_obj, CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app, cosimplicialSimplicialEquiv_unitIso_hom_app, CosimplicialObject.Augmented.toArrow_obj_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, CosimplicialObject.augment_hom_zero, CosimplicialObject.Augmented.toArrow_obj_right, CosimplicialObject.Augmented.toArrow_obj_hom, cosimplicialSimplicialEquiv_unitIso_inv_app, AlgebraicTopology.alternatingCofaceMapComplex_obj, simplicialCosimplicialEquiv_inverse_obj, simplicialCosimplicialEquiv_functor_map_app, CosimplicialObject.cechConerve_map, CosimplicialObject.Augmented.const_map_left, CosimplicialObject.augment_left, CosimplicialObject.Augmented.hom_ext_iff, CosimplicialObject.Augmented.const_obj_hom, CosimplicialObject.whiskering_obj_map_app, CosimplicialObject.Augmented.point_map, Arrow.augmentedCechConerve_right, simplicialCosimplicialEquiv_unitIso_inv_app, CosimplicialObject.equivalenceRightToLeft_right_app, SimplicialObject.Augmented.rightOp_hom_app, Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map, CosimplicialObject.Augmented.leftOp_left_obj, SimplicialObject.Augmented.rightOp_left, CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app, CosimplicialObject.whiskering_map_app_app, CosimplicialObject.equivalenceLeftToRight_left, AlgebraicTopology.alternatingCofaceMapComplex_map, CosimplicialObject.Augmented.whiskering_map_app_right, simplicialCosimplicialEquiv_functor_obj_obj, simplicialToCosimplicialAugmented_map_right, CosimplicialObject.whiskering_obj_obj_map, CosimplicialObject.Augmented.leftOp_hom_app, CosimplicialObject.instHasLimits, cosimplicialToSimplicialAugmented_map, CosimplicialObject.equivalenceRightToLeft_left, cosimplicialSimplicialEquiv_inverse_map, CosimplicialObject.cechConerve_obj, CosimplicialObject.equivalenceLeftToRight_right, Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, CosimplicialObject.Augmented.const_obj_left, cosimplicialSimplicialEquiv_functor_obj_map, CosimplicialObject.comp_left, CosimplicialObject.Augmented.point_obj, Arrow.augmentedCechConerve_left, simplicialCosimplicialEquiv_functor_obj_map, Arrow.augmentedCechConerve_hom_app, CosimplicialObject.id_left, CosimplicialObject.Augmented.drop_map
cosimplicialSimplicialEquiv 📖	CompOp	10 math math: cosimplicialSimplicialEquiv_counitIso_hom_app_app, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, cosimplicialSimplicialEquiv_functor_obj_obj, cosimplicialSimplicialEquiv_inverse_obj, cosimplicialSimplicialEquiv_functor_map_app, cosimplicialSimplicialEquiv_counitIso_inv_app_app, cosimplicialSimplicialEquiv_unitIso_hom_app, cosimplicialSimplicialEquiv_unitIso_inv_app, cosimplicialSimplicialEquiv_inverse_map, cosimplicialSimplicialEquiv_functor_obj_map
cosimplicialToSimplicialAugmented 📖	CompOp	3 math math: cosimplicialToSimplicialAugmented_obj, simplicialCosimplicialAugmentedEquiv_inverse, cosimplicialToSimplicialAugmented_map
instCategorySimplicialObject 📖	CompOp	245 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, SimplicialObject.id_left_app, SimplicialObject.whiskering_obj_map_app, AlgebraicTopology.DoldKan.N₁_map_f, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, Arrow.augmentedCechNerve_hom_app, SimplicialObject.comp_right, SimplicialObject.Augmented.point_map, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.identity_N₂, cosimplicialSimplicialEquiv_counitIso_hom_app_app, CosimplicialObject.Augmented.leftOp_right, simplicialCosimplicialEquiv_counitIso_inv_app_app, simplicialCosimplicialEquiv_inverse_map, SimplicialObject.Augmented.toArrow_map_right, SimplicialObject.opFunctor_obj_σ, Preadditive.DoldKan.equivalence_unitIso, SimplicialObject.augment_left, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, SimplicialObject.Truncated.cosk.full, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, SimplicialObject.opFunctor_obj_map, SimplicialObject.Split.forget_obj, Arrow.mapAugmentedCechNerve_left, Preadditive.DoldKan.equivalence_functor, SimplicialObject.Augmented.w₀, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, SimplicialObject.Augmented.toArrow_map_left, AlgebraicTopology.alternatingFaceMapComplex_obj_d, SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε, SimplicialObject.Augmented.toArrow_obj_left, SimplicialObject.Truncated.cosk.faithful, SimplicialObject.Split.forget_map, SimplicialObject.Split.comp_F, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, AlgebraicTopology.DoldKan.N₁_obj_p, SimplicialObject.opFunctor_map_app, Preadditive.DoldKan.equivalence_counitIso, SimplicialObject.Augmented.rightOpLeftOpIso_inv_right, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, AlgebraicTopology.alternatingFaceMapComplex_map_f, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ, SimplicialObject.Augmented.const_obj_hom, Idempotents.DoldKan.hε, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, SimplicialObject.opEquivalence_counitIso, SimplicialObject.Augmented.whiskering_map_app_right, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, simplicialToCosimplicialAugmented_map_left, AlgebraicTopology.DoldKan.map_Hσ, id_app, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, SSet.Augmented.stdSimplex_map_right, AlgebraicTopology.DoldKan.Γ₀_obj_map, cosimplicialSimplicialEquiv_functor_obj_obj, SimplicialObject.Augmented.const_map_left, simplicialCosimplicialEquiv_unitIso_hom_app, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, SSet.Augmented.stdSimplex_obj_left, SimplicialObject.Augmented.const_obj_right, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, Idempotents.instIsIdempotentCompleteSimplicialObject, Idempotents.DoldKan.equivalence_counitIso, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, simplicialCosimplicialEquiv_counitIso_hom_app_app, CosimplicialObject.Augmented.leftOp_left_map, cosimplicialSimplicialEquiv_inverse_obj, SimplicialObject.isoCoskOfIsCoskeletal_hom, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, SimplicialObject.instHasLimitsOfShape, SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, AlgebraicTopology.inclusionOfMooreComplex_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, SimplicialObject.augment_right, SimplicialObject.augment_hom_zero, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, SimplicialObject.Augmented.rightOp_right_map, Idempotents.DoldKan.equivalence_inverse, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, SimplicialObject.Splitting.ofIso_isColimit', SimplicialObject.Truncated.sk.full, cosimplicialSimplicialEquiv_functor_map_app, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, Limits.FormalCoproduct.cechFunctor_obj, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, SimplicialObject.Augmented.hom_ext_iff, AlgebraicTopology.DoldKan.map_PInfty_f, SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, cosimplicialSimplicialEquiv_counitIso_inv_app_app, SimplicialObject.augment_hom_app, SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SSet.Augmented.stdSimplex_obj_right, AlgebraicTopology.normalizedMooreComplex_objD, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, SimplicialObject.Splitting.ofIso_ι, SimplicialObject.opFunctor_obj_δ, SimplicialObject.Augmented.const_map_right, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, AlgebraicTopology.normalizedMooreComplex_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, AlgebraicTopology.DoldKan.Γ₀_map_app, SimplicialObject.comp_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, SimplicialObject.whiskering_map_app_app, SimplicialObject.Augmented.rightOp_right_obj, SimplicialObject.Augmented.rightOpLeftOpIso_hom_right, Limits.FormalCoproduct.cechFunctor_map_app, cosimplicialSimplicialEquiv_unitIso_hom_app, AlgebraicTopology.DoldKan.map_P, Arrow.augmentedCechNerve_left, Idempotents.DoldKan.η_inv_app_f, SimplicialObject.Augmented.whiskering_map_app_left, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, SimplicialObject.Augmented.drop_obj, SimplicialObject.equivalenceRightToLeft_right, comp_app, SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁, SimplicialObject.cechNerve_obj, AlgebraicTopology.DoldKan.natTransP_app, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.map_alternatingFaceMapComplex, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀_obj_obj, cosimplicialSimplicialEquiv_unitIso_inv_app, SimplicialObject.opFunctorCompOpFunctorIso_hom_app_app, Arrow.augmentedCechNerve_right, SimplicialObject.Augmented.w₀_assoc, SimplicialObject.cechNerve_map, SimplicialObject.whiskering_obj_obj_obj, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc, SimplicialObject.opEquivalence_unitIso, Idempotents.DoldKan.Γ_obj_map, SimplicialObject.Augmented.const_obj_left, simplicialCosimplicialEquiv_inverse_obj, AlgebraicTopology.DoldKan.natTransPInfty_f_app, Idempotents.DoldKan.Γ_obj_obj, simplicialCosimplicialEquiv_functor_map_app, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, SSet.Augmented.stdSimplex_obj_hom_app, SimplicialObject.whiskering_obj_obj_map, Abelian.DoldKan.equivalence_inverse, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, SimplicialObject.instHasColimitsOfShape, SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc, SimplicialObject.equivalenceRightToLeft_left, SimplicialObject.opFunctorCompOpFunctorIso_inv_app_app, SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀, SimplicialObject.Augmented.ExtraDegeneracy.const_s, simplicialCosimplicialEquiv_unitIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, Preadditive.DoldKan.equivalence_inverse, AlgebraicTopology.DoldKan.map_Q, SimplicialObject.Truncated.cosk_reflective, AlgebraicTopology.DoldKan.N₂_obj_p_f, AlgebraicTopology.DoldKan.N₂_obj_X_X, Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, SimplicialObject.Augmented.rightOp_hom_app, SimplicialObject.Augmented.point_obj, SimplicialObject.Split.natTransCofanInj_app, CosimplicialObject.Augmented.leftOp_left_obj, SimplicialObject.Augmented.rightOp_left, SimplicialObject.Truncated.sk_coreflective, SSet.Augmented.stdSimplex_map_left, Idempotents.DoldKan.equivalence_functor, SimplicialObject.Truncated.sk.faithful, AlgebraicTopology.DoldKan.N₂_obj_X_d, SimplicialObject.Augmented.toArrow_obj_hom, SimplicialObject.opEquivalence_inverse, Abelian.DoldKan.equivalence_functor, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, AlgebraicTopology.DoldKan.karoubi_PInfty_f, simplicialCosimplicialEquiv_functor_obj_obj, Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, SimplicialObject.id_right, SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, simplicialToCosimplicialAugmented_map_right, CosimplicialObject.Augmented.leftOp_hom_app, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, cosimplicialToSimplicialAugmented_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, Abelian.DoldKan.comparisonN_hom_app_f, SimplicialObject.Augmented.drop_map, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, cosimplicialSimplicialEquiv_inverse_map, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₂_map_f_app, SimplicialObject.isCoskeletal_iff_isIso, SimplicialObject.augmentedCechNerve_obj_right, SimplicialObject.augmentedCechNerve_map_left_app, AlgebraicTopology.DoldKan.Γ₂N₁_inv, SimplicialObject.augmentedCechNerve_obj_left_map, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, SimplicialObject.opEquivalence_functor, AlgebraicTopology.DoldKan.identity_N₂_objectwise, AlgebraicTopology.inclusionOfMooreComplexMap_f, Idempotents.DoldKan.hη, SimplicialObject.augmentedCechNerve_obj_left_obj, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, AlgebraicTopology.alternatingFaceMapComplex_obj_X, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, SimplicialObject.Split.id_F, AlgebraicTopology.DoldKan.map_hσ', AlgebraicTopology.DoldKan.N₂_map_f_f, SimplicialObject.instHasLimits, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, AlgebraicTopology.DoldKan.N₁Γ₀_app, cosimplicialSimplicialEquiv_functor_obj_map, Idempotents.DoldKan.N_map, Abelian.DoldKan.comparisonN_inv_app_f, SimplicialObject.equivalenceLeftToRight_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, SimplicialObject.augmentedCechNerve_obj_hom_app, SimplicialObject.augmentedCechNerve_map_right, Arrow.mapAugmentedCechNerve_right, AlgebraicTopology.DoldKan.Γ₂N₂_inv, Idempotents.DoldKan.η_hom_app_f, AlgebraicTopology.normalizedMooreComplex_obj, simplicialCosimplicialEquiv_functor_obj_map, AlgebraicTopology.DoldKan.natTransQ_app, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, SimplicialObject.instHasColimits, SimplicialObject.equivalenceLeftToRight_right, Idempotents.DoldKan.equivalence_unitIso
simplicialCosimplicialAugmentedEquiv 📖	CompOp	2 math math: simplicialCosimplicialAugmentedEquiv_inverse, simplicialCosimplicialAugmentedEquiv_functor
simplicialCosimplicialEquiv 📖	CompOp	9 math math: simplicialCosimplicialEquiv_counitIso_inv_app_app, simplicialCosimplicialEquiv_inverse_map, simplicialCosimplicialEquiv_unitIso_hom_app, simplicialCosimplicialEquiv_counitIso_hom_app_app, simplicialCosimplicialEquiv_inverse_obj, simplicialCosimplicialEquiv_functor_map_app, simplicialCosimplicialEquiv_unitIso_inv_app, simplicialCosimplicialEquiv_functor_obj_obj, simplicialCosimplicialEquiv_functor_obj_map
simplicialToCosimplicialAugmented 📖	CompOp	4 math math: simplicialToCosimplicialAugmented_map_left, simplicialToCosimplicialAugmented_obj, simplicialToCosimplicialAugmented_map_right, simplicialCosimplicialAugmentedEquiv_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_app 📖	mathematical	—	NatTrans.app Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory CategoryStruct.comp SimplicialObject Category.toCategoryStruct instCategorySimplicialObject Functor.obj	—	—
cosimplicialSimplicialEquiv_counitIso_hom_app_app 📖	mathematical	—	NatTrans.app Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.obj Functor Functor.category Functor.comp Functor.opInv Functor.opHom Functor.id Iso.hom Equivalence.counitIso CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv CategoryStruct.id Category.toCategoryStruct	—	—
cosimplicialSimplicialEquiv_counitIso_inv_app_app 📖	mathematical	—	NatTrans.app Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.obj Functor Functor.category Functor.id Functor.comp Functor.opInv Functor.opHom Iso.inv Equivalence.counitIso CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv CategoryStruct.id Category.toCategoryStruct	—	—
cosimplicialSimplicialEquiv_functor_map_app 📖	mathematical	—	NatTrans.app Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.op Opposite.unop Functor Functor.map Functor.category Equivalence.functor CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj Quiver.Hom.unop	—	—
cosimplicialSimplicialEquiv_functor_obj_map 📖	mathematical	—	Functor.map Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.obj Functor Functor.category Equivalence.functor CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Quiver.Hom.unop	—	—
cosimplicialSimplicialEquiv_functor_obj_obj 📖	mathematical	—	Functor.obj Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor Functor.category Equivalence.functor CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Opposite.op Opposite.unop	—	—
cosimplicialSimplicialEquiv_inverse_map 📖	mathematical	—	Functor.map Functor Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.category Equivalence.inverse CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Functor.unop Quiver.Hom.unop Functor.obj Opposite.op NatTrans.app	—	—
cosimplicialSimplicialEquiv_inverse_obj 📖	mathematical	—	Functor.obj Functor Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.category Equivalence.inverse CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Opposite.op Functor.unop	—	—
cosimplicialSimplicialEquiv_unitIso_hom_app 📖	mathematical	—	NatTrans.app Opposite Functor SimplexCategory SimplexCategory.smallCategory Category.opposite Functor.category Functor.id Functor.comp Functor.opHom Functor.opInv Iso.hom Equivalence.unitIso CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Functor.unop Functor.op Opposite.unop Functor.opUnopIso	—	—
cosimplicialSimplicialEquiv_unitIso_inv_app 📖	mathematical	—	NatTrans.app Opposite Functor SimplexCategory SimplexCategory.smallCategory Category.opposite Functor.category Functor.comp Functor.opHom Functor.opInv Functor.id Iso.inv Equivalence.unitIso CosimplicialObject SimplicialObject CosimplicialObject.instCategory instCategorySimplicialObject cosimplicialSimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Functor.unop Functor.op Functor.opUnopIso	—	—
cosimplicialToSimplicialAugmented_map 📖	mathematical	—	Functor.map CosimplicialObject.Augmented Opposite Category.opposite CosimplicialObject.instCategoryAugmented SimplicialObject.Augmented SimplicialObject.instCategoryAugmented cosimplicialToSimplicialAugmented Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct CosimplicialObject.Augmented.leftOp SimplicialObject instCategorySimplicialObject Functor.id SimplicialObject.const NatTrans.leftOp SimplexCategory SimplexCategory.smallCategory Comma.right CosimplicialObject CosimplicialObject.instCategory CosimplicialObject.const CommaMorphism.right Quiver.Hom.unop Comma.left CommaMorphism.left	—	—
cosimplicialToSimplicialAugmented_obj 📖	mathematical	—	Functor.obj CosimplicialObject.Augmented Opposite Category.opposite CosimplicialObject.instCategoryAugmented SimplicialObject.Augmented SimplicialObject.instCategoryAugmented cosimplicialToSimplicialAugmented Opposite.op CosimplicialObject.Augmented.leftOp	—	—
id_app 📖	mathematical	—	NatTrans.app Opposite SimplexCategory Category.opposite SimplexCategory.smallCategory CategoryStruct.id SimplicialObject Category.toCategoryStruct instCategorySimplicialObject Functor.obj	—	—
simplicialCosimplicialAugmentedEquiv_functor 📖	mathematical	—	Equivalence.functor Opposite SimplicialObject.Augmented CosimplicialObject.Augmented Category.opposite SimplicialObject.instCategoryAugmented CosimplicialObject.instCategoryAugmented simplicialCosimplicialAugmentedEquiv simplicialToCosimplicialAugmented	—	—
simplicialCosimplicialAugmentedEquiv_inverse 📖	mathematical	—	Equivalence.inverse Opposite SimplicialObject.Augmented CosimplicialObject.Augmented Category.opposite SimplicialObject.instCategoryAugmented CosimplicialObject.instCategoryAugmented simplicialCosimplicialAugmentedEquiv cosimplicialToSimplicialAugmented	—	—
simplicialCosimplicialEquiv_counitIso_hom_app_app 📖	mathematical	—	NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.obj Functor Functor.category Functor.comp Opposite.op Functor.leftOp Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct NatTrans.leftOp Functor.rightOp Opposite.unop NatTrans.rightOp Quiver.Hom.unop Functor.id Iso.hom Equivalence.counitIso SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv CategoryStruct.id	—	—
simplicialCosimplicialEquiv_counitIso_inv_app_app 📖	mathematical	—	NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.obj Functor Functor.category Functor.id Functor.comp Opposite.op Functor.leftOp Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct NatTrans.leftOp Functor.rightOp Opposite.unop NatTrans.rightOp Quiver.Hom.unop Iso.inv Equivalence.counitIso SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv CategoryStruct.id	—	—
simplicialCosimplicialEquiv_functor_map_app 📖	mathematical	—	NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.rightOp Opposite.unop Functor Functor.map Functor.category Equivalence.functor SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj Opposite.op Quiver.Hom.unop	—	—
simplicialCosimplicialEquiv_functor_obj_map 📖	mathematical	—	Functor.map SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.obj Functor Functor.category Equivalence.functor SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Opposite.op	—	—
simplicialCosimplicialEquiv_functor_obj_obj 📖	mathematical	—	Functor.obj SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor Functor.category Equivalence.functor SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Opposite.op Opposite.unop	—	—
simplicialCosimplicialEquiv_inverse_map 📖	mathematical	—	Functor.map Functor SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.category Equivalence.inverse SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Functor.leftOp NatTrans.leftOp	—	—
simplicialCosimplicialEquiv_inverse_obj 📖	mathematical	—	Functor.obj Functor SimplexCategory SimplexCategory.smallCategory Opposite Category.opposite Functor.category Equivalence.inverse SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Opposite.op Functor.leftOp	—	—
simplicialCosimplicialEquiv_unitIso_hom_app 📖	mathematical	—	NatTrans.app Opposite Functor SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.category Functor.id Functor.comp Functor.rightOp Opposite.unop NatTrans.rightOp Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Opposite.op Functor.leftOp Quiver.Hom.op NatTrans.leftOp Iso.hom Equivalence.unitIso SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Functor.rightOpLeftOpIso	—	—
simplicialCosimplicialEquiv_unitIso_inv_app 📖	mathematical	—	NatTrans.app Opposite Functor SimplexCategory Category.opposite SimplexCategory.smallCategory Functor.category Functor.comp Functor.rightOp Opposite.unop NatTrans.rightOp Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct Opposite.op Functor.leftOp Quiver.Hom.op NatTrans.leftOp Functor.id Iso.inv Equivalence.unitIso SimplicialObject CosimplicialObject instCategorySimplicialObject CosimplicialObject.instCategory simplicialCosimplicialEquiv Functor.rightOpLeftOpIso	—	—
simplicialToCosimplicialAugmented_map_left 📖	mathematical	—	CommaMorphism.left Opposite Category.opposite CosimplicialObject CosimplicialObject.instCategory CosimplicialObject.const Functor.id SimplicialObject.Augmented.rightOp Opposite.unop SimplicialObject.Augmented Functor.map SimplicialObject.instCategoryAugmented CosimplicialObject.Augmented CosimplicialObject.instCategoryAugmented simplicialToCosimplicialAugmented Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct Comma.right SimplicialObject instCategorySimplicialObject SimplicialObject.const CommaMorphism.right Quiver.Hom.unop	—	—
simplicialToCosimplicialAugmented_map_right 📖	mathematical	—	CommaMorphism.right Opposite Category.opposite CosimplicialObject CosimplicialObject.instCategory CosimplicialObject.const Functor.id SimplicialObject.Augmented.rightOp Opposite.unop SimplicialObject.Augmented Functor.map SimplicialObject.instCategoryAugmented CosimplicialObject.Augmented CosimplicialObject.instCategoryAugmented simplicialToCosimplicialAugmented NatTrans.rightOp SimplexCategory SimplexCategory.smallCategory Comma.left SimplicialObject instCategorySimplicialObject SimplicialObject.const CommaMorphism.left Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct	—	—
simplicialToCosimplicialAugmented_obj 📖	mathematical	—	Functor.obj Opposite SimplicialObject.Augmented Category.opposite SimplicialObject.instCategoryAugmented CosimplicialObject.Augmented CosimplicialObject.instCategoryAugmented simplicialToCosimplicialAugmented SimplicialObject.Augmented.rightOp Opposite.unop	—	—

CategoryTheory.CosimplicialObject

Definitions

Name	Category	Theorems
augment 📖	CompOp	4 math math: augment_right, augment_hom_app, augment_hom_zero, augment_left
const 📖	CompOp	49 math math: Augmented.leftOpRightOpIso_hom_left, id_right_app, augment_right, Augmented.leftOp_right, CategoryTheory.Arrow.mapAugmentedCechConerve_right, augment_hom_app, Augmented.const_obj_right, comp_right_app, CategoryTheory.simplicialToCosimplicialAugmented_map_left, Augmented.leftOpRightOpIso_inv_left, Augmented.whiskering_map_app_left, Augmented.leftOp_left_map, Augmented.drop_obj, CategoryTheory.SimplicialObject.Augmented.rightOp_right_map, Augmented.toArrow_map_right, Augmented.const_map_right, Augmented.toArrow_map_left, CategoryTheory.Arrow.mapAugmentedCechConerve_left, CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj, Augmented.leftOpRightOpIso_hom_right_app, Augmented.toArrow_obj_left, augment_hom_zero, Augmented.toArrow_obj_right, Augmented.toArrow_obj_hom, Augmented.const_map_left, augment_left, Augmented.hom_ext_iff, Augmented.const_obj_hom, Augmented.point_map, CategoryTheory.Arrow.augmentedCechConerve_right, equivalenceRightToLeft_right_app, CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app, Augmented.leftOp_left_obj, CategoryTheory.SimplicialObject.Augmented.rightOp_left, Augmented.leftOpRightOpIso_inv_right_app, equivalenceLeftToRight_left, Augmented.whiskering_map_app_right, CategoryTheory.simplicialToCosimplicialAugmented_map_right, Augmented.leftOp_hom_app, CategoryTheory.cosimplicialToSimplicialAugmented_map, equivalenceRightToLeft_left, equivalenceLeftToRight_right, Augmented.const_obj_left, comp_left, Augmented.point_obj, CategoryTheory.Arrow.augmentedCechConerve_left, CategoryTheory.Arrow.augmentedCechConerve_hom_app, id_left, Augmented.drop_map
eqToIso 📖	CompOp	1 math math: eqToIso_refl
instCategory 📖	CompOp	90 math math: Augmented.leftOpRightOpIso_hom_left, whiskering_obj_obj_obj, comp_app, id_right_app, instHasColimitsOfShape, CategoryTheory.Idempotents.instIsIdempotentCompleteCosimplicialObject, augment_right, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app, Augmented.leftOp_right, CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app, CategoryTheory.simplicialCosimplicialEquiv_inverse_map, CategoryTheory.Arrow.mapAugmentedCechConerve_right, AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d, augment_hom_app, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, Augmented.const_obj_right, instHasColimits, id_app, instHasLimitsOfShape, comp_right_app, CategoryTheory.simplicialToCosimplicialAugmented_map_left, Augmented.leftOpRightOpIso_inv_left, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj, CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app, Augmented.whiskering_map_app_left, CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app, Augmented.leftOp_left_map, CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj, Augmented.drop_obj, CategoryTheory.SimplicialObject.Augmented.rightOp_right_map, Augmented.toArrow_map_right, Augmented.const_map_right, CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app, CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app, Augmented.toArrow_map_left, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CategoryTheory.Arrow.mapAugmentedCechConerve_left, CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj, Augmented.leftOpRightOpIso_hom_right_app, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app, Augmented.toArrow_obj_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, augment_hom_zero, Augmented.toArrow_obj_right, Augmented.toArrow_obj_hom, CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.simplicialCosimplicialEquiv_inverse_obj, CategoryTheory.simplicialCosimplicialEquiv_functor_map_app, cechConerve_map, Augmented.const_map_left, augment_left, Augmented.hom_ext_iff, Augmented.const_obj_hom, whiskering_obj_map_app, Augmented.point_map, CategoryTheory.Arrow.augmentedCechConerve_right, CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app, equivalenceRightToLeft_right_app, CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map, Augmented.leftOp_left_obj, CategoryTheory.SimplicialObject.Augmented.rightOp_left, Augmented.leftOpRightOpIso_inv_right_app, whiskering_map_app_app, equivalenceLeftToRight_left, AlgebraicTopology.alternatingCofaceMapComplex_map, Augmented.whiskering_map_app_right, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj, CategoryTheory.simplicialToCosimplicialAugmented_map_right, whiskering_obj_obj_map, Augmented.leftOp_hom_app, instHasLimits, CategoryTheory.cosimplicialToSimplicialAugmented_map, equivalenceRightToLeft_left, CategoryTheory.cosimplicialSimplicialEquiv_inverse_map, cechConerve_obj, equivalenceLeftToRight_right, CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, Augmented.const_obj_left, CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map, comp_left, Augmented.point_obj, CategoryTheory.Arrow.augmentedCechConerve_left, CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map, CategoryTheory.Arrow.augmentedCechConerve_hom_app, id_left, Augmented.drop_map
instCategoryAugmented 📖	CompOp	63 math math: Augmented.leftOpRightOpIso_hom_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_left, id_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_map_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, Augmented.const_obj_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_map, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_inverse_obj_obj, comp_right_app, CategoryTheory.simplicialToCosimplicialAugmented_map_left, Augmented.leftOpRightOpIso_inv_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_left, Augmented.whiskering_map_app_left, cechConerveEquiv_symm_apply, Augmented.drop_obj, augmentedCechConerve_obj, Augmented.toArrow_map_right, Augmented.const_map_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, Augmented.toArrow_map_left, Augmented.leftOpRightOpIso_hom_right_app, Augmented.toArrow_obj_left, CategoryTheory.cosimplicialToSimplicialAugmented_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, Augmented.toArrow_obj_right, Augmented.toArrow_obj_hom, Augmented.const_map_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, augmentedCechConerve_map, Augmented.const_obj_hom, Augmented.point_map, equivalenceRightToLeft_right_app, CategoryTheory.simplicialToCosimplicialAugmented_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, Augmented.leftOpRightOpIso_inv_right_app, equivalenceLeftToRight_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, Augmented.whiskering_map_app_right, CategoryTheory.simplicialToCosimplicialAugmented_map_right, CategoryTheory.simplicialCosimplicialAugmentedEquiv_inverse, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app, CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_map, CategoryTheory.cosimplicialToSimplicialAugmented_map, equivalenceRightToLeft_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, Augmented.whiskering_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_map_right_app, equivalenceLeftToRight_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, Augmented.const_obj_left, cechConerveEquiv_apply, comp_left, Augmented.point_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_inv_app_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, id_left, Augmented.drop_map
instCategoryTruncated 📖	CompOp	8 math math: Truncated.whiskering_obj_obj_obj, Truncated.whiskering_map_app_app, Truncated.whiskering_obj_map_app, Truncated.instHasColimits, Truncated.instHasLimitsOfShape, Truncated.instHasColimitsOfShape, Truncated.instHasLimits, Truncated.whiskering_obj_obj_map
truncation 📖	CompOp	—
truncationCompTrunc 📖	CompOp	—
whiskering 📖	CompOp	4 math math: whiskering_obj_obj_obj, whiskering_obj_map_app, whiskering_map_app_app, whiskering_obj_obj_map
δ 📖	CompOp	55 math math: δ_comp_δ_self_assoc, SSet.PtSimplex.RelStruct.δ_map_of_lt, δ_comp_δ_self', δ_comp_δ''_assoc, δ_comp_δ_assoc, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ, δ_comp_δ', SSet.PtSimplex.MulStruct.δ_map_of_gt, δ_comp_σ_self', SSet.PtSimplex.RelStruct.δ_castSucc_map, δ_comp_σ_self_assoc, δ_comp_δ, SSet.stdSimplex.range_δ, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ι_eq_δ_assoc, δ_naturality_assoc, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, δ_comp_σ_succ_assoc, δ_comp_σ_of_gt_assoc, δ_comp_σ_succ'_assoc, δ_comp_δ_self'_assoc, δ_comp_σ_of_le, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ, δ_comp_δ_self, SSet.stdSimplex.faceSingletonComplIso_hom_ι, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, δ_comp_σ_succ', SSet.PtSimplex.MulStruct.δ_map_of_lt, SSet.horn₂₁.isPushout, δ_comp_σ_succ, δ_comp_δ'', δ_comp_σ_of_gt'_assoc, δ_comp_σ_of_gt, δ_comp_δ'_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, δ_comp_σ_self, SSet.horn₂₀.isPushout, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, SSet.stdSimplex.faceSingletonComplIso_hom_ι_assoc, SSet.horn₂₂.isPushout, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc, SSet.PtSimplex.RelStruct.δ_succ_map, δ_naturality, SSet.horn.ι_ι_assoc, SSet.PtSimplex.RelStruct.δ_map_of_gt, SSet.horn.ι_ι, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SimplexCategory.II_δ, δ_comp_σ_of_gt', δ_comp_σ_self'_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map, δ_comp_σ_of_le_assoc
σ 📖	CompOp	19 math math: σ_naturality_assoc, SimplexCategory.II_σ, δ_comp_σ_self', δ_comp_σ_self_assoc, σ_naturality, δ_comp_σ_succ_assoc, δ_comp_σ_of_gt_assoc, δ_comp_σ_succ'_assoc, δ_comp_σ_of_le, δ_comp_σ_succ', δ_comp_σ_succ, σ_comp_σ, δ_comp_σ_of_gt'_assoc, δ_comp_σ_of_gt, σ_comp_σ_assoc, δ_comp_σ_self, δ_comp_σ_of_gt', δ_comp_σ_self'_assoc, δ_comp_σ_of_le_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
augment_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id CategoryTheory.Comma.hom augment SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	—	—
augment_hom_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.map	CategoryTheory.NatTrans.app CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Comma.left CategoryTheory.Functor.id augment CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	SimplexCategory.const_eq_id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
augment_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.map	CategoryTheory.Comma.left CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id augment	—	—
augment_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.map	CategoryTheory.Comma.right CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id augment	—	—
comp_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CosimplicialObject CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj	—	—
comp_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id CategoryTheory.CategoryStruct.comp Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Comma.left	—	—
comp_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.CategoryStruct.comp Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Functor.obj	—	—
eqToIso_refl 📖	mathematical	—	eqToIso CategoryTheory.Iso.refl CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory	—	CategoryTheory.Functor.mapIso_refl
hom_ext 📖	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory	—	—	CategoryTheory.NatTrans.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory	—	hom_ext
id_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.CategoryStruct.id CategoryTheory.CosimplicialObject CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj	—	—
id_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id CategoryTheory.CategoryStruct.id Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Comma.left	—	—
id_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Comma.right CategoryTheory.CosimplicialObject instCategory const CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.CategoryStruct.id Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Functor.obj	—	—
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.CosimplicialObject instCategory	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.CosimplicialObject instCategory	—	CategoryTheory.Limits.functorCategoryHasColimitsOfShape
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.CosimplicialObject instCategory	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.CosimplicialObject instCategory	—	CategoryTheory.Limits.functorCategoryHasLimitsOfShape
whiskering_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.map CategoryTheory.CosimplicialObject instCategory whiskering	—	—
whiskering_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject instCategory whiskering	—	—
whiskering_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CosimplicialObject instCategory whiskering	—	—
whiskering_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CosimplicialObject instCategory whiskering	—	—
δ_comp_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ
δ_comp_δ' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ'
δ_comp_δ'' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ''
δ_comp_δ''_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ''
δ_comp_δ'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ'
δ_comp_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ
δ_comp_δ_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ_self
δ_comp_δ_self' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	δ_comp_δ_self
δ_comp_δ_self'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ_self'
δ_comp_δ_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ_self
δ_comp_σ_of_gt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_gt
δ_comp_σ_of_gt' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instPartialOrder covariant_swap_add_of_covariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instLinearOrder lt_of_lt_of_le Nat.instPreorder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le lt_of_lt_of_le CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_gt'
δ_comp_σ_of_gt'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instPartialOrder covariant_swap_add_of_covariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instLinearOrder lt_of_lt_of_le Nat.instPreorder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le lt_of_lt_of_le CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_gt'
δ_comp_σ_of_gt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_gt
δ_comp_σ_of_le 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_le
δ_comp_σ_of_le_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_le
δ_comp_σ_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_self CategoryTheory.Functor.map_id
δ_comp_σ_self' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ CategoryTheory.CategoryStruct.id	—	δ_comp_σ_self
δ_comp_σ_self'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_self'
δ_comp_σ_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_self
δ_comp_σ_succ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_succ CategoryTheory.Functor.map_id
δ_comp_σ_succ' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ CategoryTheory.CategoryStruct.id	—	δ_comp_σ_succ
δ_comp_σ_succ'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_succ'
δ_comp_σ_succ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ σ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_succ
δ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
δ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory δ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_naturality
σ_comp_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory σ	—	CategoryTheory.Functor.map_comp SimplexCategory.σ_comp_σ
σ_comp_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_comp_σ
σ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory σ CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
σ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory σ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_naturality

CategoryTheory.CosimplicialObject.Augmented

Definitions

Name	Category	Theorems
const 📖	CompOp	5 math math: const_obj_right, const_map_right, const_map_left, const_obj_hom, const_obj_left
drop 📖	CompOp	7 math math: drop_obj, toArrow_map_right, toArrow_map_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_hom_app_app, whiskering_map_app_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompDropIso_inv_app_app, drop_map
leftOp 📖	CompOp	14 math math: leftOpRightOpIso_hom_left, leftOp_right, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_right, leftOpRightOpIso_inv_left, leftOp_left_map, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app, CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_right, leftOpRightOpIso_hom_right_app, CategoryTheory.cosimplicialToSimplicialAugmented_obj, leftOp_left_obj, leftOpRightOpIso_inv_right_app, leftOp_hom_app, CategoryTheory.cosimplicialToSimplicialAugmented_map
leftOpRightOpIso 📖	CompOp	4 math math: leftOpRightOpIso_hom_left, leftOpRightOpIso_inv_left, leftOpRightOpIso_hom_right_app, leftOpRightOpIso_inv_right_app
point 📖	CompOp	7 math math: AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app, whiskering_map_app_left, toArrow_map_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_inv_app, toArrow_map_left, point_map, point_obj
toArrow 📖	CompOp	15 math math: CategoryTheory.CosimplicialObject.cechConerveEquiv_symm_apply, toArrow_map_right, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_right, toArrow_map_left, toArrow_obj_left, toArrow_obj_right, toArrow_obj_hom, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_inv_app_left, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.CosimplicialObject.equivalenceRightToLeft_left, AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompToArrowIso_hom_app_right, CategoryTheory.CosimplicialObject.equivalenceLeftToRight_right, CategoryTheory.CosimplicialObject.cechConerveEquiv_apply
whiskering 📖	CompOp	3 math math: whiskering_map_app_left, whiskering_map_app_right, whiskering_obj
whiskeringObj 📖	CompOp	3 math math: whiskering_map_app_left, whiskering_map_app_right, whiskering_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented const	—	—
const_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented const	—	—
const_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
const_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented const	—	—
const_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented const	—	—
drop_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory drop CategoryTheory.CommaMorphism.right CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id	—	—
drop_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory drop CategoryTheory.Comma.right CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id	—	—
hom_ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	—	CategoryTheory.Comma.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	hom_ext
leftOpRightOpIso_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left Opposite CategoryTheory.Category.opposite CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.SimplicialObject.Augmented.rightOp leftOp CategoryTheory.Iso.hom CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented leftOpRightOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
leftOpRightOpIso_hom_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.SimplicialObject.Augmented.rightOp leftOp CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented leftOpRightOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
leftOpRightOpIso_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left Opposite CategoryTheory.Category.opposite CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.SimplicialObject.Augmented.rightOp leftOp CategoryTheory.Iso.inv CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented leftOpRightOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left	—	—
leftOpRightOpIso_inv_right_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.SimplicialObject.Augmented.rightOp leftOp CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented leftOpRightOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
leftOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.leftOp CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.CosimplicialObject.const CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const leftOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop	—	—
leftOp_left_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const leftOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const Opposite.unop	—	—
leftOp_left_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const leftOp Opposite.unop CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const	—	—
leftOp_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const leftOp Opposite.unop CategoryTheory.Comma.left Opposite CategoryTheory.Category.opposite CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const	—	—
point_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented point CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id	—	—
point_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented point CategoryTheory.Comma.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id	—	—
toArrow_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented point SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory drop CategoryTheory.NatTrans.app CategoryTheory.CosimplicialObject.const CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow	—	—
toArrow_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented point SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory drop CategoryTheory.NatTrans.app CategoryTheory.CosimplicialObject.const CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow	—	—
toArrow_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Comma.left CategoryTheory.Comma.right	—	—
toArrow_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const	—	—
toArrow_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow SimplexCategory SimplexCategory.smallCategory CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const	—	—
whiskering_map_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented whiskeringObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category whiskering point	—	—
whiskering_map_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented whiskeringObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category whiskering CategoryTheory.Functor.whiskerLeft SimplexCategory SimplexCategory.smallCategory drop	—	—
whiskering_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CosimplicialObject.Augmented CategoryTheory.CosimplicialObject.instCategoryAugmented whiskering whiskeringObj	—	—

CategoryTheory.CosimplicialObject.Truncated

Definitions

Name	Category	Theorems
mkNotation 📖	CompOp	—
trunc 📖	CompOp	—
whiskering 📖	CompOp	4 math math: whiskering_obj_obj_obj, whiskering_map_app_app, whiskering_obj_map_app, whiskering_obj_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated	—	CategoryTheory.Limits.functorCategoryHasColimitsOfShape
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated	—	CategoryTheory.Limits.functorCategoryHasLimitsOfShape
whiskering_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory.Truncated CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.map CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory.Truncated CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory.Truncated CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory.Truncated CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.CosimplicialObject.Truncated CategoryTheory.CosimplicialObject.instCategoryTruncated whiskering	—	—

CategoryTheory.SimplicialObject

Definitions

Name	Category	Theorems
augment 📖	CompOp	4 math math: augment_left, augment_right, augment_hom_zero, augment_hom_app
const 📖	CompOp	81 math math: id_left_app, CategoryTheory.Arrow.augmentedCechNerve_hom_app, comp_right, Augmented.point_map, CategoryTheory.CosimplicialObject.Augmented.leftOp_right, Augmented.toArrow_map_right, augment_left, Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, CategoryTheory.Arrow.mapAugmentedCechNerve_left, Augmented.w₀, Augmented.toArrow_map_left, Augmented.ExtraDegeneracy.s'_comp_ε, Augmented.rightOpLeftOpIso_inv_right, Augmented.ExtraDegeneracy.s_comp_δ, Augmented.const_obj_hom, Augmented.whiskering_map_app_right, CategoryTheory.simplicialToCosimplicialAugmented_map_left, SSet.Augmented.stdSimplex_map_right, Augmented.const_map_left, SSet.Augmented.stdSimplex_obj_left, Augmented.const_obj_right, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, augment_right, augment_hom_zero, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, Augmented.rightOp_right_map, Augmented.hom_ext_iff, Augmented.rightOpLeftOpIso_inv_left_app, augment_hom_app, Augmented.rightOpLeftOpIso_hom_left_app, SSet.Augmented.stdSimplex_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, Augmented.const_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, comp_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, Augmented.rightOp_right_obj, Augmented.rightOpLeftOpIso_hom_right, CategoryTheory.Arrow.augmentedCechNerve_left, Augmented.whiskering_map_app_left, Augmented.ExtraDegeneracy.s_comp_σ, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, Augmented.drop_obj, equivalenceRightToLeft_right, Augmented.ExtraDegeneracy.s₀_comp_δ₁, Augmented.ExtraDegeneracy.s_comp_δ_assoc, CategoryTheory.Arrow.augmentedCechNerve_right, Augmented.w₀_assoc, Augmented.ExtraDegeneracy.s_comp_σ_assoc, Augmented.const_obj_left, SSet.Augmented.stdSimplex_obj_hom_app, Augmented.ExtraDegeneracy.s'_comp_ε_assoc, equivalenceRightToLeft_left, Augmented.ExtraDegeneracy.s_comp_δ₀, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, Augmented.rightOp_hom_app, Augmented.point_obj, CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj, Augmented.rightOp_left, SSet.Augmented.stdSimplex_map_left, Augmented.toArrow_obj_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, id_right, CategoryTheory.simplicialToCosimplicialAugmented_map_right, CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app, CategoryTheory.cosimplicialToSimplicialAugmented_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, Augmented.drop_map, augmentedCechNerve_obj_right, augmentedCechNerve_map_left_app, augmentedCechNerve_obj_left_map, augmentedCechNerve_obj_left_obj, equivalenceLeftToRight_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, augmentedCechNerve_obj_hom_app, augmentedCechNerve_map_right, CategoryTheory.Arrow.mapAugmentedCechNerve_right, equivalenceLeftToRight_right
cosk 📖	CompOp	2 math math: instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, isoCoskOfIsCoskeletal_hom
coskAdj 📖	CompOp	5 math math: instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, isoCoskOfIsCoskeletal_hom, instIsIsoAppUnitTruncatedCoskAdj, Truncated.cosk_reflective, isCoskeletal_iff_isIso
diagonal 📖	CompOp	—
eqToIso 📖	CompOp	1 math math: eqToIso_refl
instCategoryAugmented 📖	CompOp	89 math math: id_left_app, comp_right, Augmented.point_map, Augmented.toArrow_map_right, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, Augmented.w₀, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_map_app, Augmented.toArrow_map_left, Augmented.ExtraDegeneracy.s'_comp_ε, Augmented.toArrow_obj_left, Augmented.ExtraDegeneracy.const_s', Augmented.rightOpLeftOpIso_inv_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, Augmented.toArrow_obj_right, Augmented.ExtraDegeneracy.s_comp_δ, Augmented.const_obj_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, Augmented.whiskering_map_app_right, CategoryTheory.simplicialToCosimplicialAugmented_map_left, Augmented.whiskering_obj, SSet.Augmented.stdSimplex_map_right, Augmented.const_map_left, SSet.Augmented.stdSimplex_obj_left, Augmented.const_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, SSet.Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, Augmented.rightOpLeftOpIso_inv_left_app, Augmented.rightOpLeftOpIso_hom_left_app, SSet.Augmented.stdSimplex_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_right, Augmented.const_map_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_map_left_app, comp_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_right, Augmented.rightOpLeftOpIso_hom_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, Augmented.whiskering_map_app_left, Augmented.ExtraDegeneracy.s_comp_σ, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, CategoryTheory.cosimplicialToSimplicialAugmented_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app, Augmented.drop_obj, equivalenceRightToLeft_right, Augmented.ExtraDegeneracy.s₀_comp_δ₁, Augmented.ExtraDegeneracy.s_comp_δ_assoc, Augmented.w₀_assoc, Augmented.ExtraDegeneracy.s_comp_σ_assoc, cechNerveEquiv_symm_apply, Augmented.const_obj_left, SSet.Augmented.stdSimplex_obj_hom_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, Augmented.ExtraDegeneracy.s'_comp_ε_assoc, equivalenceRightToLeft_left, Augmented.ExtraDegeneracy.s_comp_δ₀, Augmented.ExtraDegeneracy.const_s, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, CategoryTheory.simplicialToCosimplicialAugmented_obj, Augmented.point_obj, SSet.Augmented.stdSimplex_map_left, Augmented.toArrow_obj_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, cechNerveEquiv_apply, id_right, CategoryTheory.simplicialToCosimplicialAugmented_map_right, CategoryTheory.simplicialCosimplicialAugmentedEquiv_inverse, CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor, CategoryTheory.cosimplicialToSimplicialAugmented_map, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map, Augmented.drop_map, augmentedCechNerve_obj_right, augmentedCechNerve_map_left_app, augmentedCechNerve_obj_left_map, augmentedCechNerve_obj_left_obj, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map, equivalenceLeftToRight_left_app, AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_obj, augmentedCechNerve_obj_hom_app, augmentedCechNerve_map_right, equivalenceLeftToRight_right
instCategoryTruncated 📖	CompOp	22 math math: Truncated.instHasLimits, Truncated.whiskering_obj_obj_obj, Truncated.whiskering_map_app_app, Truncated.cosk.full, instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, Truncated.instHasColimits, Truncated.cosk.faithful, Truncated.trunc_obj_obj, isoCoskOfIsCoskeletal_hom, Truncated.sk.full, instIsIsoAppUnitTruncatedCoskAdj, Truncated.trunc_obj_map, Truncated.trunc_map_app, Truncated.instHasLimitsOfShape, Truncated.whiskering_obj_obj_map, Truncated.cosk_reflective, Truncated.sk_coreflective, Truncated.sk.faithful, instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, isCoskeletal_iff_isIso, Truncated.instHasColimitsOfShape, Truncated.whiskering_obj_map_app
sk 📖	CompOp	1 math math: instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation
skAdj 📖	CompOp	2 math math: Truncated.sk_coreflective, instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation
truncation 📖	CompOp	7 math math: instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, isoCoskOfIsCoskeletal_hom, instIsIsoAppUnitTruncatedCoskAdj, Truncated.cosk_reflective, Truncated.sk_coreflective, instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation, isCoskeletal_iff_isIso
truncationCompTrunc 📖	CompOp	—
whiskering 📖	CompOp	10 math math: whiskering_obj_map_app, AlgebraicTopology.DoldKan.map_Hσ, AlgebraicTopology.DoldKan.map_PInfty_f, whiskering_map_app_app, AlgebraicTopology.DoldKan.map_P, AlgebraicTopology.map_alternatingFaceMapComplex, whiskering_obj_obj_obj, whiskering_obj_obj_map, AlgebraicTopology.DoldKan.map_Q, AlgebraicTopology.DoldKan.map_hσ'
δ 📖	CompOp	87 math math: SSet.δ_comp_σ_self'_apply, SSet.op_δ, δ_comp_δ_self_assoc, δ_comp_δ''_assoc, AlgebraicTopology.NormalizedMooreComplex.obj_d, δ_comp_σ_of_gt, SSet.Edge.CompStruct.d₀, SSet.Edge.tgt_eq, SSet.StrictSegal.spine_δ_arrow_eq, CategoryTheory.nerve.δ₂_zero, SSet.δ_comp_σ_succ'_apply, Augmented.ExtraDegeneracy.s_comp_δ₀_assoc, SSet.Subcomplex.PairingCore.surjective', δ_comp_σ_succ'_assoc, δ_def, δ_comp_δ_assoc, SSet.δ_naturality_apply, SSet.prodStdSimplex.objEquiv_δ_apply, Augmented.ExtraDegeneracy.s_comp_δ, SSet.StrictSegal.spine_δ_arrow_lt, SSet.δ_comp_σ_of_gt_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, SSet.spine_δ₀, δ_comp_σ_self'_assoc, δ_naturality, SSet.δ_comp_σ_succ_apply, Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc, SSet.Edge.mk'_edge, δ_comp_σ_of_gt'_assoc, δ_comp_δ'_assoc, δ_comp_σ_self', AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero, SSet.Path.arrow_tgt, δ_comp_δ', δ_comp_σ_succ', AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, SimplicialObject.opFunctor_obj_δ, δ_comp_δ'', δ_comp_δ_self, CategoryTheory.nerve.δ₁_mk₂_eq, SSet.Subcomplex.PairingCore.type₂_simplex, SSet.Edge.CompStruct.d₂, Augmented.ExtraDegeneracy.s₀_comp_δ₁, δ_comp_σ_of_le, δ_comp_σ_self, SSet.δ_comp_σ_self_apply, δ_comp_σ_of_gt_assoc, SSet.Edge.CompStruct.d₁, Augmented.ExtraDegeneracy.s_comp_δ_assoc, SSet.Subcomplex.PairingCore.nonDegenerate₂, δ_naturality_assoc, CategoryTheory.nerve.δ_obj, δ_comp_σ_succ, CategoryTheory.nerve.δ₂_mk₂_eq, SSet.δ_comp_σ_of_le_apply, SSet.Path.arrow_src, Augmented.ExtraDegeneracy.s_comp_δ₀, δ_comp_σ_of_gt', SSet.StrictSegal.spine_δ_arrow_gt, δ_comp_σ_self_assoc, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, δ_comp_δ_self', AlgebraicTopology.DoldKan.N₂_obj_X_d, SSet.δ_comp_δ''_apply, SSet.δ_comp_δ'_apply, SSet.δ_comp_σ_of_gt'_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, SSet.StrictSegalCore.δ₀_spineToSimplex, SSet.S.IsUniquelyCodimOneFace.δ_eq_iff, δ_comp_σ_of_le_assoc, δ_comp_δ, AlgebraicTopology.DoldKan.decomposition_Q, SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, SSet.Subcomplex.PairingCore.notMem₂, SSet.δ_comp_δ_apply, SSet.StrictSegal.spine_δ_vertex_lt, CategoryTheory.nerve.δ₀_eq, CategoryTheory.nerve.δ₀_mk₂_eq, SSet.S.IsUniquelyCodimOneFace.iff, δ_comp_σ_succ_assoc, SSet.S.IsUniquelyCodimOneFace.δ_index, SSet.StrictSegal.spine_δ_vertex_ge, SSet.δ_comp_δ_self_apply, CategoryTheory.nerve.δ₂_two, SSet.δ_comp_δ_self'_apply, δ_comp_δ_self'_assoc, SSet.Edge.src_eq
σ 📖	CompOp	52 math math: SSet.δ_comp_σ_self'_apply, CategoryTheory.nerve.σ_obj, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, δ_comp_σ_of_gt, σ_naturality_assoc, SSet.σ_mem_degenerate, SimplicialObject.opFunctor_obj_σ, SSet.δ_comp_σ_succ'_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_σ, σ_naturality, δ_comp_σ_succ'_assoc, SSet.op_σ, SSet.δ_comp_σ_of_gt_apply, δ_comp_σ_self'_assoc, σ_def, SSet.δ_comp_σ_succ_apply, δ_comp_σ_of_gt'_assoc, δ_comp_σ_self', PartialOrder.mem_range_nerve_σ_iff, SSet.Edge.CompStruct.idComp_simplex, δ_comp_σ_succ', σ_comp_σ, Augmented.ExtraDegeneracy.s_comp_σ, δ_comp_σ_of_le, CategoryTheory.nerve.σ₀_mk₀_eq, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, δ_comp_σ_self, SSet.δ_comp_σ_self_apply, δ_comp_σ_of_gt_assoc, Augmented.ExtraDegeneracy.s_comp_σ_assoc, δ_comp_σ_succ, SSet.δ_comp_σ_of_le_apply, AlgebraicTopology.DoldKan.hσ'_eq, CategoryTheory.nerve.σ_zero_nerveEquiv_symm, δ_comp_σ_of_gt', AlgebraicTopology.DoldKan.σ_comp_PInfty, δ_comp_σ_self_assoc, SSet.σ_comp_σ_apply, SSet.Edge.CompStruct.compId_simplex, σ_comp_σ_assoc, SSet.δ_comp_σ_of_gt'_apply, SSet.degenerate_eq_iUnion_range_σ, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, δ_comp_σ_of_le_assoc, SSet.σ_naturality_apply, AlgebraicTopology.DoldKan.decomposition_Q, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, AlgebraicTopology.DoldKan.MorphComponents.id_b, δ_comp_σ_succ_assoc, AlgebraicTopology.DoldKan.hσ'_eq', SSet.Edge.id_edge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
augment_hom_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const CategoryTheory.Comma.hom augment Opposite.unop SimplexCategory.const SimplexCategory.len SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat	—	—
augment_hom_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.NatTrans.app CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.Comma.left const augment CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	SimplexCategory.const_eq_id CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
augment_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const augment	—	—
augment_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const augment	—	—
comp_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const CategoryTheory.CommaMorphism.left CategoryTheory.CategoryStruct.comp Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Functor.obj	—	—
comp_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const CategoryTheory.CategoryStruct.comp Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Comma.right	—	—
eqToIso_refl 📖	mathematical	—	eqToIso CategoryTheory.Iso.refl CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op	—	CategoryTheory.Functor.mapIso_refl
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	—	CategoryTheory.NatTrans.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory	—	hom_ext
id_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const CategoryTheory.CommaMorphism.left CategoryTheory.CategoryStruct.id Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Functor.obj	—	—
id_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id const CategoryTheory.CategoryStruct.id Augmented CategoryTheory.Category.toCategoryStruct instCategoryAugmented CategoryTheory.Comma.right	—	—
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject	—	CategoryTheory.Limits.functorCategoryHasColimitsOfShape
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject	—	CategoryTheory.Limits.functorCategoryHasLimitsOfShape
instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion	CategoryTheory.Functor.IsLeftKanExtension CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject sk Truncated instCategoryTruncated CategoryTheory.Functor.id truncation CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Truncated.sk CategoryTheory.Adjunction.unit skAdj	—	CategoryTheory.Functor.lanAdjunction_unit CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit
instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation 📖	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.Functor.IsRightKanExtension CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject cosk Truncated instCategoryTruncated CategoryTheory.Functor.id truncation CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Truncated.cosk CategoryTheory.Adjunction.counit coskAdj	—	CategoryTheory.Functor.ranAdjunction_counit CategoryTheory.Functor.instIsRightKanExtensionObjRanAppRanCounit
whiskering_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.map CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject whiskering	—	—
whiskering_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject whiskering	—	—
whiskering_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject whiskering	—	—
whiskering_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject whiskering	—	—
δ_comp_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ
δ_comp_δ' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ'
δ_comp_δ'' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ''
δ_comp_δ''_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ Fin.le_iff_val_le_val	—	Fin.le_iff_val_le_val CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ''
δ_comp_δ'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ'
δ_comp_δ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ
δ_comp_δ_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_δ_self
δ_comp_δ_self' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	δ_comp_δ_self
δ_comp_δ_self'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ_self'
δ_comp_δ_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_δ_self
δ_comp_σ_of_gt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_gt
δ_comp_σ_of_gt' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instPartialOrder covariant_swap_add_of_covariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instLinearOrder lt_of_lt_of_le Nat.instPreorder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le lt_of_lt_of_le CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_gt'
δ_comp_σ_of_gt'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instPartialOrder covariant_swap_add_of_covariant_add Preorder.toLE PartialOrder.toPreorder Nat.instAddCommSemigroup IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instLinearOrder lt_of_lt_of_le Nat.instPreorder	—	add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le lt_of_lt_of_le CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_gt'
δ_comp_σ_of_gt_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_gt
δ_comp_σ_of_le 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_of_le
δ_comp_σ_of_le_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_of_le
δ_comp_σ_self 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_self CategoryTheory.Functor.map_id
δ_comp_σ_self' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ CategoryTheory.CategoryStruct.id	—	δ_comp_σ_self
δ_comp_σ_self'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_self'
δ_comp_σ_self_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_self
δ_comp_σ_succ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.map_comp SimplexCategory.δ_comp_σ_succ CategoryTheory.Functor.map_id
δ_comp_σ_succ' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ CategoryTheory.CategoryStruct.id	—	δ_comp_σ_succ
δ_comp_σ_succ'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_succ'
δ_comp_σ_succ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ δ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' δ_comp_σ_succ
δ_def 📖	mathematical	—	δ CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.δ	—	—
δ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
δ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op δ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_naturality
σ_comp_σ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ	—	CategoryTheory.Functor.map_comp SimplexCategory.σ_comp_σ
σ_comp_σ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_comp_σ
σ_def 📖	mathematical	—	σ CategoryTheory.Functor.map Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SimplexCategory.σ	—	—
σ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
σ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory Opposite.op σ CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' σ_naturality

CategoryTheory.SimplicialObject.Augmented

Definitions

Name	Category	Theorems
const 📖	CompOp	7 math math: ExtraDegeneracy.const_s', const_obj_hom, const_map_left, const_obj_right, const_map_right, const_obj_left, ExtraDegeneracy.const_s
drop 📖	CompOp	23 math math: toArrow_map_right, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, ExtraDegeneracy.s_comp_δ₀_assoc, w₀, toArrow_map_left, ExtraDegeneracy.s'_comp_ε, toArrow_obj_left, ExtraDegeneracy.s_comp_δ, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, ExtraDegeneracy.s₀_comp_δ₁_assoc, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app, whiskering_map_app_left, ExtraDegeneracy.s_comp_σ, drop_obj, ExtraDegeneracy.s₀_comp_δ₁, ExtraDegeneracy.s_comp_δ_assoc, w₀_assoc, ExtraDegeneracy.s_comp_σ_assoc, ExtraDegeneracy.s'_comp_ε_assoc, ExtraDegeneracy.s_comp_δ₀, ExtraDegeneracy.const_s, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_inv_app_app, drop_map
point 📖	CompOp	15 math math: point_map, toArrow_map_right, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, w₀, toArrow_map_left, ExtraDegeneracy.s'_comp_ε, ExtraDegeneracy.const_s', toArrow_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_inv_app, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso_hom_app, whiskering_map_app_right, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, w₀_assoc, ExtraDegeneracy.s'_comp_ε_assoc, point_obj
rightOp 📖	CompOp	15 math math: CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_left, rightOpLeftOpIso_inv_right, CategoryTheory.simplicialToCosimplicialAugmented_map_left, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_left, rightOp_right_map, rightOpLeftOpIso_inv_left_app, rightOpLeftOpIso_hom_left_app, rightOp_right_obj, rightOpLeftOpIso_hom_right, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app, CategoryTheory.simplicialToCosimplicialAugmented_obj, rightOp_hom_app, rightOp_left, CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app, CategoryTheory.simplicialToCosimplicialAugmented_map_right
rightOpLeftOpIso 📖	CompOp	4 math math: rightOpLeftOpIso_inv_right, rightOpLeftOpIso_inv_left_app, rightOpLeftOpIso_hom_left_app, rightOpLeftOpIso_hom_right
toArrow 📖	CompOp	15 math math: toArrow_map_right, toArrow_map_left, toArrow_obj_left, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left, toArrow_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_right, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_hom_app_left, CategoryTheory.SimplicialObject.equivalenceRightToLeft_right, CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply, AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_right, CategoryTheory.SimplicialObject.equivalenceRightToLeft_left, toArrow_obj_hom, CategoryTheory.SimplicialObject.cechNerveEquiv_apply, CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app, CategoryTheory.SimplicialObject.equivalenceLeftToRight_right
whiskering 📖	CompOp	3 math math: whiskering_map_app_right, whiskering_obj, whiskering_map_app_left
whiskeringObj 📖	CompOp	3 math math: whiskering_map_app_right, whiskering_obj, whiskering_map_app_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented const	—	—
const_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented const	—	—
const_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
const_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented const	—	—
const_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented const	—	—
drop_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const	—	—
drop_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const	—	—
hom_ext 📖	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CommaMorphism.right	—	—	CategoryTheory.Comma.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CommaMorphism.right	—	hom_ext
point_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented point CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const	—	—
point_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented point CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const	—	—
rightOpLeftOpIso_hom_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CosimplicialObject.Augmented.leftOp rightOp CategoryTheory.CommaMorphism.left CategoryTheory.Iso.hom CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented rightOpLeftOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
rightOpLeftOpIso_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CosimplicialObject.Augmented.leftOp rightOp CategoryTheory.Iso.hom CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented rightOpLeftOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
rightOpLeftOpIso_inv_left_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CosimplicialObject.Augmented.leftOp rightOp CategoryTheory.CommaMorphism.left CategoryTheory.Iso.inv CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented rightOpLeftOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
rightOpLeftOpIso_inv_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.CosimplicialObject.Augmented.leftOp rightOp CategoryTheory.Iso.inv CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented rightOpLeftOpIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
rightOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app SimplexCategory SimplexCategory.smallCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.Functor.obj CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const rightOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op	—	—
rightOp_left 📖	mathematical	—	CategoryTheory.Comma.left Opposite CategoryTheory.Category.opposite CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id rightOp Opposite.op CategoryTheory.Comma.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const	—	—
rightOp_right_map 📖	mathematical	—	CategoryTheory.Functor.map SimplexCategory SimplexCategory.smallCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id rightOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const Opposite.op	—	—
rightOp_right_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Comma.right CategoryTheory.CosimplicialObject CategoryTheory.CosimplicialObject.instCategory CategoryTheory.CosimplicialObject.const CategoryTheory.Functor.id rightOp Opposite.op CategoryTheory.Comma.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.const	—	—
toArrow_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop Opposite.op point CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow	—	—
toArrow_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop Opposite.op point CategoryTheory.NatTrans.app CategoryTheory.Comma.left CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow	—	—
toArrow_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Comma.left CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right Opposite.op	—	—
toArrow_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop Opposite.op	—	—
toArrow_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.Arrow CategoryTheory.instCategoryArrow toArrow point	—	—
whiskering_map_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented whiskeringObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category whiskering CategoryTheory.Functor.whiskerLeft Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory drop	—	—
whiskering_map_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.Functor.id CategoryTheory.SimplicialObject.const CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented whiskeringObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category whiskering point	—	—
whiskering_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented whiskering whiskeringObj	—	—
w₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop Opposite.op CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Comma.left CategoryTheory.Comma.hom point	—	CategoryTheory.congr_app CategoryTheory.CommaMorphism.w
w₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.SimplicialObject.Augmented CategoryTheory.SimplicialObject.instCategoryAugmented CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject drop Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.SimplicialObject.const CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom point	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₀

CategoryTheory.SimplicialObject.Truncated

Definitions

Name	Category	Theorems
cosk 📖	CompOp	7 math math: cosk.full, CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation, cosk.faithful, CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom, CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj, cosk_reflective, CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso
mkNotation 📖	CompOp	—
sk 📖	CompOp	4 math math: sk.full, sk_coreflective, sk.faithful, CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation
trunc 📖	CompOp	3 math math: trunc_obj_obj, trunc_obj_map, trunc_map_app
whiskering 📖	CompOp	4 math math: whiskering_obj_obj_obj, whiskering_map_app_app, whiskering_obj_obj_map, whiskering_obj_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cosk_reflective 📖	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.Functor.HasPointwiseRightKanExtension	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject cosk CategoryTheory.SimplicialObject.truncation CategoryTheory.Functor.id CategoryTheory.Adjunction.counit CategoryTheory.SimplicialObject.coskAdj	—	CategoryTheory.Functor.reflective' CategoryTheory.Functor.instFullOppositeOp CategoryTheory.ObjectProperty.full_ι CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.ObjectProperty.faithful_ι
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated	—	CategoryTheory.Limits.functorCategoryHasColimitsOfShape
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated	—	CategoryTheory.Limits.functorCategoryHasLimitsOfShape
sk_coreflective 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion CategoryTheory.Functor.HasPointwiseLeftKanExtension	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject sk CategoryTheory.SimplicialObject.truncation CategoryTheory.Adjunction.unit CategoryTheory.SimplicialObject.skAdj	—	CategoryTheory.Functor.coreflective' CategoryTheory.Functor.instFullOppositeOp CategoryTheory.ObjectProperty.full_ι CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.ObjectProperty.faithful_ι
trunc_map_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.incl CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated trunc Opposite.op CategoryTheory.Functor.obj Opposite.unop	—	—
trunc_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated trunc Opposite.op SimplexCategory.Truncated.incl Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
trunc_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated trunc Opposite.op SimplexCategory.Truncated.incl Opposite.unop	—	—
whiskering_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.map CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_map_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.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated whiskering	—	—
whiskering_obj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory.Truncated CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated whiskering	—	—

CategoryTheory.SimplicialObject.Truncated.cosk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	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.Functor.HasPointwiseRightKanExtension	CategoryTheory.Functor.Faithful CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Truncated.cosk	—	CategoryTheory.Functor.FullyFaithful.faithful
full 📖	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.Functor.HasPointwiseRightKanExtension	CategoryTheory.Functor.Full CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Truncated.cosk	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.SimplicialObject.Truncated.coskAdj

Definitions

Name	Category	Theorems
reflective 📖	CompOp	—

CategoryTheory.SimplicialObject.Truncated.sk

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion CategoryTheory.Functor.HasPointwiseLeftKanExtension	CategoryTheory.Functor.Faithful CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Truncated.sk	—	CategoryTheory.Functor.FullyFaithful.faithful
full 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite SimplexCategory.Truncated SimplexCategory CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category SimplexCategory.smallCategory SimplexCategory.len CategoryTheory.Functor.op SimplexCategory.Truncated.inclusion CategoryTheory.Functor.HasPointwiseLeftKanExtension	CategoryTheory.Functor.Full CategoryTheory.SimplicialObject.Truncated CategoryTheory.SimplicialObject.instCategoryTruncated CategoryTheory.SimplicialObject CategoryTheory.instCategorySimplicialObject CategoryTheory.SimplicialObject.Truncated.sk	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.SimplicialObject.Truncated.skAdj

Definitions

Name	Category	Theorems
coreflective 📖	CompOp	—

Simplicial

Definitions

Name	Category	Theorems
«term_^⦋_⦌» 📖	CompOp	—
«term__⦋_⦌» 📖	CompOp	—

---

← Back to Index