Documentation Verification Report

ComposableArrows

📁 Source: Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean

Statistics

Metric	Count
Definitions `ComposableArrows`	1
Theorems `essSurj_mapComposableArrows`, `essSurj_mapComposableArrows_of_hasRightCalculusOfFractions`	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
`ComposableArrows` 📖	CompOp	111 math math: `Triangulated.SpectralObject.Hom.comm`, `HomotopyCategory.spectralObjectMappingCone_δ'_app`, `nerve.edgeMk_edge`, `ComposableArrows.opEquivalence_counitIso_inv_app_app`, `Functor.mapComposableArrowsObjMk₂Iso_inv_app`, `ComposableArrows.isoMk₁_hom_app`, `ComposableArrows.sc'MapIso_inv`, `ComposableArrows.isIso_iff₂`, `Triangulated.SpectralObject.ω₂_obj_distinguished`, `nerve.functorOfNerveMap_map`, `Functor.mapComposableArrowsObjMk₁Iso_inv_app`, `nerve.homEquiv_edgeMk_map_nerveMap`, `Triangulated.SpectralObject.ω₂_obj_mor₃`, `nerve.homEquiv_apply`, `nerve.edgeMk_id`, `nerve.right_edge`, `nerve.homEquiv_edgeMk`, `Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions`, `ComposableArrows.opEquivalence_unitIso_inv_app`, `nerve.nonempty_compStruct_iff`, `ComposableArrows.isoMk₅_inv`, `Triangulated.SpectralObject.ω₂_map_hom₁`, `ComposableArrows.whiskerLeftFunctor_obj_map`, `nerve.homEquiv_comp`, `Triangulated.SpectralObject.triangle_obj₂`, `nerve.left_edge`, `nerve.mk₁_homEquiv_apply`, `ComposableArrows.isoMk₄_hom`, `ShortComplex.SnakeInput.composableArrowsFunctor_map`, `ComposableArrows.opEquivalence_functor_obj_map`, `ComposableArrows.δ₀Functor_obj_map`, `ComposableArrows.whiskerLeftFunctor_obj_obj`, `ComposableArrows.opEquivalence_functor_map_app`, `Functor.mapComposableArrowsObjMk₂Iso_hom_app`, `ComposableArrows.sc'MapIso_hom`, `ComposableArrows.opEquivalence_inverse_obj`, `HomotopyCategory.composableArrowsFunctor_obj`, `ComposableArrows.arrowEquiv_symm_apply`, `ComposableArrows.scMapIso_inv`, `ComposableArrows.opEquivalence_unitIso_hom_app`, `ComposableArrows.mapFunctorArrows_app`, `ShortComplex.mapToComposableArrows_comp`, `Functor.mapComposableArrowsObjMk₁Iso_hom_app`, `Functor.mapComposableArrows_obj_map`, `ComposableArrows.isoMk₂_inv`, `Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁`, `Triangulated.SpectralObject.triangle_mor₂`, `nerve.homEquiv_id`, `SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk`, `ComposableArrows.isoMk_inv`, `Triangulated.SpectralObject.Hom.comm_assoc`, `Triangulated.SpectralObject.ω₂_obj_mor₂`, `Triangulated.SpectralObject.id_hom`, `ComposableArrows.δlastFunctor_obj_obj`, `ComposableArrows.scMapIso_hom`, `ComposableArrows.opEquivalence_functor_obj_obj`, `Triangulated.SpectralObject.distinguished'`, `Triangulated.SpectralObject.triangle_mor₁`, `ComposableArrows.isoMk₃_hom`, `ComposableArrows.whiskerLeftFunctor_map_app`, `ComposableArrows.δlastFunctor_map_app`, `HomotopyCategory.composableArrowsFunctor_map`, `Triangulated.SpectralObject.mapTriangulatedFunctor_δ`, `ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀`, `nerve_obj`, `ComposableArrows.isoMk₅_hom`, `nerve.σ_zero_nerveEquiv_symm`, `ComposableArrows.isoMk₀_inv_app`, `Triangulated.SpectralObject.comp_hom`, `ComposableArrows.isoMk_hom`, `ComposableArrows.isIso_iff₀`, `Triangulated.SpectralObject.mapTriangulatedFunctor_δ'`, `ShortComplex.SnakeInput.composableArrowsFunctor_obj`, `ComposableArrows.isoMk₂_hom`, `ComposableArrows.isoMk₃_inv`, `HomotopyCategory.spectralObjectMappingCone_ω₁`, `ComposableArrows.opEquivalence_inverse_map`, `Functor.mapComposableArrows_obj_obj`, `ComposableArrows.arrowEquiv_apply`, `ComposableArrows.δ₀Functor_obj_obj`, `ComposableArrows.isoMk₁_inv_app`, `Triangulated.SpectralObject.ω₂_map_hom₂`, `SSet.OneTruncation₂.nerveHomEquiv_apply`, `Triangulated.SpectralObject.triangle_obj₃`, `ComposableArrows.isoMk₄_inv`, `Triangulated.SpectralObject.comp_hom_assoc`, `HomologicalComplex.HomologySequence.composableArrows₃Functor_map`, `Triangulated.SpectralObject.ω₂_obj_obj₂`, `SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero`, `Triangulated.SpectralObject.triangle_obj₁`, `ComposableArrows.δ₀Functor_map_app`, `HomologicalComplex.HomologySequence.composableArrows₃Functor_obj`, `ComposableArrows.isoMk₀_hom_app`, `ComposableArrows.functorArrows_map`, `nerveMap_app`, `Triangulated.SpectralObject.ω₂_obj_mor₁`, `nerve.functorOfNerveMap_obj`, `Triangulated.SpectralObject.ω₂_map_hom₃`, `ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁`, `ComposableArrows.opEquivalence_counitIso_hom_app_app`, `ComposableArrows.functorArrows_obj`, `SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk`, `ShortComplex.mapToComposableArrows_id`, `Triangulated.SpectralObject.ω₂_obj_obj₁`, `Localization.essSurj_mapComposableArrows`, `ComposableArrows.isIso_iff₁`, `nerve.edgeMk_surjective`, `Triangulated.SpectralObject.ω₂_obj_obj₃`, `ComposableArrows.δlastFunctor_obj_map`, `nerve.homEquiv_symm_apply`, `Functor.mapComposableArrows_map_app`

