Basic

📁 Source: Mathlib/CategoryTheory/ComposableArrows/Basic.lean

Statistics

Metric	Count
Definitions map, obj, map, obj, app', arrow, arrowEquiv, hom, homMk, homMkSucc, homMk₀, homMk₁, homMk₂, homMk₃, homMk₄, homMk₅, isoMk, isoMkSucc, isoMk₀, isoMk₁, isoMk₂, isoMk₃, isoMk₄, isoMk₅, left, map', mkOfObjOfMapSucc, mk₀, mk₁, mk₂, mk₃, mk₄, mk₅, obj', opEquivalence, precomp, right, tacticValid, whiskerLeft, whiskerLeftFunctor, δlast, δlastFunctor, δ₀, δ₀Functor, mapComposableArrows, mapComposableArrowsObjMk₁Iso, mapComposableArrowsObjMk₂Iso, mapComposableArrowsOpIso, castSuccFunctor, succFunctor	50
Theorems map_comp, map_id, map_comp, map_id, map_one_one, map_one_succ, map_succ_succ, map_zero_one, map_zero_one', map_zero_succ_succ, map_zero_zero, obj_one, obj_succ, obj_zero, arrowEquiv_apply, arrowEquiv_symm_apply, ext, ext_succ, ext₀, ext₁, ext₂, ext₂_of_arrow, ext₃, ext₄, ext₅, homMkSucc_app_succ, homMkSucc_app_zero, homMk_app, homMk₀_app, homMk₁_app, homMk₂_app_one, homMk₂_app_two, homMk₂_app_two', homMk₂_app_zero, homMk₃_app_one, homMk₃_app_three, homMk₃_app_two, homMk₃_app_zero, homMk₄_app_four, homMk₄_app_one, homMk₄_app_three, homMk₄_app_two, homMk₄_app_zero, homMk₅_app_five, homMk₅_app_four, homMk₅_app_one, homMk₅_app_three, homMk₅_app_two, homMk₅_app_zero, hom_ext_succ, hom_ext₀, hom_ext₀_iff, hom_ext₁, hom_ext₁_iff, hom_ext₂, hom_ext₂_iff, hom_ext₃, hom_ext₃_iff, hom_ext₄, hom_ext₄_iff, hom_ext₅, hom_ext₅_iff, isIso_iff₀, isIso_iff₁, isIso_iff₂, isoMkSucc_hom, isoMkSucc_inv, isoMk_hom, isoMk_inv, isoMk₀_hom_app, isoMk₀_inv_app, isoMk₁_hom_app, isoMk₁_inv_app, isoMk₂_hom, isoMk₂_inv, isoMk₃_hom, isoMk₃_inv, isoMk₄_hom, isoMk₄_inv, isoMk₅_hom, isoMk₅_inv, map'_comp, map'_eq_hom₁, map'_inv_eq_inv_map', map'_self, mkOfObjOfMapSucc_arrow, mkOfObjOfMapSucc_exists, mkOfObjOfMapSucc_map_succ, mkOfObjOfMapSucc_obj, mk₀_map, mk₀_obj, mk₀_surjective, mk₁_comp_eqToHom, mk₁_eqToHom_comp, mk₁_hom, mk₁_map, mk₁_obj, mk₁_surjective, mk₂_surjective, mk₃_surjective, mk₄_surjective, mk₅_surjective, naturality', naturality'_assoc, opEquivalence_counitIso_hom_app_app, opEquivalence_counitIso_inv_app_app, opEquivalence_functor_map_app, opEquivalence_functor_obj_map, opEquivalence_functor_obj_obj, opEquivalence_inverse_map, opEquivalence_inverse_obj, opEquivalence_unitIso_hom_app, opEquivalence_unitIso_inv_app, precomp_map, precomp_obj, precomp_surjective, precomp_δ₀, whiskerLeftFunctor_map_app, whiskerLeftFunctor_obj_map, whiskerLeftFunctor_obj_obj, whiskerLeft_map, whiskerLeft_obj, δlastFunctor_map_app, δlastFunctor_obj_map, δlastFunctor_obj_obj, δ₀Functor_map_app, δ₀Functor_obj_map, δ₀Functor_obj_obj, mapComposableArrowsObjMk₁Iso_hom_app, mapComposableArrowsObjMk₁Iso_inv_app, mapComposableArrowsObjMk₂Iso_hom_app, mapComposableArrowsObjMk₂Iso_inv_app, mapComposableArrows_map_app, mapComposableArrows_obj_map, mapComposableArrows_obj_obj, castSuccFunctor_map, castSuccFunctor_obj, succFunctor_map, succFunctor_obj	139
Total	189

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
app' 📖	CompOp	22 math math: hom_ext₅_iff, CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono', CategoryTheory.Abelian.mono_of_epi_of_epi_mono', CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi, hom_ext₃_iff, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, CategoryTheory.Abelian.isIso_of_isIso_of_mono, naturality', CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono, homMkSucc_app_succ, hom_ext₁_iff, hom_ext₂_iff, CategoryTheory.Abelian.isIso_of_epi_of_isIso, hom_ext₀_iff, hom_ext₄_iff, naturality'_assoc, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono
arrow 📖	CompOp	1 math math: mkOfObjOfMapSucc_arrow
arrowEquiv 📖	CompOp	2 math math: arrowEquiv_symm_apply, arrowEquiv_apply
hom 📖	CompOp	15 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mk₁_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.mk₁_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, map'_eq_hom₁, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncation₂.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
homMk 📖	CompOp	3 math math: isoMk_inv, isoMk_hom, homMk_app
homMkSucc 📖	CompOp	4 math math: isoMkSucc_hom, homMkSucc_app_zero, isoMkSucc_inv, homMkSucc_app_succ
homMk₀ 📖	CompOp	1 math math: homMk₀_app
homMk₁ 📖	CompOp	13 math math: CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, mapFunctorArrows_app, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, functorArrows_map, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, homMk₁_app
homMk₂ 📖	CompOp	6 math math: homMk₂_app_two, isoMk₂_inv, homMk₂_app_zero, isoMk₂_hom, homMk₂_app_one, homMk₂_app_two'
homMk₃ 📖	CompOp	7 math math: homMk₃_app_three, isoMk₃_hom, homMk₃_app_two, isoMk₃_inv, homMk₃_app_one, HomologicalComplex.HomologySequence.composableArrows₃Functor_map, homMk₃_app_zero
homMk₄ 📖	CompOp	7 math math: homMk₄_app_four, homMk₄_app_three, homMk₄_app_zero, isoMk₄_hom, homMk₄_app_one, isoMk₄_inv, homMk₄_app_two
homMk₅ 📖	CompOp	9 math math: homMk₅_app_five, homMk₅_app_zero, isoMk₅_inv, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, homMk₅_app_two, homMk₅_app_three, isoMk₅_hom, homMk₅_app_one, homMk₅_app_four
isoMk 📖	CompOp	2 math math: isoMk_inv, isoMk_hom
isoMkSucc 📖	CompOp	2 math math: isoMkSucc_hom, isoMkSucc_inv
isoMk₀ 📖	CompOp	2 math math: isoMk₀_inv_app, isoMk₀_hom_app
isoMk₁ 📖	CompOp	2 math math: isoMk₁_hom_app, isoMk₁_inv_app
isoMk₂ 📖	CompOp	2 math math: isoMk₂_inv, isoMk₂_hom
isoMk₃ 📖	CompOp	2 math math: isoMk₃_hom, isoMk₃_inv
isoMk₄ 📖	CompOp	2 math math: isoMk₄_hom, isoMk₄_inv
isoMk₅ 📖	CompOp	2 math math: isoMk₅_inv, isoMk₅_hom
left 📖	CompOp	17 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mk₁_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, Precomp.map_zero_succ_succ, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.left_edge, CategoryTheory.nerve.mk₁_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncation₂.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, precomp_surjective, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
map' 📖	CompOp	51 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, exact_iff_δlast, Exact.cokerIsoKer'_hom_inv_id_assoc, IsComplex.zero'_assoc, CategoryTheory.nerve.δ₂_zero, CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat, Exact.cokerIsoKer'_hom, IsComplex.opcyclesToCycles_fac_assoc, Precomp.map_zero_succ_succ, HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat, exact_iff_δ₀, mkOfObjOfMapSucc_map_succ, IsComplex.mono_cokerToKer', map'_comp, IsComplex.zero_assoc, Exact.opcyclesIsoCycles_hom_fac_assoc, Exact.opcyclesIsoCycles_hom_fac, IsComplex.opcyclesToCycles_fac, Exact.cokerIsoKer'_inv_hom_id, HomotopyCategory.composableArrowsFunctor_obj, map'_inv_eq_inv_map', Exact.isIso_map', mapFunctorArrows_app, Exact.cokerIsoKer'_hom_inv_id, naturality', CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, isComplex₂_iff, Exact.cokerIsoKer'_inv_hom_id_assoc, HomotopyCategory.composableArrowsFunctor_map, Exact.cokerIsoKer_hom_fac_assoc, map'_eq_hom₁, HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat, Exact.cokerIsoKer_hom_fac, IsComplex.epi_cokerToKer', map'_self, Exact.isIso_cokerToKer', Precomp.map_succ_succ, mkOfObjOfMapSucc_exists, functorArrows_map, IsComplex.cokerToKer'_fac_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, naturality'_assoc, Precomp.map_one_succ, functorArrows_obj, IsComplex.cokerToKer'_fac, IsComplex.zero, IsComplex.cokerToKer_fac, CategoryTheory.nerve.δ₂_two, IsComplex.zero', IsComplex.cokerToKer_fac_assoc
mkOfObjOfMapSucc 📖	CompOp	3 math math: mkOfObjOfMapSucc_arrow, mkOfObjOfMapSucc_map_succ, mkOfObjOfMapSucc_obj
mk₀ 📖	CompOp	5 math math: mk₀_surjective, mk₀_obj, CategoryTheory.nerve.σ₀_mk₀_eq, mk₀_map, CategoryTheory.nerveMap_app_mk₀
mk₁ 📖	CompOp	252 math math: CategoryTheory.Triangulated.SpectralObject.Hom.comm, CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₂, CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc, CategoryTheory.nerve.edgeMk_edge, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app, CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles, CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_H, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_π, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc, CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.zero₂_assoc, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₁, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁, CategoryTheory.nerve.δ₂_zero, CategoryTheory.Abelian.SpectralObject.instMonoFromOpcycles, CategoryTheory.Abelian.SpectralObject.sc₂_X₃, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₂, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d, twoδ₁Toδ₀_app_zero, CategoryTheory.Abelian.SpectralObject.δToCycles_πE, CategoryTheory.Abelian.SpectralObject.shortComplex_X₂, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app, CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles, CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.δ_toCycles, CategoryTheory.Abelian.SpectralObject.δ_δ_assoc, CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_i, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv, mk₁_eqToHom_comp, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_H, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le', CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, mk₁_hom, CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv_assoc, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i, CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_inv, mk₁_surjective, CategoryTheory.Abelian.SpectralObject.δ_δ, CategoryTheory.Abelian.SpectralObject.cyclesMap_i, CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i_assoc, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, CategoryTheory.Abelian.SpectralObject.toCycles_descCycles, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀, mkOfObjOfMapSucc_arrow, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le', CategoryTheory.Abelian.SpectralObject.EToCycles_i_assoc, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀', CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_hom, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂, CategoryTheory.Abelian.SpectralObject.πE_ιE, CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom_assoc, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃, CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom, CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.isIso_fromOpcycles, CategoryTheory.Abelian.SpectralObject.zero₃, CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_ι, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_g, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_g, CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, twoδ₂Toδ₁_app_zero, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p, CategoryTheory.Abelian.SpectralObject.p_opcyclesToE, CategoryTheory.Triangulated.SpectralObject.triangle_obj₂, CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_H, CategoryTheory.nerve.mk₁_homEquiv_apply, mk₁_comp_eqToHom, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id, CategoryTheory.nerveMap_app_mk₁, CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.isIso_toCycles, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₂, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g, CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ_assoc, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_X₂, CategoryTheory.Abelian.SpectralObject.sc₂_g, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ_assoc, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles, CategoryTheory.Abelian.SpectralObject.δToCycles_πE_assoc, CategoryTheory.Abelian.SpectralObject.sc₁_X₁, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f, CategoryTheory.Abelian.SpectralObject.zero₂, arrowEquiv_symm_apply, CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE_assoc, mk₁_obj, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₂, CategoryTheory.Abelian.SpectralObject.instEpiToCycles, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₁, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_ι, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁, CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂, CategoryTheory.Triangulated.SpectralObject.triangle_mor₂, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc, CategoryTheory.Abelian.SpectralObject.iCycles_δ, CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁, CategoryTheory.Abelian.SpectralObject.Hom.comm, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_f, CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₂, CategoryTheory.nerve.δ₁_mk₂_eq, CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap_assoc, CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, twoδ₁Toδ₀_app_one, CategoryTheory.Abelian.SpectralObject.sc₂_X₁, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc, mk₁_map, SSet.Truncated.HomotopyCategory.homToNerveMk_app_one, CategoryTheory.Abelian.SpectralObject.zero₁, CategoryTheory.Abelian.SpectralObject.δ_naturality_assoc, CategoryTheory.nerve.σ₀_mk₀_eq, CategoryTheory.Abelian.SpectralObject.δ_naturality, CategoryTheory.Abelian.SpectralObject.d_EIsoH_hom_assoc, CategoryTheory.Abelian.SpectralObject.sc₃_X₁, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc, CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_π, CategoryTheory.Triangulated.SpectralObject.triangle_mor₁, CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_inv_assoc, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_K, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles_assoc, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃, CategoryTheory.Abelian.SpectralObject.sc₂_X₂, CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac, CategoryTheory.nerve.δ₂_mk₂_eq, CategoryTheory.Abelian.SpectralObject.δToCycles_cyclesIso_inv, CategoryTheory.Abelian.SpectralObject.p_descOpcycles, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁, CategoryTheory.Abelian.SpectralObject.πE_ιE_assoc, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_g, instIsIsoOfNatNatTwoδ₁Toδ₀, CategoryTheory.ShortComplex.toComposableArrows_map, CategoryTheory.Abelian.SpectralObject.Hom.comm_assoc, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac, CategoryTheory.Abelian.SpectralObject.sc₁_X₃, CategoryTheory.Abelian.SpectralObject.δ_toCycles_assoc, CategoryTheory.nerve.σ_zero_nerveEquiv_symm, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_inv_hom_id, CategoryTheory.Abelian.SpectralObject.p_descOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.p_fromOpcycles, CategoryTheory.Abelian.SpectralObject.Ψ_fromOpcycles, CategoryTheory.Abelian.SpectralObject.p_opcyclesMap, CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.isZero_H_obj_of_isIso, CategoryTheory.Abelian.SpectralObject.instEpiPOpcycles, CategoryTheory.Triangulated.TStructure.ω₁δ_app, CategoryTheory.Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc, CategoryTheory.Abelian.SpectralObject.ιE_δFromOpcycles, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_H, twoδ₂Toδ₁_app_one, CategoryTheory.Abelian.SpectralObject.δToCycles_iCycles_assoc, SSet.Truncated.HomotopyCategory.homToNerveMk_app_edge, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁, CategoryTheory.ShortComplex.toComposableArrows_obj, CategoryTheory.Abelian.SpectralObject.liftCycles_i, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc, CategoryTheory.Abelian.SpectralObject.EToCycles_i, CategoryTheory.Abelian.SpectralObject.zero₃_assoc, CategoryTheory.Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀', CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le, CategoryTheory.Abelian.SpectralObject.shortComplex_X₁, CategoryTheory.Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀', CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₁, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id, CategoryTheory.Abelian.SpectralObject.sc₃_X₃, CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_Q, CategoryTheory.Abelian.SpectralObject.shortComplex_X₃, CategoryTheory.Abelian.SpectralObject.sc₃_X₂, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₃, CategoryTheory.Triangulated.SpectralObject.triangle_obj₃, CategoryTheory.Abelian.SpectralObject.p_opcyclesToE_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, CategoryTheory.Abelian.SpectralObject.δ_pOpcycles, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv, CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₁, CategoryTheory.Triangulated.SpectralObject.triangle_obj₁, CategoryTheory.Abelian.SpectralObject.toCycles_Ψ, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₂, CategoryTheory.Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc, functorArrows_map, CategoryTheory.Abelian.SpectralObject.liftCycles_i_assoc, CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_f, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id, CategoryTheory.Abelian.SpectralObject.sc₁_X₂, CategoryTheory.Abelian.SpectralObject.sc₂_f, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, CategoryTheory.Abelian.SpectralObject.toCycles_πE_descE, CategoryTheory.Abelian.SpectralObject.EIsoH_hom_naturality, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, instIsIsoOfNatNatTwoδ₂Toδ₁, CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₃, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_f, CategoryTheory.Abelian.SpectralObject.cyclesIsoH_inv, functorArrows_obj, CategoryTheory.Abelian.SpectralObject.cyclesMap_i_assoc, CategoryTheory.Abelian.SpectralObject.liftE_ιE_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.sc₃_f, CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc, CategoryTheory.Abelian.SpectralObject.zero₁_assoc, CategoryTheory.nerve.δ₀_mk₂_eq, CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_X₃, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁, CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc, CategoryTheory.Abelian.SpectralObject.instMonoICycles, CategoryTheory.Abelian.SpectralObject.fromOpcyles_δ, CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.toCycles_descCycles_assoc, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁, CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso, CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le, CategoryTheory.nerve.δ₂_two, CategoryTheory.Abelian.SpectralObject.sc₁_g, CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_X₃, CategoryTheory.Abelian.SpectralObject.toCycles_i, CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃, CategoryTheory.nerve.homEquiv_symm_apply, CategoryTheory.Triangulated.TStructure.spectralObject_δ
mk₂ 📖	CompOp	26 math math: CategoryTheory.Abelian.SpectralObject.exact₁', threeδ₂Toδ₁_app_zero, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app, exact_iff_δlast, threeδ₂Toδ₁_app_one, CategoryTheory.Abelian.SpectralObject.cyclesMap_id, threeδ₁Toδ₀_app_zero, threeδ₃Toδ₂_app_one, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, threeδ₂Toδ₁_app_two, exact_iff_δ₀, CategoryTheory.Abelian.SpectralObject.exact₂', CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app, CategoryTheory.Abelian.SpectralObject.exact₃', CategoryTheory.nerve.δ₁_mk₂_eq, threeδ₁Toδ₀_app_two, CategoryTheory.nerve.δ₂_mk₂_eq, threeδ₃Toδ₂_app_two, CategoryTheory.Abelian.SpectralObject.opcyclesMap_id, threeδ₁Toδ₀_app_one, threeδ₃Toδ₂_app_zero, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.nerve.δ₀_mk₂_eq, mk₂_surjective
mk₃ 📖	CompOp	26 math math: fourδ₁Toδ₀_app_zero, fourδ₄Toδ₃_app_two, CategoryTheory.Abelian.SpectralObject.shortComplexMap_id, fourδ₄Toδ₃_app_one, CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp_assoc, fourδ₂Toδ₁_app_three, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₂, fourδ₂Toδ₁_app_zero, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₃, CategoryTheory.Abelian.SpectralObject.map_comp, fourδ₁Toδ₀_app_two, fourδ₂Toδ₁_app_one, fourδ₃Toδ₂_app_one, mk₃_surjective, CategoryTheory.Abelian.SpectralObject.shortComplexMap_τ₁, fourδ₂Toδ₁_app_two, fourδ₃Toδ₂_app_two, fourδ₃Toδ₂_app_three, fourδ₁Toδ₀_app_one, CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp, fourδ₄Toδ₃_app_zero, fourδ₁Toδ₀_app_three, fourδ₄Toδ₃_app_three, CategoryTheory.Abelian.SpectralObject.map_comp_assoc, fourδ₃Toδ₂_app_zero, CategoryTheory.Abelian.SpectralObject.map_id
mk₄ 📖	CompOp	1 math math: mk₄_surjective
mk₅ 📖	CompOp	1 math math: mk₅_surjective
obj' 📖	CompOp	30 math math: CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono', CategoryTheory.Abelian.mono_of_epi_of_epi_mono', CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono', CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono', Precomp.obj_one, isoMkSucc_hom, CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono, isoMk₅_inv, CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono, CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi, isoMk₄_hom, isoMkSucc_inv, map'_inv_eq_inv_map', isoMk₂_inv, CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono, CategoryTheory.Abelian.isIso_of_isIso_of_mono, naturality', CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, isoMk₃_hom, Precomp.obj_succ, isoMk₅_hom, isoMk₂_hom, isoMk₃_inv, CategoryTheory.Abelian.isIso_of_epi_of_isIso, isoMk₄_inv, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, naturality'_assoc, CategoryTheory.Abelian.mono_of_epi_of_epi_of_mono, CategoryTheory.Abelian.mono_of_mono_of_mono_of_mono
opEquivalence 📖	CompOp	9 math math: opEquivalence_counitIso_inv_app_app, opEquivalence_unitIso_inv_app, opEquivalence_functor_obj_map, opEquivalence_functor_map_app, opEquivalence_inverse_obj, opEquivalence_unitIso_hom_app, opEquivalence_functor_obj_obj, opEquivalence_inverse_map, opEquivalence_counitIso_hom_app_app
precomp 📖	CompOp	4 math math: precomp_obj, precomp_δ₀, precomp_surjective, precomp_map
right 📖	CompOp	15 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, mk₁_hom, CategoryTheory.nerve.homEquiv_apply, CategoryTheory.nerve.right_edge, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.nerve.mk₁_homEquiv_apply, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, arrowEquiv_apply, SSet.OneTruncation₂.nerveHomEquiv_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom
tacticValid 📖	CompOp	—
whiskerLeft 📖	CompOp	3 math math: whiskerLeft_obj, whiskerLeft_map, CategoryTheory.nerve_map
whiskerLeftFunctor 📖	CompOp	3 math math: whiskerLeftFunctor_obj_map, whiskerLeftFunctor_obj_obj, whiskerLeftFunctor_map_app
δlast 📖	CompOp	2 math math: exact_iff_δlast, Exact.δlast
δlastFunctor 📖	CompOp	3 math math: δlastFunctor_obj_obj, δlastFunctor_map_app, δlastFunctor_obj_map
δ₀ 📖	CompOp	7 math math: isoMkSucc_hom, exact_iff_δ₀, isoMkSucc_inv, homMkSucc_app_succ, precomp_δ₀, CategoryTheory.nerve.δ₀_eq, Exact.δ₀
δ₀Functor 📖	CompOp	3 math math: δ₀Functor_obj_map, δ₀Functor_obj_obj, δ₀Functor_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.ComposableArrows CategoryTheory.Arrow EquivLike.toFunLike Equiv.instEquivLike arrowEquiv left right hom	—	—
arrowEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Arrow CategoryTheory.ComposableArrows EquivLike.toFunLike Equiv.instEquivLike Equiv.symm arrowEquiv mk₁ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
ext 📖	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—	CategoryTheory.Functor.ext_of_iso CategoryTheory.Category.assoc CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id
ext_succ 📖	—	obj' δ₀ map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.eqToHom CategoryTheory.Functor.congr_obj CategoryTheory.ComposableArrows	—	—	CategoryTheory.Functor.congr_obj CategoryTheory.Functor.ext_of_iso CategoryTheory.eqToHom_app CategoryTheory.Category.assoc CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.Category.comp_id
ext₀ 📖	—	obj' CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—	ext
ext₁ 📖	—	left right hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	—	CategoryTheory.Functor.ext_of_iso CategoryTheory.Category.assoc CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id Fintype.complete
ext₂ 📖	—	obj' map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—	ext_succ ext₁
ext₂_of_arrow 📖	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map'	—	—	mk₂_surjective
ext₃ 📖	—	obj' map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—	ext_succ ext₂
ext₄ 📖	—	obj' map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—	ext_succ ext₃
ext₅ 📖	—	obj' map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	—	ext_succ ext₄
homMkSucc_app_succ 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' δ₀ CategoryTheory.CategoryStruct.comp map' app'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMkSucc app' δ₀	—	—
homMkSucc_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' δ₀ CategoryTheory.CategoryStruct.comp map' app'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMkSucc	—	—
homMk_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk	—	—
homMk₀_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
homMk₁_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
homMk₂_app_one 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₂	—	—
homMk₂_app_two 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₂	—	—
homMk₂_app_two' 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₂	—	—
homMk₂_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₂	—	—
homMk₃_app_one 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₃	—	—
homMk₃_app_three 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₃	—	—
homMk₃_app_two 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₃	—	—
homMk₃_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₃	—	—
homMk₄_app_four 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₄	—	—
homMk₄_app_one 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₄	—	—
homMk₄_app_three 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₄	—	—
homMk₄_app_two 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₄	—	—
homMk₄_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₄	—	—
homMk₅_app_five 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
homMk₅_app_four 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
homMk₅_app_one 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
homMk₅_app_three 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
homMk₅_app_two 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
homMk₅_app_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map'	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder homMk₅	—	—
hom_ext_succ 📖	—	app' CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder δ₀Functor	—	—	CategoryTheory.NatTrans.ext' CategoryTheory.congr_app
hom_ext₀ 📖	—	app'	—	—	CategoryTheory.NatTrans.ext' Fintype.complete
hom_ext₀_iff 📖	mathematical	—	app'	—	hom_ext₀
hom_ext₁ 📖	—	app'	—	—	CategoryTheory.NatTrans.ext'
hom_ext₁_iff 📖	mathematical	—	app'	—	hom_ext₁
hom_ext₂ 📖	—	app'	—	—	hom_ext_succ hom_ext₁
hom_ext₂_iff 📖	mathematical	—	app'	—	hom_ext₂
hom_ext₃ 📖	—	app'	—	—	hom_ext_succ hom_ext₂
hom_ext₃_iff 📖	mathematical	—	app'	—	hom_ext₃
hom_ext₄ 📖	—	app'	—	—	hom_ext_succ hom_ext₃
hom_ext₄_iff 📖	mathematical	—	app'	—	hom_ext₄
hom_ext₅ 📖	—	app'	—	—	hom_ext_succ hom_ext₄
hom_ext₅_iff 📖	mathematical	—	app'	—	hom_ext₅
isIso_iff₀ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.isIso_iff_isIso_app Fintype.complete
isIso_iff₁ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.isIso_iff_isIso_app Fintype.complete
isIso_iff₂ 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.isIso_iff_isIso_app Fintype.complete
isoMkSucc_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' δ₀ map' app' CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMkSucc homMkSucc obj' δ₀	—	—
isoMkSucc_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' δ₀ map' app' CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMkSucc homMkSucc obj' δ₀	—	—
isoMk_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk homMk CategoryTheory.Functor.obj	—	—
isoMk_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk homMk CategoryTheory.Functor.obj	—	—
isoMk₀_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category isoMk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isoMk₀_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category isoMk₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isoMk₁_hom_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map' CategoryTheory.Iso.hom	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category isoMk₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isoMk₁_inv_app 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map' CategoryTheory.Iso.hom	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category isoMk₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
isoMk₂_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map' CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₂ homMk₂ obj'	—	—
isoMk₂_inv 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' CategoryTheory.CategoryStruct.comp map' CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₂ homMk₂ obj'	—	—
isoMk₃_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₃ homMk₃ obj'	—	—
isoMk₃_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₃ homMk₃ obj'	—	—
isoMk₄_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₄ homMk₄ obj'	—	—
isoMk₄_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₄ homMk₄ obj'	—	—
isoMk₅_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.hom CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₅ homMk₅ obj'	—	—
isoMk₅_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder isoMk₅ homMk₅ obj'	—	—
map'_comp 📖	mathematical	—	map' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	CategoryTheory.Functor.map_comp
map'_eq_hom₁ 📖	mathematical	—	map' hom	—	—
map'_inv_eq_inv_map' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.hom	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' CategoryTheory.Iso.inv	—	CategoryTheory.cancel_epi CategoryTheory.IsSplitEpi.epi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
map'_self 📖	mathematical	—	map' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder	—	CategoryTheory.Functor.map_id
mkOfObjOfMapSucc_arrow 📖	mathematical	—	arrow mkOfObjOfMapSucc mk₁	—	ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp mkOfObjOfMapSucc_map_succ
mkOfObjOfMapSucc_exists 📖	mathematical	—	CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Iso.inv map' CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mkOfObjOfMapSucc_map_succ 📖	mathematical	—	map' mkOfObjOfMapSucc	—	mkOfObjOfMapSucc_exists
mkOfObjOfMapSucc_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mkOfObjOfMapSucc	—	—
mk₀_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mk₀_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₀	—	—
mk₀_surjective 📖	mathematical	—	mk₀	—	le_rfl ext₀
mk₁_comp_eqToHom 📖	mathematical	—	mk₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id
mk₁_eqToHom_comp 📖	mathematical	—	mk₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp
mk₁_hom 📖	mathematical	—	mk₁ left right hom	—	ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk₁_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ Mk₁.map	—	—
mk₁_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder mk₁ Mk₁.obj	—	—
mk₁_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mk₁	—	le_rfl ext₁ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk₂_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mk₂	—	le_rfl ext₂ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk₃_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mk₃	—	le_rfl ext₃ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk₄_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mk₄	—	le_rfl ext₄ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk₅_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mk₅	—	le_rfl ext₅ CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
naturality' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj' map' app'	—	CategoryTheory.NatTrans.naturality
naturality'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder map' obj' app'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality'
opEquivalence_counitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Equivalence.inverse CategoryTheory.Functor.leftOpRightOpEquiv CategoryTheory.Equivalence.op CategoryTheory.Equivalence.congrLeft CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.trans OrderDual OrderDual.instPreorder CategoryTheory.orderDualEquivalence OrderIso.equivalence Fin.revOrderIso CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Equivalence.counitIso opEquivalence CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.monotone OrderIso.symm CategoryTheory.Equivalence.counitInv	—	OrderIso.monotone CategoryTheory.Equivalence.invFunIdAssoc_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opEquivalence_counitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Equivalence.inverse CategoryTheory.Functor.leftOpRightOpEquiv CategoryTheory.Equivalence.op CategoryTheory.Equivalence.congrLeft CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.trans OrderDual OrderDual.instPreorder CategoryTheory.orderDualEquivalence OrderIso.equivalence Fin.revOrderIso CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Equivalence.counitIso opEquivalence CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.monotone OrderIso.symm CategoryTheory.Equivalence.unitInv	—	OrderIso.monotone CategoryTheory.Equivalence.invFunIdAssoc_hom_app CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
opEquivalence_functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ComposableArrows CategoryTheory.Equivalence.functor CategoryTheory.Functor.leftOpRightOpEquiv CategoryTheory.Equivalence.op CategoryTheory.Equivalence.congrLeft CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.trans OrderDual OrderDual.instPreorder CategoryTheory.orderDualEquivalence OrderIso.equivalence Fin.revOrderIso CategoryTheory.Functor.map opEquivalence Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Quiver.Hom.unop	—	—
opEquivalence_functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ComposableArrows CategoryTheory.Equivalence.functor opEquivalence Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop OrderDual OrderDual.instPreorder Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso Fin.revOrderIso OrderIso.monotone Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual CategoryTheory.homOfLE Opposite.op	—	—
opEquivalence_functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.ComposableArrows CategoryTheory.Equivalence.functor opEquivalence Opposite.op Opposite.unop	—	—
opEquivalence_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ComposableArrows Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor CategoryTheory.Equivalence.inverse opEquivalence Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp OrderDual OrderDual.instPreorder Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm Fin.revOrderIso CategoryTheory.Equivalence.functor CategoryTheory.orderDualEquivalence CategoryTheory.Functor.leftOp CategoryTheory.Functor.whiskerLeft CategoryTheory.NatTrans.leftOp	—	—
opEquivalence_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ComposableArrows Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor CategoryTheory.Equivalence.inverse opEquivalence Opposite.op CategoryTheory.Functor.comp OrderDual OrderDual.instPreorder Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm Fin.revOrderIso CategoryTheory.Equivalence.functor CategoryTheory.orderDualEquivalence CategoryTheory.Functor.leftOp	—	—
opEquivalence_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.ComposableArrows CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.op CategoryTheory.Equivalence.congrLeft CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.trans OrderDual OrderDual.instPreorder CategoryTheory.orderDualEquivalence OrderIso.equivalence Fin.revOrderIso CategoryTheory.Functor.leftOpRightOpEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso opEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm OrderIso.monotone Opposite.unop CategoryTheory.Functor.leftOp CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Equivalence.funInvIdAssoc CategoryTheory.Functor.whiskerLeft Quiver.Hom.unop CategoryTheory.Functor.rightOp CategoryTheory.Functor.rightOpLeftOpIso	—	OrderIso.monotone CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
opEquivalence_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.ComposableArrows CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.op CategoryTheory.Equivalence.congrLeft CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.trans OrderDual OrderDual.instPreorder CategoryTheory.orderDualEquivalence OrderIso.equivalence Fin.revOrderIso CategoryTheory.Functor.leftOpRightOpEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso opEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.op Monotone.functor DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm CategoryTheory.Functor.leftOp CategoryTheory.Functor.obj OrderIso.monotone Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.whiskerLeft Quiver.Hom.unop CategoryTheory.Functor.rightOp CategoryTheory.Functor.rightOpLeftOpIso CategoryTheory.Equivalence.funInvIdAssoc	—	OrderIso.monotone CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
precomp_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder precomp Precomp.map	—	—
precomp_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder precomp Precomp.obj	—	—
precomp_surjective 📖	mathematical	—	CategoryTheory.ComposableArrows Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct left precomp	—	ext_succ CategoryTheory.Functor.congr_obj CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
precomp_δ₀ 📖	mathematical	—	δ₀ precomp	—	—
whiskerLeftFunctor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category whiskerLeftFunctor CategoryTheory.Functor.obj	—	—
whiskerLeftFunctor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category whiskerLeftFunctor	—	—
whiskerLeftFunctor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows CategoryTheory.Functor.category whiskerLeftFunctor	—	—
whiskerLeft_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder whiskerLeft CategoryTheory.Functor.obj	—	—
whiskerLeft_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder whiskerLeft	—	—
δlastFunctor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp Fin.castSuccFunctor CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category δlastFunctor	—	—
δlastFunctor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category δlastFunctor	—	—
δlastFunctor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows CategoryTheory.Functor.category δlastFunctor	—	—
δ₀Functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.comp Fin.succFunctor CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category δ₀Functor	—	—
δ₀Functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category δ₀Functor CategoryTheory.homOfLE	—	—
δ₀Functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows CategoryTheory.Functor.category δ₀Functor	—	—

