Basic

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

Statistics

Metric	Count
Definitions hasShift, add, zero, HasShift, shift, shiftMonoidal, ShiftMkCore, F, add, zero, hasShiftMk, instMonoidalDiscreteFunctorFunctorF, instMonoidalDiscreteFunctorShiftMonoidalFunctor, shiftAdd, shiftComm, shiftEquiv, shiftEquiv', shiftFunctor, shiftFunctorAdd, shiftFunctorAdd', shiftFunctorComm, shiftFunctorCompIsoId, shiftFunctorZero, shiftFunctorZero', shiftMonoidalFunctor, shiftNegShift, shiftShiftNeg, shiftZero, «term_⟦_⟧'», «term_⟦_⟧»	30
Theorems map_add_hom_app, map_add_inv_app, map_zero_hom_app, map_zero_inv_app, add_zero_hom_app, add_zero_inv_app, assoc_hom_app, assoc_hom_app_assoc, assoc_inv_app, assoc_inv_app_assoc, shiftFunctorAdd_eq, shiftFunctorZero_eq, shiftFunctor_eq, zero_add_hom_app, zero_add_inv_app, instIsEquivalenceShiftFunctor, shiftComm', shiftComm_hom_comp, shiftComm_hom_comp_assoc, shiftComm_symm, shiftEquiv'_counitIso, shiftEquiv'_functor, shiftEquiv'_inverse, shiftEquiv'_unitIso, shiftFunctorAdd'_add_zero, shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd'_assoc, shiftFunctorAdd'_assoc_hom_app, shiftFunctorAdd'_assoc_hom_app_assoc, shiftFunctorAdd'_assoc_inv_app, shiftFunctorAdd'_assoc_inv_app_assoc, shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_zero_add, shiftFunctorAdd'_zero_add_hom_app, shiftFunctorAdd'_zero_add_inv_app, shiftFunctorAdd_add_zero_hom_app, shiftFunctorAdd_add_zero_inv_app, shiftFunctorAdd_assoc, shiftFunctorAdd_assoc_hom_app, shiftFunctorAdd_assoc_hom_app_assoc, shiftFunctorAdd_assoc_inv_app, shiftFunctorAdd_assoc_inv_app_assoc, shiftFunctorAdd_zero_add_hom_app, shiftFunctorAdd_zero_add_inv_app, shiftFunctorComm_eq, shiftFunctorComm_eq_refl, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc, shiftFunctorComm_hom_app_of_add_eq_zero, shiftFunctorComm_hom_app_of_add_eq_zero_assoc, shiftFunctorComm_inv_app_of_add_eq_zero, shiftFunctorComm_inv_app_of_add_eq_zero_assoc, shiftFunctorComm_symm, shiftFunctorComm_zero_hom_app, shiftFunctorCompIsoId_add'_hom_app, shiftFunctorCompIsoId_add'_inv_app, shiftFunctorCompIsoId_naturality_1, shiftFunctorCompIsoId_naturality_1_assoc, shiftFunctorCompIsoId_zero_zero_hom_app, shiftFunctorCompIsoId_zero_zero_inv_app, shiftFunctorZero_hom_app_shift, shiftFunctorZero_inv_app_shift, shiftZero', shift_equiv_triangle, shift_neg_shift', shift_shift', shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app, shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app, shift_shiftFunctorCompIsoId_hom_app, shift_shiftFunctorCompIsoId_inv_app, shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app, shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app, shift_shift_neg', shift_zero_eq_zero	75
Total	105

CategoryTheory

Definitions

