Documentation Verification Report

SimplicialObject

📁 Source: Mathlib/CategoryTheory/Idempotents/SimplicialObject.lean

Statistics

Metric	Count
Definitions `SimplicialObject`	1
Theorems `instIsIdempotentCompleteCosimplicialObject`, `instIsIdempotentCompleteSimplicialObject`	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
`SimplicialObject` 📖	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`

CategoryTheory.Idempotents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIdempotentCompleteCosimplicialObject` 📖	mathematical	—	`CategoryTheory.IsIdempotentComplete` `CategoryTheory.CosimplicialObject` `CategoryTheory.CosimplicialObject.instCategory`	—	`functor_category_isIdempotentComplete`
`instIsIdempotentCompleteSimplicialObject` 📖	mathematical	—	`CategoryTheory.IsIdempotentComplete` `CategoryTheory.SimplicialObject` `CategoryTheory.instCategorySimplicialObject`	—	`functor_category_isIdempotentComplete`

---

← Back to Index