CategoryTheory.Localization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essSurj_mapComposableArrows` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.mapComposableArrows`	—	`essSurj_mapComposableArrows_of_hasRightCalculusOfFractions` `CategoryTheory.Functor.IsLocalization.op` `CategoryTheory.MorphismProperty.instHasRightCalculusOfFractionsOppositeOpOfHasLeftCalculusOfFractions` `CategoryTheory.Functor.essSurj_of_iso` `CategoryTheory.Functor.essSurj_comp` `CategoryTheory.Functor.instEssSurjOppositeRightOp` `CategoryTheory.Equivalence.essSurj_functor` `CategoryTheory.Functor.instEssSurjOppositeOp` `CategoryTheory.Functor.essSurj_of_comp_fully_faithful` `CategoryTheory.Functor.rightOp_faithful` `CategoryTheory.Equivalence.faithful_functor` `CategoryTheory.Functor.rightOp_full` `CategoryTheory.Equivalence.full_functor`
`essSurj_mapComposableArrows_of_hasRightCalculusOfFractions` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.Functor.mapComposableArrows`	—	`essSurj` `CategoryTheory.ComposableArrows.mk₀_surjective` `CategoryTheory.Functor.EssSurj.mem_essImage` `CategoryTheory.ComposableArrows.precomp_surjective` `inverts` `exists_rightFraction` `CategoryTheory.MorphismProperty.RightFraction.hs` `CategoryTheory.Category.assoc` `CategoryTheory.cancel_mono` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map`

---

← Back to Index