Name	Category	Theorems
HasShift 📖	CompData	—
ShiftMkCore 📖	CompData	—
hasShiftMk 📖	CompOp	3 math math: ShiftMkCore.shiftFunctorZero_eq, ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq
instMonoidalDiscreteFunctorFunctorF 📖	CompOp	—
instMonoidalDiscreteFunctorShiftMonoidalFunctor 📖	CompOp	—
shiftAdd 📖	CompOp	1 math math: shift_shift'
shiftComm 📖	CompOp	9 math math: DifferentialObject.shiftFunctor_obj_d, Functor.commShift₂_comm, shiftComm_hom_comp_assoc, Functor.CommShift₂.comm, shiftComm', DifferentialObject.shiftFunctor_map_f, shiftComm_hom_comp, shiftComm_symm, Functor.commShift₂_comm_assoc
shiftEquiv 📖	CompOp	—
shiftEquiv' 📖	CompOp	4 math math: shiftEquiv'_functor, shiftEquiv'_inverse, shiftEquiv'_unitIso, shiftEquiv'_counitIso
shiftFunctor 📖	CompOp	772 math math: shiftFunctorZero_inv_app_obj_of_induced, Triangulated.SpectralObject.Hom.comm, HomotopyCategory.spectralObjectMappingCone_δ'_app, Triangulated.TStructure.eTriangleLTGE_map_app_hom₃, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, SingleFunctors.shiftIso_add, Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ', Functor.CommShift.isoAdd_hom_app, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, ObjectProperty.prop_shift_iff_of_isStableUnderShift, shiftFunctorAdd'_assoc_inv_app, Triangulated.Octahedron.mem, Triangulated.TStructure.truncGEδLT_comp_truncLTι, SingleFunctors.Hom.comm, Pretriangulated.shiftFunctorCompIsoId_op_hom_app, Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, shift_shiftFunctorCompIsoId_hom_app, Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc, DifferentialObject.shiftFunctor_obj_d, Abelian.Ext.homLinearEquiv_apply, Functor.shiftIso_add_inv_app, Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, shiftFunctorComm_zero_hom_app, ShiftedHom.neg_comp, Functor.CommShift.isoAdd_inv_app, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, Triangulated.TStructure.eTriangleLTGE_map_app_hom₂, HasShift.Induced.add_inv_app_obj, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁, MorphismProperty.IsCompatibleWithShift.shiftFunctor_comp_inverts, Pretriangulated.Triangle.invRotate_mor₃, CochainComplex.isStrictlyGE_shift, Adjunction.LeftAdjointCommShift.iso_hom_app_assoc, Pretriangulated.Triangle.invRotate_obj₁, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, shift_shift', Functor.shiftIso_add', NatTrans.CommShiftCore.shift_app_comm, Functor.map_shiftFunctorComm_hom_app, CochainComplex.HomComplex.Cochain.leftShift_smul, Pretriangulated.Triangle.shiftFunctor_map_hom₁, Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app, ShiftedHom.mk₀_zero, Triangulated.Octahedron'.triangle_mor₃, Pretriangulated.opShiftFunctorEquivalence_inverse, shiftFunctorAdd'_zero_add, shiftFunctorComm_eq_refl, shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app, Functor.shiftIso_hom_app_comp, Pretriangulated.shiftFunctorZero_op_inv_app, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, Triangulated.TStructure.triangleLEGE_map_hom₃, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, Adjunction.LeftAdjointCommShift.iso_inv_app_assoc, Functor.mapTriangle_obj, Triangulated.Octahedron'.mem, SingleFunctors.shiftIso_add', Functor.commShiftOp_iso_eq, DifferentialObject.d_squared_apply, ShiftedHom.opEquiv_symm_add, Pretriangulated.shiftFunctorCompIsoId_op_inv_app, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, GradedObject.shiftFunctor_map_apply, Pretriangulated.Triangle.shift_distinguished, Functor.shiftIso_zero_inv_app, Functor.commShift₂_comm, Pretriangulated.Triangle.shiftFunctor_obj, Abelian.Ext.smul_hom, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, Pretriangulated.invRotCompRot_inv_app_hom₃, shiftEquiv'_functor, ObjectProperty.prop_shift_iff, Functor.CommShift.isoZero_hom_app, LocalizerMorphism.commShift_iso_hom_app, CochainComplex.HomComplex.Cochain.rightUnshift_neg, DifferentialObject.shiftFunctor_obj_obj, Functor.commShiftIso_comp_hom_app, Functor.commShiftIso_map₂CochainComplex_flip_hom_app, Functor.mapTriangleCommShiftIso_inv_app_hom₁, ShiftedHom.comp_add, CochainComplex.mappingConeCompTriangle_mor₃, CochainComplex.HomComplex.Cochain.shift_add, Triangulated.SpectralObject.ω₂_obj_mor₃, Triangulated.TStructure.triangleω₁δ_map_hom₁, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, Pretriangulated.shiftFunctorAdd'_op_hom_app, shiftFunctorCompIsoId_naturality_1, Localization.instHasSmallLocalizedHomObjShiftFunctor_1, Pretriangulated.Opposite.OpOpCommShift.iso_inv_app, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, CochainComplex.HomComplex.Cochain.shift_neg, DifferentialObject.shiftZero_hom_app_f, Functor.shiftMap_comp', Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_epi, HasShift.Induced.zero_inv_app_obj, shift_shift_neg', NatTrans.CommShift.shift_comm, LocalizerMorphism.commShift_iso_inv_app, HasShift.Induced.add_hom_app_obj, Triangulated.TStructure.ω₁δ_naturality_assoc, pullbackShiftFunctorZero_inv_app, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, Pretriangulated.Triangle.functorMk_map_hom₃, HomologicalComplex.dgoToHomologicalComplex_obj_d, Pretriangulated.commShiftIso_opOp_inv_app, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, oppositeShiftFunctorAdd_inv_app, Functor.shiftIso_zero_hom_app, Functor.isoShift_inv_naturality_assoc, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, Triangulated.TStructure.triangleω₁δ_map_hom₂, Pretriangulated.Triangle.functorMk_map_hom₁, CochainComplex.XIsoOfEq_shift, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app_assoc, CochainComplex.HomComplex.Cochain.rightUnshift_comp, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CochainComplex.mappingCone.inr_triangleδ, Pretriangulated.TriangleMorphism.comm₃, Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app_assoc, Triangulated.TStructure.isGE_shift_iff, ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, Functor.shift_map_op_assoc, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality, Triangulated.TStructure.triangleLEGT_map_hom₁, Triangulated.TStructure.truncGEδLT_comp_truncLTι_app, Triangulated.Octahedron'.comm₂, Pretriangulated.commShiftIso_opOp_hom_app_assoc, Triangulated.TStructure.isIso_truncLT_map_iff, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality, Pretriangulated.shiftFunctorAdd'_op_inv_app, shiftEquiv'_inverse, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, HomotopyCategory.instAdditiveIntUpShiftFunctor, NatTrans.shift_comm_assoc, CochainComplex.HomComplex.Cochain.shift_zero, shiftFunctorCompIsoId_add'_inv_app, shiftFunctorAdd_zero_add_hom_app, ShiftedHom.zero_comp, CochainComplex.shiftFunctorZero_inv_app_f, shiftFunctorAdd'_assoc, SingleFunctors.Hom.comm_assoc, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, ObjectProperty.instAdditiveFullSubcategoryShiftFunctor, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CochainComplex.HomComplex.Cochain.leftShift_comp, Triangulated.Localization.instAdditiveLocalization'ShiftFunctorInt, Triangulated.TStructure.triangleLTLTGELT_map_hom₁, Functor.isoShift_inv_naturality, Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, Adjunction.unit_app_shift_commShiftIso_inv_app, Functor.CommShift.ofIso_commShiftIso_hom_app, Quotient.LiftCommShift.iso_hom_app, CochainComplex.isKInjective_shift_iff, Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, Shift.linear_of_localization, ShiftedHom.comp_mk₀, Triangulated.Octahedron.comm₄_assoc, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, shiftComm_hom_comp_assoc, Triangulated.TStructure.isLE_shift_iff, TwistShiftData.shiftFunctorZero_hom_app, CochainComplex.HomComplex.Cochain.leftShift_rightShift, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, Functor.isoShift_hom_naturality, Functor.CommShift.isoZero'_inv_app, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, Functor.commShiftOfLocalization_iso_inv_app, Triangulated.SpectralObject.ω₂_map_hom₁, Functor.commShiftOfLocalization.iso_inv_app, Pretriangulated.Triangle.rotate_mor₃, Functor.CommShift.comp_commShiftIso_inv_app, Abelian.Ext.singleFunctor_map_comp_hom, Triangulated.Localization.complete_distinguished_triangle_morphism, Triangulated.TStructure.exists_triangle, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, DifferentialObject.d_squared, ShiftedHom.mk₀_comp, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc, ProjectiveResolution.extMk_hom, Functor.shiftIso_add_hom_app, Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃, shiftFunctorAdd_inv_app_obj_of_induced, Triangulated.Octahedron.triangle_mor₃, TwistShiftData.shift_z_app, Abelian.Ext.mapExactFunctor_hom, CochainComplex.HomComplex.Cochain.shift_smul, Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃, Triangulated.Octahedron.map_m₃, Triangulated.TStructure.triangleω₁δ_map_hom₃, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, Functor.shiftMap_comp, Functor.shiftIso_add'_hom_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, Pretriangulated.Triangle.distinguished_iff_of_isZero₂, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, Triangulated.TStructure.triangleLTLTGELT_obj_mor₃, Pretriangulated.Triangle.shift_distinguished_iff, shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, DifferentialObject.Hom.comm_assoc, Functor.shiftIso_inv_naturality, CochainComplex.HomComplex.Cochain.leftUnshift_v, shiftFunctorAdd'_zero_add_inv_app, Adjunction.shift_counit_app, Functor.map_shift_unop, Triangulated.TStructure.triangleLEGT_obj_mor₃, Pretriangulated.invRotate_map_hom₁, Functor.op_commShiftIso_hom_app_assoc, pullbackShiftFunctorZero'_hom_app, CochainComplex.HomComplex.Cochain.rightShift_leftShift, Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, Pretriangulated.comp_distTriang_mor_zero₃₁, Pretriangulated.Triangle.mor₃_eq_zero_of_epi₂, pullbackShiftFunctorZero_hom_app, Functor.shiftMap_comp'_assoc, DifferentialObject.shiftZero_inv_app_f, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, Functor.mapTriangle_map_hom₁, Triangulated.TStructure.isLE_shift, NatTrans.CommShiftCore.shift_app, Pretriangulated.contractible_distinguished₂, CochainComplex.HomComplex.Cochain.leftUnshift_smul, Functor.ShiftSequence.induced_shiftIso_hom_app_obj, NatTrans.shift_comm, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, shift_equiv_triangle, shiftFunctorZero_hom_app_obj_of_induced, Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app_assoc, Functor.shiftIso_zero, Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CochainComplex.shiftFunctor_map_f', shiftFunctorAdd'_add_zero_inv_app, CochainComplex.HomComplex.Cochain.rightShift_zero, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, LocalizerMorphism.commShift_iso_hom_app_assoc, Functor.shiftIso_add, Pretriangulated.Triangle.isZero₂_iff_isIso₃, Functor.commShiftPullback_iso_eq, CochainComplex.quasiIso_shift_iff, CochainComplex.HomComplex.Cochain.rightUnshift_v, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, shiftFunctorCompIsoId_naturality_1_assoc, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃, Pretriangulated.Opposite.OpOpCommShift.iso_hom_app_assoc, CochainComplex.shiftFunctorAdd'_inv_app_f', ShiftedHom.comp_zero, Functor.ShiftSequence.induced.shiftIso_hom_app_obj, Abelian.Ext.hom_comp_singleFunctor_map_shift, Functor.commShiftIso_hom_naturality_assoc, shiftFunctorAdd'_zero_add_hom_app, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, Pretriangulated.commShiftIso_unopUnop_inv_app, Functor.mapTriangleCommShiftIso_hom_app_hom₃, SingleFunctors.shiftIso_add_inv_app, Functor.ShiftSequence.induced_shiftIso_hom_app_obj_assoc, Localization.SmallShiftedHom.equiv_shift', Functor.commShiftIso_comp_inv_app, Functor.mapCochainComplexShiftIso_inv_app_f, LocalizerMorphism.commShift_iso_inv_app_assoc, Functor.map_shiftFunctorCompIsoId_inv_app_assoc, oppositeShiftFunctorZero_inv_app, HomotopyCategory.instLinearIntUpShiftFunctor, Functor.mapTriangleCommShiftIso_inv_app_hom₃, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, Functor.map_shiftFunctorComm_assoc, Triangulated.TStructure.triangleLTGE_map_hom₃, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, Functor.map_shiftFunctorCompIsoId_hom_app_assoc, Pretriangulated.Triangle.invRotate_mor₁, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, CochainComplex.mappingCone.inr_triangleδ_assoc, Triangulated.TStructure.eTriangleLTGE_map_app_hom₁, CochainComplex.HomComplex.Cochain.leftShift_zero, Functor.commShiftIso_hom_naturality, Functor.CommShift.comp_commShiftIso_hom_app, ShiftedHom.comp_neg, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, Pretriangulated.shiftFunctorZero_op_hom_app, Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, DifferentialObject.shiftFunctorAdd_hom_app_f, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, Functor.complete_distinguished_essImageDistTriang_morphism, Shift.instLinearLocalizationShiftFunctorOfCommShiftOfQ, Abelian.Ext.homAddEquiv_apply, Functor.op_commShiftIso_inv_app_assoc, Functor.map_shiftFunctorCompIsoId_hom_app, NatTrans.CommShiftCore.shift_app_assoc, ShiftedHom.comp_smul, shiftFunctorAdd'_add_zero, shiftFunctorCompIsoId_add'_hom_app, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, Triangulated.TStructure.le_shift, Functor.CommShift₂.comm, pullbackShiftFunctorAdd'_hom_app, Pretriangulated.comp_distTriang_mor_zero₂₃, Localization.instHasSmallLocalizedHomObjShiftFunctor, shiftFunctorZero_inv_app_shift, Adjunction.commShiftIso_inv_app_counit_app_assoc, DerivedCategory.instAdditiveShiftFunctorInt, Functor.CommShift.id_commShiftIso_inv_app, CochainComplex.quasiIsoAt_shift_iff, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, ObjectProperty.trW_iff', CochainComplex.instIsKProjectiveObjIntShiftFunctor, Functor.commShiftIso_inv_naturality_assoc, instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom, shiftFunctorAdd'_assoc_inv_app_assoc, Adjunction.LeftAdjointCommShift.iso_inv_app, Functor.mapTriangleInvRotateIso_inv_app_hom₁, CochainComplex.HomComplex.Cochain.rightShift_smul, shiftFunctorAdd'_add_zero_hom_app, shiftComm', Functor.mapTriangleRotateIso_hom_app_hom₃, NatTrans.CommShiftCore.shift_app_comm_assoc, CochainComplex.homOfDegreewiseSplit_f, CochainComplex.shiftFunctorAdd_inv_app_f, Triangulated.Octahedron.map_m₁, Abelian.Ext.add_hom, shiftFunctorAdd_assoc_hom_app_assoc, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, NatTrans.CommShiftCore.shift_comm, Adjunction.unit_app_shift_commShiftIso_inv_app_assoc, ObjectProperty.hasInducedTStructure_iff, Functor.commShiftIso_map₂CochainComplex_inv_app, Functor.commShiftOfLocalization.iso_inv_app_assoc, Triangulated.SpectralObject.Hom.comm_assoc, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, Pretriangulated.rotate_map_hom₃, shiftFunctorZero_hom_app_shift, Adjunction.CommShift.compatibilityCounit_left, Functor.op_commShiftIso_inv_app, Triangulated.TStructure.triangleLTLTGELT_map_hom₂, ShiftedHom.opEquiv'_symm_apply, NatTrans.CommShiftCore.shift_comm_assoc, Functor.mapHomologicalComplex_commShiftIso_inv_app_f, ObjectProperty.extensionProduct_iff, Pretriangulated.binaryProductTriangle_mor₃, shiftFunctor_of_induced, Functor.CommShift.id_commShiftIso_hom_app, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, Adjunction.commShiftIso_hom_app_counit_app_shift_assoc, Triangulated.TStructure.triangleLTGE_map_hom₂, CochainComplex.HomComplex.Cochain.shift_units_smul, Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, MorphismProperty.shift, SingleFunctors.postcomp_shiftIso_inv_app, shiftFunctorAdd_assoc_inv_app_assoc, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, shiftFunctorAdd_assoc, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, Pretriangulated.distinguished_cocone_triangle, ShiftedHom.mk₀_add, Functor.shiftMap_zero, DifferentialObject.objEqToHom_d, Triangulated.TStructure.exists_triangle_zero_one, Triangulated.TStructure.triangleLTGE_obj_mor₃, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂, Pretriangulated.Opposite.OpOpCommShift.iso_inv_app_assoc, Abelian.Ext.zero_hom, Localization.SmallShiftedHom.equiv_shift, Functor.shiftIso_hom_naturality_assoc, Pretriangulated.TriangleOpEquivalence.functor_obj, HasShift.Induced.zero_hom_app_obj, ShiftedHom.add_comp, Adjunction.shift_unit_app, Adjunction.RightAdjointCommShift.iso_hom_app_assoc, Adjunction.unit_app_commShiftIso_hom_app_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, Pretriangulated.TriangleMorphism.comm₃_assoc, Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, Triangulated.SpectralObject.distinguished', Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, Functor.commShiftOfLocalization.iso_hom_app, NatTrans.app_shift_assoc, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality, SingleFunctors.shiftIso_zero, Pretriangulated.distinguished_cocone_triangle₁, CochainComplex.HomComplex.Cochain.leftUnshift_add, DifferentialObject.shiftFunctor_map_f, Pretriangulated.Triangle.π₃Toπ₁_app, Functor.commShiftIso_id_hom_app, Functor.shiftIso_hom_app_comp_assoc, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, Triangulated.TStructure.isIso_truncGT_map_iff, Functor.CommShift.ofIso_commShiftIso_inv_app, Localization.instHasSmallLocalizedHomObjShiftFunctor_3, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃, DerivedCategory.instLinearShiftFunctorInt, oppositeShiftFunctorZero_hom_app, CochainComplex.HomComplex.Cochain.rightShift_units_smul, HomologicalComplex.dgoToHomologicalComplex_map_f, Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_pos, Pretriangulated.Triangle.rotate_obj₃, shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁, shiftZero', CochainComplex.HomComplex.Cochain.rightUnshift_smul, Triangulated.SpectralObject.mapTriangulatedFunctor_δ, Triangulated.TStructure.triangleLEGE_map_hom₁, Triangulated.TStructure.triangleLTLTGELT_map_hom₃, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, DifferentialObject.shiftFunctorAdd_inv_app_f, shiftFunctorAdd_add_zero_inv_app, Pretriangulated.binaryBiproductTriangle_mor₃, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, Pretriangulated.Triangle.functorMk_map_hom₂, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, ShiftedHom.opEquiv_symm_apply_comp, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁, Functor.FullyFaithful.hasShift.map_add_hom_app, Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc, Functor.mapTriangle_map_hom₃, CochainComplex.HomComplex.Cochain.δ_shift, Functor.mapDifferentialObject_obj_d, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, ShiftedHom.opEquiv'_symm_add, Functor.commShiftIso_map₂CochainComplex_flip_inv_app, Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃, shift_shiftFunctorCompIsoId_inv_app, Pretriangulated.Triangle.shiftFunctor_eq, ShiftedHom.opEquiv'_zero_add_symm, ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, shiftEquiv'_unitIso, Pretriangulated.Opposite.distinguished_cocone_triangle, Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, Pretriangulated.Triangle.mono₃, Functor.shift_map_op, Functor.mapTriangleCommShiftIso_inv_app_hom₂, InjectiveResolution.extMk_hom, Pretriangulated.shiftFunctor_op_map, Pretriangulated.rotCompInvRot_inv_app_hom₁, shiftComm_hom_comp, NatTrans.shift_app_assoc, Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, Pretriangulated.productTriangle_mor₃, CochainComplex.HomComplex.Cochain.δ_rightUnshift, ShiftMkCore.shiftFunctor_eq, NatTrans.CommShiftCore.app_shift, Pretriangulated.TriangleOpEquivalence.inverse_obj, Pretriangulated.commShiftIso_opOp_hom_app, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, shift_zero_eq_zero, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, CochainComplex.HomComplex.Cocycle.shift_coe, ShiftedHom.map_smul, Adjunction.CommShift.compatibilityUnit_right, Functor.CommShift.isoAdd'_hom_app, shiftComm_symm, CochainComplex.isStrictlyLE_shift, Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, Triangulated.TStructure.isIso_truncLE_map_iff, shiftFunctorAdd_add_zero_hom_app, Triangulated.SpectralObject.mapTriangulatedFunctor_δ', CochainComplex.HomComplex.Cochain.δ_rightShift, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, shiftFunctorComm_inv_app_of_add_eq_zero, Functor.CommShift.isoZero_inv_app, CochainComplex.HomComplex.Cochain.leftShift_v, Functor.commShiftIso_inv_naturality, CochainComplex.HomComplex.Cochain.rightUnshift_add, Pretriangulated.Triangle.epi₃, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app, HomologicalComplex₂.totalShift₂Iso_hom_naturality, DifferentialObject.Hom.comm, MorphismProperty.IsCompatibleWithShift.condition, Triangulated.TStructure.truncGEπ_comp_truncGEδLT, Pretriangulated.contractibleTriangle_mor₃, CochainComplex.shiftFunctor_obj_X', TwistShiftData.shiftFunctorAdd'_inv_app, CochainComplex.HomComplex.Cochain.shift_v, Pretriangulated.Triangle.shiftFunctor_map_hom₃, CochainComplex.shiftFunctorZero_hom_app_f, Triangulated.TStructure.ω₁δ_app, ShiftedHom.opEquiv'_symm_comp, Abelian.Ext.neg_hom, Triangulated.TStructure.triangleω₁δ_obj_mor₃, Functor.mapTriangleCommShiftIso_hom_app_hom₁, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CochainComplex.HomComplex.Cochain.shiftAddHom_apply, Functor.isoShift_hom_naturality_assoc, CochainComplex.HomComplex.Cochain.δ_leftUnshift, Pretriangulated.commShiftIso_opOp_inv_app_assoc, Pretriangulated.commShiftIso_unopUnop_inv_app_assoc, Adjunction.RightAdjointCommShift.iso_inv_app, CochainComplex.shiftFunctorAdd'_hom_app_f', CochainComplex.HomComplex.Cochain.leftShift_add, Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc, ObjectProperty.HasInducedTStructure.exists_triangle_zero_one, CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain, Functor.map_shift_unop_assoc, Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, Triangulated.Octahedron.comm₂, CochainComplex.shiftEval_hom_app, Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, TwistShiftData.shiftFunctorAdd'_hom_app, Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE, Functor.shiftIso_hom_app_comp_shiftMap, CochainComplex.shiftFunctor_obj_d', Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, Functor.shiftIso_add'_inv_app, CochainComplex.instHasMapBifunctorObjIntShiftFunctor, Triangulated.TStructure.ge_shift, Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃, Triangulated.instNonemptyOctahedron, Functor.mapHomologicalComplex_commShiftIso_hom_app_f, Functor.FullyFaithful.hasShift.map_add_inv_app, Adjunction.RightAdjointCommShift.iso_inv_app_assoc, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, Functor.CommShift.OfComp.map_iso_hom_app_assoc, Triangulated.Localization.distinguished_cocone_triangle, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, Adjunction.unit_app_commShiftIso_hom_app, Pretriangulated.invRotCompRot_hom_app_hom₃, CochainComplex.HomComplex.Cochain.leftShift_units_smul, Functor.commShiftIso_id_inv_app, HomotopyCategory.homologyShiftIso_hom_app, ShiftedHom.map_add, CochainComplex.shiftFunctorAdd_hom_app_f, pullbackShiftFunctorZero'_inv_app, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, shiftFunctorComm_hom_app_of_add_eq_zero, ShiftedHom.opEquiv_symm_apply, shiftFunctorComm_inv_app_of_add_eq_zero_assoc, instIsEquivalenceShiftFunctor, shiftFunctorComm_symm, ShiftedHom.opEquiv'_apply, oppositeShiftFunctorAdd'_hom_app, shiftFunctorComm_eq, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, Quotient.LiftCommShift.iso_inv_app, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, hasExt_iff, Adjunction.LeftAdjointCommShift.iso_hom_app, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, Triangulated.SpectralObject.ω₂_map_hom₂, Functor.ShiftSequence.shiftIso_add, Localization.hasSmallLocalizedShiftedHom_iff, Triangulated.Octahedron'.comm₃_assoc, Pretriangulated.complete_distinguished_triangle_morphism, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, Functor.commShiftOfLocalization_iso_hom_app, Pretriangulated.Triangle.isZero₃_iff, Triangulated.TStructure.triangleLTGE_map_hom₁, CochainComplex.shiftFunctorComm_hom_app_f, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃, Triangulated.AbelianSubcategory.shift_ι_map_ιK_assoc, shiftFunctorAdd_assoc_hom_app, Functor.mapTriangleRotateIso_inv_app_hom₃, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, DifferentialObject.d_squared_assoc, CochainComplex.HomComplex.Cochain.rightShift_neg, HomologicalComplex₂.totalShift₁Iso_hom_naturality, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, Functor.commShiftOfLocalization.iso_hom_app_assoc, Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, NatTrans.app_shift, ShiftedHom.map_zero, Triangulated.TStructure.isGE_shift, Pretriangulated.Triangle.mor₃_eq_zero_of_mono₁, Pretriangulated.Triangle.shiftFunctor_map_hom₂, Pretriangulated.complete_distinguished_triangle_morphism₁, Pretriangulated.shiftFunctorCompIsoId_op_hom_app_assoc, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃, MorphismProperty.IsCompatibleWithTriangulation.compatible_with_triangulation, Functor.mapCochainComplexShiftIso_hom_app_f, Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, SingleFunctors.shiftIso_add_hom_app, shiftFunctorCompIsoId_zero_zero_hom_app, CochainComplex.shiftEval_inv_app, Triangulated.Octahedron'.comm₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, ShiftedHom.mk₀_neg, Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, Functor.shiftIso_inv_naturality_assoc, DifferentialObject.objEqToHom_d_assoc, Triangulated.TStructure.truncGEδLT_comp_truncLTι_app_assoc, Functor.mapTriangleCommShiftIso_hom_app_hom₂, NatTrans.shift_app_comm_assoc, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂, Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃, NatTrans.shift_app, Pretriangulated.commShiftIso_unopUnop_hom_app, DifferentialObject.d_squared_apply_assoc, Triangulated.TStructure.triangleLEGT_map_hom₃, Functor.ShiftSequence.induced_shiftMap, Functor.commShiftIso_eq_ofInduced, shiftFunctorAdd_hom_app_obj_of_induced, Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂, Functor.map_shiftFunctorComm, Functor.op_commShiftIso_hom_app, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, Pretriangulated.Opposite.OpOpCommShift.iso_hom_app, Pretriangulated.Triangle.isZero₁_iff, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, Localization.SmallHom.equiv_shift, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, CochainComplex.isKProjective_shift_iff, Functor.mapTriangleInvRotateIso_hom_app_hom₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, Adjunction.commShiftIso_inv_app_counit_app, shiftFunctorAdd'_assoc_hom_app_assoc, NatTrans.shift_app_comm, Functor.shiftMap_comp_assoc, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_zero, Pretriangulated.commShiftIso_unopUnop_hom_app_assoc, CochainComplex.HomComplex.Cocycle.leftShift_coe, SingleFunctors.shiftIso_zero_hom_app, Triangulated.TStructure.truncGELTδLT_app, Functor.map_shiftFunctorCompIsoId_inv_app, Triangulated.TStructure.eTruncGEδLT_coe, Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁, Abelian.Ext.homLinearEquiv_symm_apply, CochainComplex.HomComplex.Cochain.shift_v', Triangulated.SpectralObject.ω₂_map_hom₃, Triangulated.TStructure.ω₁δ_naturality, Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app, Triangulated.TStructure.triangleLEGT_map_hom₂, Pretriangulated.Opposite.complete_distinguished_triangle_morphism, Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, Functor.CommShift.OfComp.map_iso_inv_app, ObjectProperty.trW.shift, Adjunction.RightAdjointCommShift.iso_hom_app, CochainComplex.HomComplex.Cochain.rightShift_add, CochainComplex.ShiftSequence.shiftIso_inv_app, Triangulated.Octahedron'.comm₃, Localization.SmallShiftedHom.equiv_apply, Pretriangulated.opShiftFunctorEquivalence_functor, Triangulated.Octahedron.comm₄, Functor.commShift₂_comm_assoc, Localization.instHasSmallLocalizedHomObjShiftFunctor_2, CochainComplex.isGE_shift, Triangulated.TStructure.triangleLEGE_obj_mor₃, Functor.FullyFaithful.hasShift.map_zero_inv_app, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂, Functor.ShiftSequence.shiftIso_zero, Functor.commShiftIso_map₂CochainComplex_hom_app, SingleFunctors.shiftIso_add'_inv_app, Pretriangulated.contractible_distinguished₁, CochainComplex.HomComplex.Cocycle.rightUnshift_coe, MorphismProperty.IsCompatibleWithShift.iff, Pretriangulated.productTriangle.zero₃₁, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, Pretriangulated.TriangleOpEquivalence.inverse_map, CochainComplex.HomComplex.Cochain.δ_leftShift, pullbackShiftFunctorAdd'_inv_app, Functor.shiftIso_hom_naturality, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, TwistShiftData.shiftFunctor_map, CochainComplex.HomComplex.CohomologyClass.toHom_mk, TwistShiftData.shiftFunctorZero_inv_app, shiftFunctorCompIsoId_zero_zero_inv_app, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, Adjunction.shift_unit_app_assoc, oppositeShiftFunctorAdd_hom_app, Functor.commShiftUnop_commShiftIso, CochainComplex.liftCycles_shift_homologyπ_assoc, Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app_assoc, Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, Functor.ShiftSequence.induced_shiftMap_assoc, Adjunction.commShiftIso_hom_app_counit_app_shift, ObjectProperty.prop_shiftClosure_iff, Triangulated.TStructure.triangleLEGE_map_hom₂, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, Triangulated.AbelianSubcategory.shift_ι_map_ιK, ShiftedHom.smul_comp, HomRel.IsCompatibleWithShift.condition, CochainComplex.HomComplex.Cochain.leftShift_neg, InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, SingleFunctors.shiftIso_add'_hom_app, Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, ShiftedHom.mk₀_smul, Functor.mapDifferentialObject_map_f, oppositeShiftFunctorAdd'_inv_app, Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, Functor.FullyFaithful.hasShift.map_zero_hom_app, Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁, CochainComplex.HomComplex.Cochain.leftUnshift_neg, shiftFunctorAdd_assoc_inv_app, instAdditiveOppositeShiftShiftFunctor, CochainComplex.isLE_shift, NatTrans.CommShiftCore.app_shift_assoc, shiftFunctorAdd'_assoc_hom_app, Pretriangulated.rotCompInvRot_hom_app_hom₁, SingleFunctors.postcomp_shiftIso_hom_app, Pretriangulated.Triangle.functorMk_obj, Functor.CommShift.isoAdd'_inv_app, Pretriangulated.Triangle.coyoneda_exact₁, Functor.CommShift.OfComp.map_iso_hom_app, Functor.CommShift.OfComp.map_iso_inv_app_assoc, Functor.CommShift.isoZero'_hom_app, GradedObject.shiftFunctor_obj_apply, CochainComplex.HomComplex.Cocycle.rightShift_coe, shiftFunctorAdd_zero_add_inv_app, shiftFunctorComm_hom_app_of_add_eq_zero_assoc, CochainComplex.liftCycles_shift_homologyπ, CochainComplex.HomComplex.Cochain.leftUnshift_zero, Functor.mapTriangle_map_hom₂, Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality, Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, Triangulated.TStructure.isIso_truncGE_map_iff, SingleFunctors.shiftIso_zero_inv_app, Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, Adjunction.shift_counit_app_assoc, shift_neg_shift', ObjectProperty.trW_iff, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, Pretriangulated.shiftFunctorCompIsoId_op_inv_app_assoc, ShiftedHom.opEquiv'_add_symm, Pretriangulated.Triangle.yoneda_exact₃, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, CochainComplex.ShiftSequence.shiftIso_hom_app, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc, Triangulated.Octahedron.comm₂_assoc, Triangulated.TStructure.spectralObject_δ, CochainComplex.mappingCone.map_δ
shiftFunctorAdd 📖	CompOp	37 math math: SingleFunctors.shiftIso_add, Functor.CommShift.isoAdd_hom_app, Functor.shiftIso_add_inv_app, Functor.CommShift.isoAdd_inv_app, HasShift.Induced.add_inv_app_obj, Pretriangulated.Triangle.shiftFunctorAdd_eq, HasShift.Induced.add_hom_app_obj, oppositeShiftFunctorAdd_inv_app, shiftFunctorAdd_zero_add_hom_app, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc, Functor.shiftIso_add_hom_app, shiftFunctorAdd_inv_app_obj_of_induced, Functor.shiftIso_add, SingleFunctors.shiftIso_add_inv_app, DifferentialObject.shiftFunctorAdd_hom_app_f, CochainComplex.shiftFunctorAdd_inv_app_f, shiftFunctorAdd_assoc_hom_app_assoc, shiftFunctorAdd_assoc_inv_app_assoc, CochainComplex.shiftFunctorAdd_eq, shiftFunctorAdd_assoc, ShiftMkCore.shiftFunctorAdd_eq, DifferentialObject.shiftFunctorAdd_inv_app_f, shiftFunctorAdd_add_zero_inv_app, Functor.FullyFaithful.hasShift.map_add_hom_app, shiftFunctorAdd_add_zero_hom_app, Functor.FullyFaithful.hasShift.map_add_inv_app, CochainComplex.shiftFunctorAdd_hom_app_f, Functor.ShiftSequence.shiftIso_add, shiftFunctorAdd_assoc_hom_app, SingleFunctors.shiftIso_add_hom_app, shiftFunctorAdd_hom_app_obj_of_induced, oppositeShiftFunctorAdd_hom_app, shiftFunctorAdd_assoc_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_zero_add_inv_app, ShiftedHom.opEquiv'_add_symm
shiftFunctorAdd' 📖	CompOp	61 math math: Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, shiftFunctorAdd'_assoc_inv_app, Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, Functor.shiftIso_add', shiftFunctorAdd'_zero_add, Functor.shiftIso_hom_app_comp, SingleFunctors.shiftIso_add', CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, Pretriangulated.shiftFunctorAdd'_op_hom_app, Pretriangulated.shiftFunctorAdd'_op_inv_app, shiftFunctorCompIsoId_add'_inv_app, shiftFunctorAdd'_assoc, Functor.shiftIso_add'_hom_app, shiftFunctorAdd'_zero_add_inv_app, Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, shiftFunctorAdd'_add_zero_inv_app, CochainComplex.shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_zero_add_hom_app, Localization.SmallShiftedHom.equiv_shift', CochainComplex.shiftFunctorAdd'_eq, shiftFunctorAdd'_add_zero, shiftFunctorCompIsoId_add'_hom_app, pullbackShiftFunctorAdd'_hom_app, shiftFunctorAdd'_assoc_inv_app_assoc, shiftFunctorAdd'_add_zero_hom_app, shiftFunctorAdd_assoc_hom_app_assoc, ShiftedHom.opEquiv'_symm_apply, shiftFunctorAdd_assoc_inv_app_assoc, shiftFunctorAdd_assoc, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₂, Localization.SmallShiftedHom.equiv_shift, Functor.shiftIso_hom_app_comp_assoc, ShiftedHom.opEquiv_symm_apply_comp, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₁, Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃, Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, Functor.CommShift.isoAdd'_hom_app, TwistShiftData.shiftFunctorAdd'_inv_app, Pretriangulated.Triangle.shiftFunctorAdd'_eq, CochainComplex.shiftFunctorAdd'_hom_app_f', Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₁, TwistShiftData.shiftFunctorAdd'_hom_app, Functor.shiftIso_hom_app_comp_shiftMap, Functor.shiftIso_add'_inv_app, ShiftedHom.opEquiv'_apply, oppositeShiftFunctorAdd'_hom_app, shiftFunctorComm_eq, Pretriangulated.Triangle.shiftFunctorAdd'_inv_app_hom₃, shiftFunctorAdd_assoc_hom_app, Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂, shiftFunctorAdd'_assoc_hom_app_assoc, SingleFunctors.shiftIso_add'_inv_app, pullbackShiftFunctorAdd'_inv_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, SingleFunctors.shiftIso_add'_hom_app, oppositeShiftFunctorAdd'_inv_app, shiftFunctorAdd_assoc_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_assoc_hom_app, Functor.CommShift.isoAdd'_inv_app, Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply
shiftFunctorComm 📖	CompOp	26 math math: Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, shiftFunctorComm_zero_hom_app, Functor.map_shiftFunctorComm_hom_app, Pretriangulated.Triangle.shiftFunctor_map_hom₁, shiftFunctorComm_eq_refl, Pretriangulated.Triangle.shiftFunctor_obj, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc, Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, Functor.map_shiftFunctorComm_assoc, shiftFunctorZero_inv_app_shift, shiftFunctorZero_hom_app_shift, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, shiftFunctorComm_inv_app_of_add_eq_zero, Pretriangulated.Triangle.shiftFunctor_map_hom₃, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, shiftFunctorComm_hom_app_of_add_eq_zero, shiftFunctorComm_inv_app_of_add_eq_zero_assoc, shiftFunctorComm_symm, shiftFunctorComm_eq, CochainComplex.shiftFunctorComm_hom_app_f, Pretriangulated.Triangle.shiftFunctor_map_hom₂, Functor.map_shiftFunctorComm, shiftFunctorComm_hom_app_of_add_eq_zero_assoc
shiftFunctorCompIsoId 📖	CompOp	51 math math: Pretriangulated.shiftFunctorCompIsoId_op_hom_app, shift_shiftFunctorCompIsoId_hom_app, Pretriangulated.Triangle.invRotate_mor₃, Adjunction.LeftAdjointCommShift.iso_hom_app_assoc, shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app, Adjunction.LeftAdjointCommShift.iso_inv_app_assoc, Pretriangulated.shiftFunctorCompIsoId_op_inv_app, Pretriangulated.invRotCompRot_inv_app_hom₃, shiftFunctorCompIsoId_naturality_1, shift_shift_neg', shiftFunctorCompIsoId_add'_inv_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, shiftFunctorCompIsoId_naturality_1_assoc, Functor.map_shiftFunctorCompIsoId_inv_app_assoc, Functor.map_shiftFunctorCompIsoId_hom_app_assoc, Pretriangulated.Triangle.invRotate_mor₁, Functor.map_shiftFunctorCompIsoId_hom_app, shiftFunctorCompIsoId_add'_hom_app, Adjunction.LeftAdjointCommShift.iso_inv_app, Adjunction.RightAdjointCommShift.iso_hom_app_assoc, shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app, Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, shift_shiftFunctorCompIsoId_inv_app, shiftEquiv'_unitIso, Pretriangulated.rotCompInvRot_inv_app_hom₁, shiftFunctorComm_inv_app_of_add_eq_zero, shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app, Adjunction.RightAdjointCommShift.iso_inv_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, Adjunction.RightAdjointCommShift.iso_inv_app_assoc, Pretriangulated.invRotCompRot_hom_app_hom₃, shiftFunctorComm_hom_app_of_add_eq_zero, shiftFunctorComm_inv_app_of_add_eq_zero_assoc, shiftEquiv'_counitIso, Adjunction.LeftAdjointCommShift.iso_hom_app, Pretriangulated.shiftFunctorCompIsoId_op_hom_app_assoc, shiftFunctorCompIsoId_zero_zero_hom_app, Functor.map_shiftFunctorCompIsoId_inv_app, Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, Adjunction.RightAdjointCommShift.iso_hom_app, shiftFunctorCompIsoId_zero_zero_inv_app, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, Pretriangulated.rotCompInvRot_hom_app_hom₁, shiftFunctorComm_hom_app_of_add_eq_zero_assoc, shift_neg_shift', Pretriangulated.shiftFunctorCompIsoId_op_inv_app_assoc, Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc
shiftFunctorZero 📖	CompOp	57 math math: shiftFunctorZero_inv_app_obj_of_induced, shiftFunctorComm_zero_hom_app, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁, CochainComplex.shiftFunctorZero_eq, shiftFunctorAdd'_zero_add, Pretriangulated.shiftFunctorZero_op_inv_app, Functor.shiftIso_zero_inv_app, Functor.CommShift.isoZero_hom_app, DifferentialObject.shiftZero_hom_app_f, HasShift.Induced.zero_inv_app_obj, pullbackShiftFunctorZero_inv_app, Functor.shiftIso_zero_hom_app, Pretriangulated.Triangle.shiftFunctorZero_eq, shiftFunctorAdd_zero_add_hom_app, CochainComplex.shiftFunctorZero_inv_app_f, TwistShiftData.shiftFunctorZero_hom_app, shiftFunctorAdd'_zero_add_inv_app, pullbackShiftFunctorZero'_hom_app, Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, pullbackShiftFunctorZero_hom_app, DifferentialObject.shiftZero_inv_app_f, shiftFunctorZero_hom_app_obj_of_induced, Functor.shiftIso_zero, shiftFunctorAdd'_add_zero_inv_app, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₃, shiftFunctorAdd'_zero_add_hom_app, oppositeShiftFunctorZero_inv_app, Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, Pretriangulated.shiftFunctorZero_op_hom_app, shiftFunctorAdd'_add_zero, shiftFunctorZero_inv_app_shift, shiftFunctorAdd'_add_zero_hom_app, shiftFunctorZero_hom_app_shift, HasShift.Induced.zero_hom_app_obj, ShiftMkCore.shiftFunctorZero_eq, SingleFunctors.shiftIso_zero, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₃, oppositeShiftFunctorZero_hom_app, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₁, shiftFunctorAdd_add_zero_inv_app, ShiftedHom.opEquiv'_zero_add_symm, shiftFunctorAdd_add_zero_hom_app, Functor.CommShift.isoZero_inv_app, CochainComplex.shiftFunctorZero_hom_app_f, pullbackShiftFunctorZero'_inv_app, shiftFunctorCompIsoId_zero_zero_hom_app, Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, SingleFunctors.shiftIso_zero_hom_app, Functor.FullyFaithful.hasShift.map_zero_inv_app, Pretriangulated.Triangle.shiftFunctorZero_hom_app_hom₂, Functor.ShiftSequence.shiftIso_zero, TwistShiftData.shiftFunctorZero_inv_app, shiftFunctorCompIsoId_zero_zero_inv_app, Functor.FullyFaithful.hasShift.map_zero_hom_app, shiftFunctorAdd_zero_add_inv_app, SingleFunctors.shiftIso_zero_inv_app
shiftFunctorZero' 📖	CompOp	4 math math: Functor.CommShift.isoZero'_inv_app, pullbackShiftFunctorZero'_hom_app, pullbackShiftFunctorZero'_inv_app, Functor.CommShift.isoZero'_hom_app
shiftMonoidalFunctor 📖	CompOp	—
shiftNegShift 📖	CompOp	1 math math: shift_equiv_triangle
shiftShiftNeg 📖	CompOp	1 math math: shift_equiv_triangle
shiftZero 📖	CompOp	1 math math: shiftZero'
«term_⟦_⟧'» 📖	CompOp	—
«term_⟦_⟧» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsEquivalenceShiftFunctor 📖	mathematical	—	Functor.IsEquivalence shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	Equivalence.isEquivalence_functor
shiftComm' 📖	mathematical	—	Functor.map shiftFunctor AddCommMonoid.toAddMonoid Functor.obj CategoryStruct.comp Category.toCategoryStruct Iso.hom shiftComm	—	shiftComm_symm NatTrans.naturality_assoc Iso.hom_inv_id_app Category.comp_id
shiftComm_hom_comp 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddCommMonoid.toAddMonoid Iso.hom shiftComm Functor.map	—	shiftComm' shiftComm_symm Iso.symm_hom Iso.inv_hom_id_assoc
shiftComm_hom_comp_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddCommMonoid.toAddMonoid Iso.hom shiftComm Functor.map	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftComm_hom_comp
shiftComm_symm 📖	mathematical	—	Iso.symm Functor.obj shiftFunctor AddCommMonoid.toAddMonoid shiftComm	—	Iso.ext NatTrans.congr_app shiftFunctorComm_symm
shiftEquiv'_counitIso 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Equivalence.counitIso shiftEquiv' shiftFunctorCompIsoId SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
shiftEquiv'_functor 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Equivalence.functor shiftEquiv' shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
shiftEquiv'_inverse 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Equivalence.inverse shiftEquiv' shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
shiftEquiv'_unitIso 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Equivalence.unitIso shiftEquiv' Iso.symm Functor Functor.category Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.id shiftFunctorCompIsoId	—	—
shiftFunctorAdd'_add_zero 📖	mathematical	—	shiftFunctorAdd' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass add_zero Iso.trans Functor Functor.category shiftFunctor Functor.comp Functor.id Iso.symm Functor.rightUnitor Functor.isoWhiskerLeft shiftFunctorZero	—	Iso.ext add_zero NatTrans.ext' Functor.congr_obj eqToHom_app ε_app_obj eqToHom_map Category.id_comp
shiftFunctorAdd'_add_zero_hom_app 📖	mathematical	—	NatTrans.app shiftFunctor Functor.comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.hom Functor Functor.category shiftFunctorAdd' add_zero Functor.id Iso.inv shiftFunctorZero Functor.obj	—	add_zero Category.id_comp NatTrans.congr_app shiftFunctorAdd'_add_zero
shiftFunctorAdd'_add_zero_inv_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.inv Functor Functor.category shiftFunctorAdd' add_zero Functor.id Iso.hom shiftFunctorZero Functor.obj	—	add_zero Category.comp_id NatTrans.congr_app shiftFunctorAdd'_add_zero
shiftFunctorAdd'_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	Iso.trans Functor Functor.category shiftFunctor Functor.comp shiftFunctorAdd' Functor.isoWhiskerRight Functor.associator Functor.isoWhiskerLeft	—	Iso.ext NatTrans.ext' shiftFunctorAdd'_eq_shiftFunctorAdd Category.comp_id Functor.congr_obj eqToHom_app obj_μ_inv_app eqToHom_map δ_μ_app_assoc Category.assoc
shiftFunctorAdd'_assoc_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor Functor.comp NatTrans.app Iso.hom Functor Functor.category shiftFunctorAdd' Functor.map	—	Category.comp_id NatTrans.congr_app shiftFunctorAdd'_assoc
shiftFunctorAdd'_assoc_hom_app_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor NatTrans.app Functor.comp Iso.hom Functor Functor.category shiftFunctorAdd' Functor.map	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorAdd'_assoc_hom_app
shiftFunctorAdd'_assoc_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor Functor.comp Functor.map NatTrans.app Iso.inv Functor Functor.category shiftFunctorAdd'	—	Category.assoc Category.id_comp NatTrans.congr_app shiftFunctorAdd'_assoc
shiftFunctorAdd'_assoc_inv_app_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor Functor.map NatTrans.app Functor.comp Iso.inv Functor Functor.category shiftFunctorAdd'	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorAdd'_assoc_inv_app
shiftFunctorAdd'_eq_shiftFunctorAdd 📖	mathematical	—	shiftFunctorAdd' AddSemigroup.toAdd AddMonoid.toAddSemigroup shiftFunctorAdd	—	Iso.ext Category.id_comp
shiftFunctorAdd'_zero_add 📖	mathematical	—	shiftFunctorAdd' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero_add Iso.trans Functor Functor.category shiftFunctor Functor.comp Functor.id Iso.symm Functor.leftUnitor Functor.isoWhiskerRight shiftFunctorZero	—	Iso.ext zero_add NatTrans.ext' Functor.congr_obj eqToHom_app obj_ε_app eqToHom_map Category.id_comp
shiftFunctorAdd'_zero_add_hom_app 📖	mathematical	—	NatTrans.app shiftFunctor Functor.comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.hom Functor Functor.category shiftFunctorAdd' zero_add Functor.map Functor.obj Functor.id Iso.inv shiftFunctorZero	—	zero_add Category.id_comp NatTrans.congr_app shiftFunctorAdd'_zero_add
shiftFunctorAdd'_zero_add_inv_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.inv Functor Functor.category shiftFunctorAdd' zero_add Functor.map Functor.obj Functor.id Iso.hom shiftFunctorZero	—	zero_add Category.comp_id NatTrans.congr_app shiftFunctorAdd'_zero_add
shiftFunctorAdd_add_zero_hom_app 📖	mathematical	—	NatTrans.app shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Functor.comp Iso.hom Functor Functor.category shiftFunctorAdd CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id eqToHom Iso.inv shiftFunctorZero	—	Functor.congr_obj add_zero eqToHom_app eqToHom_trans_assoc Category.id_comp
shiftFunctorAdd_add_zero_inv_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup Iso.inv Functor Functor.category shiftFunctorAdd CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id Iso.hom shiftFunctorZero eqToHom	—	Functor.congr_obj add_zero eqToHom_app Category.assoc eqToHom_trans Category.comp_id
shiftFunctorAdd_assoc 📖	mathematical	—	Iso.trans Functor Functor.category shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup Functor.comp shiftFunctorAdd Functor.isoWhiskerRight Functor.associator shiftFunctorAdd' add_assoc Functor.isoWhiskerLeft	—	Iso.ext add_assoc NatTrans.ext' Category.comp_id shiftFunctorAdd'_eq_shiftFunctorAdd NatTrans.congr_app shiftFunctorAdd'_assoc
shiftFunctorAdd_assoc_hom_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup Functor.comp NatTrans.app Iso.hom Functor Functor.category shiftFunctorAdd Functor.map shiftFunctorAdd' add_assoc	—	add_assoc Category.comp_id NatTrans.congr_app shiftFunctorAdd_assoc
shiftFunctorAdd_assoc_hom_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup NatTrans.app Functor.comp Iso.hom Functor Functor.category shiftFunctorAdd Functor.map shiftFunctorAdd' add_assoc	—	add_assoc Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorAdd_assoc_hom_app
shiftFunctorAdd_assoc_inv_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor Functor.comp AddSemigroup.toAdd AddMonoid.toAddSemigroup Functor.map NatTrans.app Iso.inv Functor Functor.category shiftFunctorAdd shiftFunctorAdd' add_assoc	—	add_assoc Category.assoc Category.id_comp NatTrans.congr_app shiftFunctorAdd_assoc
shiftFunctorAdd_assoc_inv_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup Functor.map NatTrans.app Functor.comp Iso.inv Functor Functor.category shiftFunctorAdd shiftFunctorAdd' add_assoc	—	add_assoc Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorAdd_assoc_inv_app
shiftFunctorAdd_zero_add_hom_app 📖	mathematical	—	NatTrans.app shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Functor.comp Iso.hom Functor Functor.category shiftFunctorAdd CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id eqToHom Functor.map Iso.inv shiftFunctorZero	—	Functor.congr_obj zero_add eqToHom_app eqToHom_trans_assoc Category.id_comp
shiftFunctorAdd_zero_add_inv_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup Iso.inv Functor Functor.category shiftFunctorAdd CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id Functor.map Iso.hom shiftFunctorZero eqToHom	—	Functor.congr_obj zero_add eqToHom_app Category.assoc eqToHom_trans Category.comp_id
shiftFunctorComm_eq 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	shiftFunctorComm Iso.trans Functor Functor.category Functor.comp shiftFunctor AddCommMonoid.toAddMonoid Iso.symm shiftFunctorAdd'	—	shiftFunctorAdd'_eq_shiftFunctorAdd
shiftFunctorComm_eq_refl 📖	mathematical	—	shiftFunctorComm Iso.refl Functor Functor.category Functor.comp shiftFunctor AddCommMonoid.toAddMonoid	—	shiftFunctorComm_eq Iso.symm_self_id
shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.comp shiftFunctor AddCommMonoid.toAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NatTrans.app Iso.hom Functor Functor.category shiftFunctorComm Functor.map AddSemigroup.toAdd AddMonoid.toAddSemigroup shiftFunctorAdd	—	cancel_mono mono_of_strongMono strongMono_of_isIso NatIso.inv_app_isIso Functor.map_isIso Category.assoc Iso.hom_inv_id_app Category.id_comp shiftFunctorComm_eq Functor.map_id Category.comp_id add_assoc add_comm shiftFunctorAdd'_assoc_hom_app_assoc Iso.hom_inv_id_app_assoc shiftFunctorAdd'_assoc_hom_app Iso.inv_hom_id_app_assoc
shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddCommMonoid.toAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NatTrans.app Functor.comp Iso.hom Functor Functor.category shiftFunctorComm Functor.map AddSemigroup.toAdd AddMonoid.toAddSemigroup shiftFunctorAdd	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app
shiftFunctorComm_hom_app_of_add_eq_zero 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	NatTrans.app Functor.comp shiftFunctor AddCommMonoid.toAddMonoid Iso.hom Functor Functor.category shiftFunctorComm CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id shiftFunctorCompIsoId Iso.inv	—	shiftFunctorComm_eq Category.assoc Iso.hom_inv_id_app_assoc
shiftFunctorComm_hom_app_of_add_eq_zero_assoc 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddCommMonoid.toAddMonoid NatTrans.app Functor.comp Iso.hom Functor Functor.category shiftFunctorComm Functor.id shiftFunctorCompIsoId Iso.inv	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorComm_hom_app_of_add_eq_zero
shiftFunctorComm_inv_app_of_add_eq_zero 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	NatTrans.app Functor.comp shiftFunctor AddCommMonoid.toAddMonoid Iso.inv Functor Functor.category shiftFunctorComm CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id Iso.hom shiftFunctorCompIsoId	—	shiftFunctorComm_eq Category.assoc Iso.hom_inv_id_app_assoc
shiftFunctorComm_inv_app_of_add_eq_zero_assoc 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor AddCommMonoid.toAddMonoid NatTrans.app Functor.comp Iso.inv Functor Functor.category shiftFunctorComm Functor.id Iso.hom shiftFunctorCompIsoId	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorComm_inv_app_of_add_eq_zero
shiftFunctorComm_symm 📖	mathematical	—	Iso.symm Functor Functor.category Functor.comp shiftFunctor AddCommMonoid.toAddMonoid shiftFunctorComm	—	Iso.ext shiftFunctorComm_eq add_comm
shiftFunctorComm_zero_hom_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor AddCommMonoid.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.hom Functor Functor.category shiftFunctorComm CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id shiftFunctorZero Functor.map Iso.inv	—	shiftFunctorZero_hom_app_shift Category.assoc Iso.hom_inv_id_app Functor.map_id Category.comp_id
shiftFunctorCompIsoId_add'_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	NatTrans.app Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.id Iso.hom Functor Functor.category shiftFunctorCompIsoId CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map shiftFunctorAdd'	—	cancel_mono mono_of_strongMono strongMono_of_isIso NatIso.inv_app_isIso Iso.hom_inv_id_app shiftFunctorCompIsoId_add'_inv_app Category.assoc Iso.hom_inv_id_app_assoc Functor.map_comp_assoc Functor.map_id Category.id_comp Functor.map_comp
shiftFunctorCompIsoId_add'_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	NatTrans.app Functor.id Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Iso.inv Functor Functor.category shiftFunctorCompIsoId CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map shiftFunctorAdd'	—	Functor.map_comp Category.assoc NatTrans.naturality cancel_mono mono_of_strongMono strongMono_of_isIso NatIso.inv_app_isIso Iso.hom_inv_id_app AddRightCancelSemigroup.toIsRightCancelAdd add_assoc shiftFunctorAdd'_assoc_inv_app Functor.map_comp_assoc add_zero Iso.hom_inv_id_app_assoc shiftFunctorAdd'_add_zero_hom_app Functor.map_id Category.id_comp
shiftFunctorCompIsoId_naturality_1 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.id Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NatTrans.app Iso.inv Functor Functor.category shiftFunctorCompIsoId Functor.map Iso.hom	—	NatIso.naturality_1
shiftFunctorCompIsoId_naturality_1_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NatTrans.app Functor.id Functor.comp Iso.inv Functor Functor.category shiftFunctorCompIsoId Functor.map Iso.hom	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorCompIsoId_naturality_1
shiftFunctorCompIsoId_zero_zero_hom_app 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Functor.id Iso.hom Functor Functor.category shiftFunctorCompIsoId add_zero CategoryStruct.comp Category.toCategoryStruct Functor.obj Functor.map shiftFunctorZero	—	add_zero shiftFunctorAdd'_zero_add_inv_app
shiftFunctorCompIsoId_zero_zero_inv_app 📖	mathematical	—	NatTrans.app Functor.id Functor.comp shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.inv Functor Functor.category shiftFunctorCompIsoId add_zero CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctorZero Functor.map	—	add_zero shiftFunctorAdd'_zero_add_hom_app
shiftFunctorZero_hom_app_shift 📖	mathematical	—	NatTrans.app shiftFunctor AddCommMonoid.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Functor.id Iso.hom Functor Functor.category shiftFunctorZero Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.comp shiftFunctorComm Functor.map	—	zero_add shiftFunctorAdd'_zero_add_inv_app add_zero shiftFunctorComm_eq Category.assoc Iso.hom_inv_id_app Category.comp_id shiftFunctorAdd'_add_zero_inv_app
shiftFunctorZero_inv_app_shift 📖	mathematical	—	NatTrans.app Functor.id shiftFunctor AddCommMonoid.toAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.inv Functor Functor.category shiftFunctorZero Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.comp Functor.map shiftFunctorComm	—	cancel_mono mono_of_strongMono strongMono_of_isIso NatIso.hom_app_isIso Category.assoc Iso.inv_hom_id_app shiftFunctorZero_hom_app_shift Iso.inv_hom_id_app_assoc Functor.map_comp Functor.map_id
shiftZero' 📖	mathematical	—	Functor.map shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryStruct.comp Category.toCategoryStruct Functor.obj Iso.hom shiftZero Iso.inv	—	Iso.app_inv Iso.app_hom NatIso.naturality_2
shift_equiv_triangle 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Functor.obj shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Functor.map Iso.inv shiftShiftNeg Iso.hom shiftNegShift CategoryStruct.id	—	Equivalence.functor_unitIso_comp
shift_neg_shift' 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.obj NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid CategoryStruct.comp Category.toCategoryStruct Functor.comp Functor.id NatTrans.app Iso.hom Functor Functor.category shiftFunctorCompIsoId neg_add_cancel Iso.inv	—	neg_add_cancel NatIso.naturality_2
shift_shift' 📖	mathematical	—	Functor.map shiftFunctor Functor.obj CategoryStruct.comp Category.toCategoryStruct AddSemigroup.toAdd AddMonoid.toAddSemigroup Iso.inv shiftAdd Iso.hom	—	NatTrans.naturality Iso.inv_hom_id_app_assoc
shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.obj Functor.comp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Functor.id NatTrans.app Iso.hom Functor Functor.category shiftFunctorCompIsoId add_neg_cancel neg_add_cancel	—	shift_shiftFunctorCompIsoId_hom_app add_neg_cancel
shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.obj Functor.id Functor.comp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NatTrans.app Iso.inv Functor Functor.category shiftFunctorCompIsoId add_neg_cancel neg_add_cancel	—	shift_shiftFunctorCompIsoId_inv_app add_neg_cancel
shift_shiftFunctorCompIsoId_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.obj Functor.comp Functor.id NatTrans.app Iso.hom Functor Functor.category shiftFunctorCompIsoId	—	zero_add add_zero Functor.map_comp shiftFunctorAdd'_zero_add_inv_app shiftFunctorAdd'_add_zero_inv_app shiftFunctorAdd'_assoc_inv_app neg_eq_of_add_eq_zero_left add_neg_cancel
shift_shiftFunctorCompIsoId_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Functor.obj Functor.id Functor.comp NatTrans.app Iso.inv Functor Functor.category shiftFunctorCompIsoId	—	cancel_mono Functor.map_mono Functor.preservesMonomorphisms_of_isRightAdjoint Functor.isRightAdjoint_of_isEquivalence instIsEquivalenceShiftFunctor mono_of_strongMono strongMono_of_isIso NatIso.hom_app_isIso Functor.map_comp Iso.inv_hom_id_app Functor.map_id shift_shiftFunctorCompIsoId_hom_app
shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Functor.obj Functor.comp Functor.id NatTrans.app Iso.hom Functor Functor.category shiftFunctorCompIsoId neg_add_cancel add_neg_cancel	—	shift_shiftFunctorCompIsoId_hom_app neg_add_cancel
shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Functor.obj Functor.id Functor.comp NatTrans.app Iso.inv Functor Functor.category shiftFunctorCompIsoId neg_add_cancel add_neg_cancel	—	shift_shiftFunctorCompIsoId_inv_app neg_add_cancel
shift_shift_neg' 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.comp Functor.id NatTrans.app Iso.hom Functor Functor.category shiftFunctorCompIsoId add_neg_cancel Iso.inv	—	add_neg_cancel NatIso.naturality_2
shift_zero_eq_zero 📖	mathematical	—	Functor.map shiftFunctor SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasZeroMorphisms.zero Functor.obj	—	Functor.map_zero Functor.preservesZeroMorphisms_of_full Functor.IsEquivalence.full instIsEquivalenceShiftFunctor

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
hasShift 📖	CompOp	1 math math: CategoryTheory.Functor.shiftFunctorIso_ofHasShiftOfFullyFaithful

