ComposableArrows 📖 | CompOp | 332 mathmath: Triangulated.SpectralObject.Hom.comm, HomotopyCategory.spectralObjectMappingCone_δ'_app, Abelian.SpectralObject.δ_eq_zero_of_isIso₂, Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc, nerve.edgeMk_edge, Abelian.SpectralObject.exact₁', ComposableArrows.opEquivalence_counitIso_inv_app_app, Functor.mapComposableArrowsObjMk₂Iso_inv_app, ComposableArrows.isoMk₁_hom_app, ComposableArrows.sc'MapIso_inv, Abelian.SpectralObject.δToCycles_iCycles, Abelian.SpectralObject.leftHomologyDataShortComplex_H, Abelian.SpectralObject.homologyDataIdId_left_π, Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc, Abelian.SpectralObject.liftOpcycles_fromOpcycles_assoc, ComposableArrows.isIso_iff₂, Abelian.SpectralObject.zero₂_assoc, Abelian.SpectralObject.cokernelSequenceCycles_X₁, Abelian.SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁, Triangulated.SpectralObject.ω₂_obj_distinguished, Abelian.SpectralObject.instMonoFromOpcycles, Abelian.SpectralObject.sc₂_X₃, Abelian.SpectralObject.cokernelSequenceOpcycles_X₂, Abelian.SpectralObject.toCycles_πE_d, nerve.functorOfNerveMap_map, Abelian.SpectralObject.δToCycles_πE, Abelian.SpectralObject.shortComplex_X₂, Functor.mapComposableArrowsObjMk₁Iso_inv_app, Abelian.SpectralObject.d_ιE_fromOpcycles, Abelian.SpectralObject.toCycles_πE_d_assoc, nerve.homEquiv_edgeMk_map_nerveMap, Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀, Abelian.SpectralObject.δ_toCycles, Abelian.SpectralObject.δ_δ_assoc, Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles, Abelian.SpectralObject.homologyDataIdId_left_i, Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv, Abelian.SpectralObject.homologyDataIdId_left_H, Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le', Triangulated.SpectralObject.ω₂_obj_mor₃, Triangulated.TStructure.triangleω₁δ_map_hom₁, Abelian.SpectralObject.δToCycles_cyclesIso_inv_assoc, Abelian.SpectralObject.cyclesMap_id, Abelian.SpectralObject.cyclesIso_hom_i, Abelian.SpectralObject.pOpcycles_δFromOpcycles, Triangulated.TStructure.ω₁δ_naturality_assoc, Abelian.SpectralObject.homologyDataIdId_iso_inv, nerve.homEquiv_apply, Abelian.SpectralObject.δ_δ, Abelian.SpectralObject.cyclesMap_i, Abelian.SpectralObject.cyclesIso_hom_i_assoc, Triangulated.TStructure.triangleω₁δ_map_hom₂, Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le, nerve.edgeMk_id, nerve.right_edge, Triangulated.TStructure.spectralObject_ω₁, Abelian.SpectralObject.toCycles_descCycles, Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀, Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le', Abelian.SpectralObject.comp_hom, nerve.homEquiv_edgeMk, Abelian.SpectralObject.EToCycles_i_assoc, Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions, Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀', Triangulated.TStructure.ω₁_map, Abelian.SpectralObject.toCycles_cyclesMap, Abelian.SpectralObject.homologyDataIdId_iso_hom, Abelian.SpectralObject.IsFirstQuadrant.isZero₂, Abelian.SpectralObject.comp_hom_assoc, Abelian.SpectralObject.πE_ιE, Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc, ComposableArrows.opEquivalence_unitIso_inv_app, nerve.nonempty_compStruct_iff, ComposableArrows.isoMkSucc_hom, Abelian.SpectralObject.p_opcyclesIso_inv, Abelian.SpectralObject.πE_EIsoH_hom_assoc, Abelian.SpectralObject.kernelSequenceOpcyclesE_X₃, Abelian.SpectralObject.d_EIsoH_hom, ComposableArrows.isoMk₅_inv, Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀, Abelian.SpectralObject.isIso_fromOpcycles, Abelian.SpectralObject.zero₃, Abelian.SpectralObject.rightHomologyDataShortComplex_ι, Abelian.SpectralObject.cokernelSequenceE_g, Abelian.SpectralObject.kernelSequenceE_g, Abelian.SpectralObject.toCycles_cyclesMap_assoc, Abelian.SpectralObject.exact₂', Triangulated.SpectralObject.ω₂_map_hom₁, Abelian.SpectralObject.homologyDataIdId_right_p, ComposableArrows.whiskerLeftFunctor_obj_map, nerve.homEquiv_comp, Abelian.SpectralObject.p_opcyclesToE, Triangulated.SpectralObject.triangle_obj₂, Abelian.SpectralObject.rightHomologyDataShortComplex_H, nerve.left_edge, nerve.mk₁_homEquiv_apply, Abelian.SpectralObject.cyclesIsoH_inv_hom_id, Abelian.SpectralObject.ιE_δFromOpcycles_assoc, Abelian.SpectralObject.isIso_toCycles, ComposableArrows.isoMk₄_hom, Triangulated.TStructure.triangleω₁δ_map_hom₃, Abelian.SpectralObject.shortComplexMap_id, Abelian.SpectralObject.liftE_ιE_fromOpcycles, ShortComplex.SnakeInput.composableArrowsFunctor_map, ComposableArrows.opEquivalence_functor_obj_map, Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le, Abelian.SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃, Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, ComposableArrows.δ₀Functor_obj_map, Abelian.SpectralObject.kernelSequenceOpcycles_X₂, Abelian.SpectralObject.kernelSequenceCyclesE_g, ComposableArrows.isoMkSucc_inv, Abelian.SpectralObject.fromOpcyles_δ_assoc, Abelian.SpectralObject.cokernelSequenceCycles_X₂, Abelian.SpectralObject.sc₂_g, Abelian.SpectralObject.cyclesIsoH_inv_hom_id_assoc, Abelian.SpectralObject.toCycles_Ψ_assoc, Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles, Abelian.SpectralObject.δToCycles_πE_assoc, Abelian.SpectralObject.sc₁_X₁, ComposableArrows.whiskerLeftFunctor_obj_obj, ComposableArrows.opEquivalence_functor_map_app, Functor.mapComposableArrowsObjMk₂Iso_hom_app, ComposableArrows.sc'MapIso_hom, Abelian.SpectralObject.cokernelSequenceCycles_f, ComposableArrows.opEquivalence_inverse_obj, Abelian.SpectralObject.zero₂, HomotopyCategory.composableArrowsFunctor_obj, ComposableArrows.arrowEquiv_symm_apply, Triangulated.TStructure.spectralObjectFunctor_map_hom, ComposableArrows.scMapIso_inv, Abelian.SpectralObject.toCycles_πE_descE_assoc, Abelian.SpectralObject.opcyclesIsoH_hom, Abelian.SpectralObject.cyclesIsoH_hom_EIsoH_inv_assoc, Abelian.SpectralObject.opcyclesMap_fromOpcycles, Abelian.SpectralObject.shortComplexMap_comp_assoc, Abelian.SpectralObject.cokernelSequenceE_X₂, Abelian.SpectralObject.instEpiToCycles, ComposableArrows.opEquivalence_unitIso_hom_app, ComposableArrows.mapFunctorArrows_app, ShortComplex.mapToComposableArrows_comp, Functor.mapComposableArrowsObjMk₁Iso_hom_app, Abelian.SpectralObject.cokernelSequenceCyclesE_X₁, Functor.mapComposableArrows_obj_map, Abelian.SpectralObject.Ψ_fromOpcycles_assoc, Abelian.SpectralObject.homologyDataIdId_right_ι, Abelian.SpectralObject.exact₃', Abelian.SpectralObject.p_fromOpcycles_assoc, Abelian.SpectralObject.πE_EIsoH_hom, ComposableArrows.isoMk₂_inv, Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, Abelian.SpectralObject.IsFirstQuadrant.isZero₁, Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁, Triangulated.TStructure.ω₁_obj, Abelian.SpectralObject.liftOpcycles_fromOpcycles, Abelian.SpectralObject.IsThirdQuadrant.isZero₂, Triangulated.SpectralObject.triangle_mor₂, Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc, nerve.homEquiv_id, Abelian.SpectralObject.iCycles_δ, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁, Abelian.SpectralObject.Hom.comm, Abelian.SpectralObject.kernelSequenceE_f, ComposableArrows.isoMk_inv, Abelian.SpectralObject.kernelSequenceCycles_X₂, Triangulated.SpectralObject.Hom.comm_assoc, Abelian.SpectralObject.p_opcyclesMap_assoc, Abelian.SpectralObject.d_ιE_fromOpcycles_assoc, Triangulated.SpectralObject.ω₂_obj_mor₂, Triangulated.SpectralObject.id_hom, Abelian.SpectralObject.sc₂_X₁, Abelian.SpectralObject.opcyclesIsoH_inv_hom_id_assoc, Abelian.SpectralObject.zero₁, Abelian.SpectralObject.δ_naturality_assoc, ComposableArrows.δlastFunctor_obj_obj, Abelian.SpectralObject.δ_naturality, Abelian.SpectralObject.d_EIsoH_hom_assoc, Abelian.SpectralObject.sc₃_X₁, ComposableArrows.scMapIso_hom, ComposableArrows.opEquivalence_functor_obj_obj, Abelian.SpectralObject.leftHomologyDataShortComplex_π, Triangulated.SpectralObject.distinguished', Triangulated.SpectralObject.triangle_mor₁, ComposableArrows.isoMk₃_hom, Abelian.SpectralObject.p_opcyclesIso_inv_assoc, ComposableArrows.whiskerLeftFunctor_map_app, Abelian.SpectralObject.shortComplexMap_τ₂, ComposableArrows.δlastFunctor_map_app, Abelian.SpectralObject.homologyDataIdId_left_K, Abelian.SpectralObject.δ_pOpcycles_assoc, Abelian.SpectralObject.id_hom, HomotopyCategory.composableArrowsFunctor_map, Triangulated.SpectralObject.mapTriangulatedFunctor_δ, Abelian.SpectralObject.shortComplexMap_τ₃, Abelian.SpectralObject.map_comp, Abelian.SpectralObject.sc₂_X₂, Abelian.SpectralObject.cokernelIsoCycles_hom_fac, Abelian.SpectralObject.δToCycles_cyclesIso_inv, Abelian.SpectralObject.p_descOpcycles, Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁, Abelian.SpectralObject.πE_ιE_assoc, Abelian.SpectralObject.kernelSequenceOpcycles_g, ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀, nerve_obj, Abelian.SpectralObject.Hom.comm_assoc, Abelian.SpectralObject.opcyclesIsoKernel_hom_fac, ComposableArrows.isoMk₅_hom, Abelian.SpectralObject.sc₁_X₃, Abelian.SpectralObject.δ_toCycles_assoc, nerve.σ_zero_nerveEquiv_symm, ComposableArrows.isoMk₀_inv_app, Triangulated.SpectralObject.comp_hom, Abelian.SpectralObject.opcyclesIsoH_inv_hom_id, ComposableArrows.isoMk_hom, Abelian.SpectralObject.p_descOpcycles_assoc, ComposableArrows.isIso_iff₀, Abelian.SpectralObject.p_fromOpcycles, Abelian.SpectralObject.Ψ_fromOpcycles, Abelian.SpectralObject.p_opcyclesMap, Triangulated.SpectralObject.mapTriangulatedFunctor_δ', Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc, Abelian.SpectralObject.isZero_H_obj_of_isIso, ShortComplex.SnakeInput.composableArrowsFunctor_obj, Abelian.SpectralObject.instEpiPOpcycles, Triangulated.TStructure.ω₁δ_app, ComposableArrows.isoMk₂_hom, Abelian.SpectralObject.opcyclesIsoKernel_hom_fac_assoc, Abelian.SpectralObject.ιE_δFromOpcycles, ComposableArrows.isoMk₃_inv, Abelian.SpectralObject.homologyDataIdId_right_H, Abelian.SpectralObject.δToCycles_iCycles_assoc, HomotopyCategory.spectralObjectMappingCone_ω₁, ComposableArrows.opEquivalence_inverse_map, Abelian.SpectralObject.shortComplexMap_τ₁, Functor.mapComposableArrows_obj_obj, ComposableArrows.arrowEquiv_apply, Abelian.SpectralObject.opcyclesMap_id, Abelian.SpectralObject.liftCycles_i, Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc, Abelian.SpectralObject.EToCycles_i, Abelian.SpectralObject.zero₃_assoc, Abelian.SpectralObject.mono_H_map_twoδ₁Toδ₀', ComposableArrows.δ₀Functor_obj_obj, Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le, Abelian.SpectralObject.shortComplex_X₁, Abelian.SpectralObject.isIso_H_map_twoδ₁Toδ₀', Abelian.SpectralObject.cokernelSequenceOpcycles_X₁, Abelian.SpectralObject.opcyclesIsoH_hom_inv_id, Abelian.SpectralObject.sc₃_X₃, Abelian.SpectralObject.homologyDataIdId_right_Q, ComposableArrows.isoMk₁_inv_app, Abelian.SpectralObject.shortComplex_X₃, Abelian.SpectralObject.sc₃_X₂, Triangulated.SpectralObject.ω₂_map_hom₂, Abelian.SpectralObject.kernelSequenceCycles_X₃, SSet.OneTruncation₂.nerveHomEquiv_apply, Triangulated.SpectralObject.triangle_obj₃, ComposableArrows.isoMk₄_inv, Triangulated.SpectralObject.comp_hom_assoc, HomologicalComplex.HomologySequence.composableArrows₃Functor_map, Abelian.SpectralObject.p_opcyclesToE_assoc, Triangulated.SpectralObject.ω₂_obj_obj₂, Abelian.SpectralObject.δ_pOpcycles, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv, Abelian.SpectralObject.δ_eq_zero_of_isIso₁, Abelian.SpectralObject.cokernelSequenceE_X₁, Triangulated.SpectralObject.triangle_obj₁, Abelian.SpectralObject.toCycles_Ψ, Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃, Abelian.SpectralObject.kernelSequenceE_X₂, ComposableArrows.δ₀Functor_map_app, Abelian.SpectralObject.opcyclesIsoH_hom_inv_id_assoc, HomologicalComplex.HomologySequence.composableArrows₃Functor_obj, ComposableArrows.mkOfObjOfMapSucc_exists, ComposableArrows.isoMk₀_hom_app, ComposableArrows.functorArrows_map, Abelian.SpectralObject.liftCycles_i_assoc, nerveMap_app, Abelian.SpectralObject.cokernelSequenceE_f, Triangulated.SpectralObject.ω₂_obj_mor₁, Abelian.SpectralObject.cyclesIsoH_hom_inv_id, Abelian.SpectralObject.sc₁_X₂, ComposableArrows.precomp_surjective, nerve.functorOfNerveMap_obj, Abelian.SpectralObject.shortComplexMap_comp, Abelian.SpectralObject.sc₂_f, Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, Abelian.SpectralObject.toCycles_πE_descE, Abelian.SpectralObject.EIsoH_hom_naturality, Triangulated.SpectralObject.ω₂_map_hom₃, ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁, Abelian.SpectralObject.kernelSequenceE_X₃, Triangulated.TStructure.ω₁δ_naturality, Abelian.SpectralObject.cokernelSequenceOpcyclesE_f, ComposableArrows.opEquivalence_counitIso_hom_app_app, Abelian.SpectralObject.cyclesIsoH_inv, ComposableArrows.functorArrows_obj, Abelian.SpectralObject.cyclesMap_i_assoc, Abelian.SpectralObject.liftE_ιE_fromOpcycles_assoc, Abelian.SpectralObject.sc₃_f, Abelian.SpectralObject.iCycles_δ_assoc, Abelian.SpectralObject.zero₁_assoc, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, ShortComplex.mapToComposableArrows_id, Abelian.SpectralObject.kernelSequenceCyclesE_X₃, Triangulated.SpectralObject.ω₂_obj_obj₁, Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc, Abelian.SpectralObject.pOpcycles_δFromOpcycles_assoc, Abelian.SpectralObject.instMonoICycles, Abelian.SpectralObject.fromOpcyles_δ, Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀, Abelian.SpectralObject.toCycles_descCycles_assoc, Abelian.SpectralObject.IsThirdQuadrant.isZero₁, Abelian.SpectralObject.map_comp_assoc, Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso, Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le, Localization.essSurj_mapComposableArrows, ComposableArrows.isIso_iff₁, Abelian.SpectralObject.sc₁_g, Abelian.SpectralObject.kernelSequenceOpcycles_X₃, nerve.edgeMk_surjective, Abelian.SpectralObject.toCycles_i, Abelian.SpectralObject.toCycles_i_assoc, Triangulated.SpectralObject.ω₂_obj_obj₃, Abelian.SpectralObject.map_id, ComposableArrows.δlastFunctor_obj_map, nerve.homEquiv_symm_apply, Triangulated.TStructure.spectralObject_δ, Functor.mapComposableArrows_map_app
|