Augmented

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean

Statistics

Metric	Count
Definitions Augmented, Augmented, Augmented	3
Theorems	0
Total	3

CategoryTheory.CosimplicialObject

Definitions

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

CategoryTheory.SimplicialObject

Definitions

Name	Category	Theorems
Augmented 📖	CompOp	83 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, Augmented.const_map_left, Augmented.const_obj_right, AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_obj, 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, 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, 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, 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

SSet

Definitions

Name	Category	Theorems
Augmented 📖	CompOp	6 math math: Augmented.stdSimplex_map_right, Augmented.stdSimplex_obj_left, Augmented.StandardSimplex.nonempty_extraDegeneracy_stdSimplex, Augmented.stdSimplex_obj_right, Augmented.stdSimplex_obj_hom_app, Augmented.stdSimplex_map_left

---

← Back to Index