CategoryTheory.Functor.FullyFaithful.hasShift

Definitions

Name	Category	Theorems
add 📖	CompOp	2 math math: map_add_hom_app, map_add_inv_app
zero 📖	CompOp	2 math math: map_zero_inv_app, map_zero_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_hom_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.shiftFunctorAdd CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.FullyFaithful.map_preimage
map_add_inv_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.comp AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Iso.hom CategoryTheory.shiftFunctorAdd	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Functor.FullyFaithful.map_preimage
map_zero_hom_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category zero CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.shiftFunctor CategoryTheory.shiftFunctorZero	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.FullyFaithful.map_preimage
map_zero_inv_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category zero CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Functor.comp CategoryTheory.shiftFunctorZero	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Functor.FullyFaithful.map_preimage

CategoryTheory.HasShift

Definitions

Name	Category	Theorems
shift 📖	CompOp	—
shiftMonoidal 📖	CompOp	—

CategoryTheory.ShiftMkCore

Definitions

Name	Category	Theorems
F 📖	CompOp	9 math math: add_zero_hom_app, assoc_inv_app_assoc, add_zero_inv_app, shiftFunctor_eq, zero_add_hom_app, assoc_hom_app, zero_add_inv_app, assoc_hom_app_assoc, assoc_inv_app
add 📖	CompOp	9 math math: add_zero_hom_app, assoc_inv_app_assoc, add_zero_inv_app, shiftFunctorAdd_eq, zero_add_hom_app, assoc_hom_app, zero_add_inv_app, assoc_hom_app_assoc, assoc_inv_app
zero 📖	CompOp	5 math math: add_zero_hom_app, add_zero_inv_app, shiftFunctorZero_eq, zero_add_hom_app, zero_add_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_zero_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app F AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.eqToHom CategoryTheory.Iso.inv zero	—	—
add_zero_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp F AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Iso.hom zero CategoryTheory.eqToHom	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Iso.hom_inv_id_app add_zero_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl
assoc_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.Functor.map CategoryTheory.eqToHom	—	—
assoc_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.Functor.map CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' assoc_hom_app
assoc_inv_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F CategoryTheory.Functor.comp AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.eqToHom	—	CategoryTheory.cancel_mono CategoryTheory.mono_comp CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Functor.map_comp CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id assoc_hom_app CategoryTheory.eqToHom_trans_assoc CategoryTheory.eqToHom_refl CategoryTheory.Category.id_comp
assoc_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj F AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' assoc_inv_app
shiftFunctorAdd_eq 📖	mathematical	—	CategoryTheory.shiftFunctorAdd CategoryTheory.hasShiftMk add	—	—
shiftFunctorZero_eq 📖	mathematical	—	CategoryTheory.shiftFunctorZero CategoryTheory.hasShiftMk zero	—	—
shiftFunctor_eq 📖	mathematical	—	CategoryTheory.shiftFunctor CategoryTheory.hasShiftMk F	—	—
zero_add_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app F AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.eqToHom CategoryTheory.Functor.map CategoryTheory.Iso.inv zero	—	—
zero_add_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp F AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Iso.hom zero CategoryTheory.eqToHom	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Iso.hom_inv_id_app zero_add_hom_app CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl

---

← Back to Index