CategoryTheory.ComposableArrows.Mk₁

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: CategoryTheory.ComposableArrows.mk₁_map, map_comp, map_id
obj 📖	CompOp	3 math math: CategoryTheory.ComposableArrows.mk₁_obj, map_comp, map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	—	map LE.le.trans PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj	—	LE.le.trans map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	—

CategoryTheory.ComposableArrows.Precomp

Definitions

Name	Category	Theorems
map 📖	CompOp	11 math math: map_zero_one', map_zero_one, map_zero_succ_succ, CategoryTheory.ShortComplex.toComposableArrows_map, map_comp, map_succ_succ, map_one_succ, map_zero_zero, map_id, CategoryTheory.ComposableArrows.precomp_map, map_one_one
obj 📖	CompOp	9 math math: CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app, obj_one, CategoryTheory.ComposableArrows.precomp_obj, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app, obj_succ, obj_zero, CategoryTheory.ShortComplex.toComposableArrows_obj, map_comp, map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_comp 📖	mathematical	—	map LE.le.trans PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj	—	LE.le.trans CategoryTheory.Category.id_comp zero_add Fin.instNeZeroHAddNatOfNat_mathlib CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.homOfLE_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	CategoryTheory.Functor.map_id
map_one_one 📖	mathematical	—	map CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
map_one_succ 📖	mathematical	—	map CategoryTheory.ComposableArrows.map'	—	—
map_succ_succ 📖	mathematical	—	map CategoryTheory.ComposableArrows.map'	—	—
map_zero_one 📖	mathematical	—	map	—	—
map_zero_one' 📖	mathematical	—	map	—	—
map_zero_succ_succ 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows.left CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.map'	—	—
map_zero_zero 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
obj_one 📖	mathematical	—	obj CategoryTheory.ComposableArrows.obj'	—	—
obj_succ 📖	mathematical	—	obj CategoryTheory.ComposableArrows.obj'	—	—
obj_zero 📖	mathematical	—	obj	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapComposableArrows 📖	CompOp	10 math math: mapComposableArrowsObjMk₂Iso_inv_app, mapComposableArrowsObjMk₁Iso_inv_app, CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions, mapComposableArrowsObjMk₂Iso_hom_app, mapComposableArrowsObjMk₁Iso_hom_app, mapComposableArrows_obj_map, mapComposableArrows_obj_obj, CategoryTheory.nerveMap_app, CategoryTheory.Localization.essSurj_mapComposableArrows, mapComposableArrows_map_app
mapComposableArrowsObjMk₁Iso 📖	CompOp	2 math math: mapComposableArrowsObjMk₁Iso_inv_app, mapComposableArrowsObjMk₁Iso_hom_app
mapComposableArrowsObjMk₂Iso 📖	CompOp	2 math math: mapComposableArrowsObjMk₂Iso_inv_app, mapComposableArrowsObjMk₂Iso_hom_app
mapComposableArrowsOpIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapComposableArrowsObjMk₁Iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj CategoryTheory.ComposableArrows category mapComposableArrows CategoryTheory.ComposableArrows.mk₁ map CategoryTheory.Iso.hom mapComposableArrowsObjMk₁Iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapComposableArrowsObjMk₁Iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₁ obj map CategoryTheory.ComposableArrows category mapComposableArrows CategoryTheory.Iso.inv mapComposableArrowsObjMk₁Iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapComposableArrowsObjMk₂Iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj CategoryTheory.ComposableArrows category mapComposableArrows CategoryTheory.ComposableArrows.mk₂ map CategoryTheory.Iso.hom mapComposableArrowsObjMk₂Iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows.Precomp.obj CategoryTheory.ComposableArrows.mk₁ CategoryTheory.CategoryStruct.id	—	—
mapComposableArrowsObjMk₂Iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ obj map CategoryTheory.ComposableArrows category mapComposableArrows CategoryTheory.Iso.inv mapComposableArrowsObjMk₂Iso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ComposableArrows.Precomp.obj CategoryTheory.ComposableArrows.mk₁ CategoryTheory.CategoryStruct.id	—	—
mapComposableArrows_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder comp map CategoryTheory.ComposableArrows category mapComposableArrows obj	—	—
mapComposableArrows_obj_map 📖	mathematical	—	map Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder obj CategoryTheory.ComposableArrows category mapComposableArrows	—	—
mapComposableArrows_obj_obj 📖	mathematical	—	obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows category mapComposableArrows	—	—

Fin

Definitions

Name	Category	Theorems
castSuccFunctor 📖	CompOp	3 math math: CategoryTheory.ComposableArrows.δlastFunctor_map_app, castSuccFunctor_obj, castSuccFunctor_map
succFunctor 📖	CompOp	3 math math: CategoryTheory.ComposableArrows.δ₀Functor_map_app, succFunctor_obj, succFunctor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
castSuccFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder instPartialOrder castSuccFunctor	—	—
castSuccFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder castSuccFunctor	—	—
succFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory PartialOrder.toPreorder instPartialOrder succFunctor CategoryTheory.homOfLE	—	—
succFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder instPartialOrder succFunctor	—	—

---

← Back to Index