CommShift

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

Statistics

Metric	Count
Definitions `CommShift`, `CommShift`, `CommShift`, `iso`, `commShiftIso`, `comp`, `id`, `iso`, `isoAdd`, `isoAdd'`, `isoZero`, `isoZero'`, `ofComp`, `ofHasShiftOfFullyFaithful`, `ofIso`, `CommShift`, `CommShiftCore`	17
Theorems `map_iso_hom_app`, `map_iso_hom_app_assoc`, `map_iso_inv_app`, `map_iso_inv_app_assoc`, `add`, `commShiftIso_add`, `commShiftIso_zero`, `comp_commShiftIso_hom_app`, `comp_commShiftIso_inv_app`, `id_commShiftIso_hom_app`, `id_commShiftIso_inv_app`, `isoAdd'_assoc`, `isoAdd'_hom_app`, `isoAdd'_inv_app`, `isoAdd'_isoZero`, `isoAdd_hom_app`, `isoAdd_inv_app`, `isoZero'_eq_isoZero`, `isoZero'_hom_app`, `isoZero'_inv_app`, `isoZero_hom_app`, `isoZero_inv_app`, `isoZero_isoAdd'_`, `ofComp_compatibility`, `ofIso_commShiftIso_hom_app`, `ofIso_commShiftIso_inv_app`, `ofIso_compatibility`, `zero`, `commShiftIso_add'`, `commShiftIso_comp_hom_app`, `commShiftIso_comp_inv_app`, `commShiftIso_hom_naturality`, `commShiftIso_hom_naturality_assoc`, `commShiftIso_id_hom_app`, `commShiftIso_id_inv_app`, `commShiftIso_inv_naturality`, `commShiftIso_inv_naturality_assoc`, `commShiftIso_zero'`, `map_shiftFunctorComm`, `map_shiftFunctorComm_assoc`, `map_shiftFunctorComm_hom_app`, `map_shiftFunctorCompIsoId_hom_app`, `map_shiftFunctorCompIsoId_hom_app_assoc`, `map_shiftFunctorCompIsoId_inv_app`, `map_shiftFunctorCompIsoId_inv_app_assoc`, `shiftFunctorIso_ofHasShiftOfFullyFaithful`, `associator`, `comp`, `id`, `leftUnitor`, `of_core`, `of_isIso`, `of_iso_inv`, `of_iso_symm`, `rightUnitor`, `shift_comm`, `verticalComposition`, `whiskerLeft`, `whiskerRight`, `add`, `app_shift`, `app_shift_assoc`, `shift_app`, `shift_app_assoc`, `shift_app_comm`, `shift_app_comm_assoc`, `shift_comm`, `shift_comm_assoc`, `zero`, `app_shift`, `app_shift_assoc`, `shift_app`, `shift_app_assoc`, `shift_app_comm`, `shift_app_comm_assoc`, `shift_comm`, `shift_comm_assoc`	77
Total	94

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`CommShift` 📖	CompData	9 math math: `CommShift.mk'`, `CommShift.instId`, `IsTriangulated.commShift`, `commShiftPullback`, `commShift_of_leftAdjoint`, `commShift_op`, `CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int`, `CommShift.instComp`, `commShift_of_rightAdjoint`

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`CommShift` 📖	MathDef	8 math math: `CommShift.mk'`, `CommShift.instTrans`, `CommShift.instRefl`, `CommShift.mk''`, `commShift_of_functor`, `CategoryTheory.Pretriangulated.instCommShiftOppositeOpOpEquivalenceInt`, `commShift_of_inverse`, `CommShift.instSymm`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`CommShift` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftIso_add'` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CommShift.commShiftIso` `CommShift.isoAdd'`	—	`CommShift.commShiftIso_add`
`commShiftIso_comp_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `CommShift.comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `map`	—	`CommShift.comp_commShiftIso_hom_app`
`commShiftIso_comp_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `CommShift.comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `map`	—	`CommShift.comp_commShiftIso_inv_app`
`commShiftIso_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `comp` `map` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CommShift.commShiftIso`	—	`CategoryTheory.NatTrans.naturality`
`commShiftIso_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `map` `CategoryTheory.NatTrans.app` `comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShiftIso_hom_naturality`
`commShiftIso_id_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `CategoryTheory.shiftFunctor` `id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `CommShift.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`CommShift.id_commShiftIso_hom_app`
`commShiftIso_id_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `comp` `id` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CommShift.commShiftIso` `CommShift.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `obj`	—	`CommShift.id_commShiftIso_inv_app`
`commShiftIso_inv_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `comp` `map` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CommShift.commShiftIso`	—	`CategoryTheory.NatTrans.naturality`
`commShiftIso_inv_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `map` `CategoryTheory.NatTrans.app` `comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShiftIso_inv_naturality`
`commShiftIso_zero'` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`CommShift.commShiftIso` `CommShift.isoZero'`	—	`CommShift.isoZero'_eq_isoZero` `CommShift.commShiftIso_zero`
`map_shiftFunctorComm` 📖	mathematical	—	`map` `obj` `comp` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorComm` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.NatTrans.congr_app` `CommShift.commShiftIso_add` `CategoryTheory.shiftFunctorComm_eq` `CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CommShift.isoAdd_hom_app` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `map_isIso` `CategoryTheory.NatIso.inv_app_isIso` `map_comp_assoc` `CategoryTheory.Iso.inv_hom_id_app` `map_id` `CategoryTheory.Category.id_comp` `add_comm` `map_comp` `commShiftIso_add'` `CommShift.isoAdd'_hom_app` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id`
`map_shiftFunctorComm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `map` `CategoryTheory.NatTrans.app` `comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorComm` `CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_shiftFunctorComm`
`map_shiftFunctorComm_hom_app` 📖	mathematical	—	`map` `obj` `comp` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorComm` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.NatTrans.congr_app` `CommShift.commShiftIso_add` `CategoryTheory.shiftFunctorComm_eq` `CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CommShift.isoAdd_hom_app` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `map_isIso` `CategoryTheory.NatIso.inv_app_isIso` `map_comp_assoc` `CategoryTheory.Iso.inv_hom_id_app` `map_id` `CategoryTheory.Category.id_comp` `map_comp` `add_comm` `commShiftIso_add'` `CommShift.isoAdd'_hom_app` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id`
`map_shiftFunctorCompIsoId_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`map` `obj` `comp` `CategoryTheory.shiftFunctor` `id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CommShift.commShiftIso`	—	`CategoryTheory.NatTrans.congr_app` `commShiftIso_add'` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `map_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CommShift.commShiftIso_zero` `CommShift.isoZero_hom_app` `CommShift.isoAdd'_hom_app` `map_comp` `map_comp_assoc` `CategoryTheory.Iso.hom_inv_id_app` `map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id`
`map_shiftFunctorCompIsoId_hom_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `map` `CategoryTheory.NatTrans.app` `comp` `id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorCompIsoId` `CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_shiftFunctorCompIsoId_hom_app`
`map_shiftFunctorCompIsoId_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`map` `obj` `id` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CommShift.commShiftIso`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `map_isIso` `CategoryTheory.NatIso.hom_app_isIso` `map_comp` `CategoryTheory.Iso.hom_inv_id_app` `map_id` `map_shiftFunctorCompIsoId_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.Category.id_comp`
`map_shiftFunctorCompIsoId_inv_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.shiftFunctor` `map` `CategoryTheory.NatTrans.app` `id` `comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctorCompIsoId` `CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_shiftFunctorCompIsoId_inv_app`
`shiftFunctorIso_ofHasShiftOfFullyFaithful` 📖	mathematical	—	`CommShift.commShiftIso` `FullyFaithful.hasShift` `CommShift.ofHasShiftOfFullyFaithful`	—	—

CategoryTheory.Functor.CommShift

Definitions

Name	Category	Theorems
`commShiftIso` 📖	CompOp	157 math math: `zero`, `CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app_assoc`, `CategoryTheory.NatTrans.CommShiftCore.shift_app_comm`, `CategoryTheory.Functor.map_shiftFunctorComm_hom_app`, `CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app_assoc`, `CategoryTheory.Functor.mapTriangle_obj`, `CategoryTheory.Functor.commShiftOp_iso_eq`, `CategoryTheory.Functor.commShift₂_comm`, `CategoryTheory.LocalizerMorphism.commShift_iso_hom_app`, `CategoryTheory.Functor.commShiftIso_comp_hom_app`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app`, `CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁`, `CategoryTheory.Functor.commShiftIso_add'`, `CategoryTheory.NatTrans.CommShift.shift_comm`, `CategoryTheory.LocalizerMorphism.commShift_iso_inv_app`, `commShiftIso_add`, `CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq`, `CategoryTheory.Functor.shift_map_op_assoc`, `CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app_assoc`, `CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso`, `CategoryTheory.NatTrans.shift_comm_assoc`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop`, `CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app`, `ofIso_commShiftIso_hom_app`, `CategoryTheory.Quotient.LiftCommShift.iso_hom_app`, `CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app`, `CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app`, `comp_commShiftIso_inv_app`, `CategoryTheory.Triangulated.Octahedron.map_m₃`, `CategoryTheory.Adjunction.shift_counit_app`, `CategoryTheory.Functor.map_shift_unop`, `CategoryTheory.Adjunction.leftAdjointCommShift_commShiftIso`, `CategoryTheory.Functor.op_commShiftIso_hom_app_assoc`, `CategoryTheory.Functor.mapTriangle_map_hom₁`, `CategoryTheory.NatTrans.CommShiftCore.shift_app`, `CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj`, `CategoryTheory.NatTrans.shift_comm`, `CategoryTheory.LocalizerMorphism.commShift_iso_hom_app_assoc`, `CategoryTheory.Functor.commShiftPullback_iso_eq`, `add`, `CategoryTheory.Functor.ShiftSequence.induced.shiftIso_hom_app_obj`, `CategoryTheory.Functor.commShiftIso_hom_naturality_assoc`, `CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app`, `CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃`, `CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj_assoc`, `CategoryTheory.Localization.SmallShiftedHom.equiv_shift'`, `CategoryTheory.Functor.commShiftIso_comp_inv_app`, `CategoryTheory.LocalizerMorphism.commShift_iso_inv_app_assoc`, `CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app_assoc`, `CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃`, `CategoryTheory.Functor.map_shiftFunctorComm_assoc`, `CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app_assoc`, `CategoryTheory.Functor.commShiftIso_hom_naturality`, `comp_commShiftIso_hom_app`, `CategoryTheory.Functor.op_commShiftIso_inv_app_assoc`, `CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app`, `CategoryTheory.NatTrans.CommShiftCore.shift_app_assoc`, `CategoryTheory.Functor.CommShift₂.comm`, `CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app_assoc`, `id_commShiftIso_inv_app`, `CategoryTheory.Functor.commShiftIso_inv_naturality_assoc`, `CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app`, `CategoryTheory.Functor.mapTriangleInvRotateIso_inv_app_hom₁`, `CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃`, `CategoryTheory.NatTrans.CommShiftCore.shift_app_comm_assoc`, `CategoryTheory.Triangulated.Octahedron.map_m₁`, `CategoryTheory.NatTrans.CommShiftCore.shift_comm`, `CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app_assoc`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app`, `CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app_assoc`, `CategoryTheory.Functor.op_commShiftIso_inv_app`, `CategoryTheory.Functor.shiftFunctorIso_ofHasShiftOfFullyFaithful`, `CategoryTheory.NatTrans.CommShiftCore.shift_comm_assoc`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f`, `id_commShiftIso_hom_app`, `CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift_assoc`, `CategoryTheory.SingleFunctors.postcomp_shiftIso_inv_app`, `CategoryTheory.Localization.SmallShiftedHom.equiv_shift`, `CategoryTheory.Adjunction.shift_unit_app`, `CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app_assoc`, `CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app_assoc`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc`, `CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app`, `CategoryTheory.NatTrans.app_shift_assoc`, `CategoryTheory.Functor.commShiftIso_id_hom_app`, `ofIso_commShiftIso_inv_app`, `CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ`, `CategoryTheory.Functor.mapTriangle_map_hom₃`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc`, `CategoryTheory.Functor.shift_map_op`, `CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂`, `CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso`, `CategoryTheory.NatTrans.shift_app_assoc`, `CategoryTheory.NatTrans.CommShiftCore.app_shift`, `CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app`, `CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ'`, `CategoryTheory.Functor.commShiftIso_inv_naturality`, `HomotopyCategory.homologyFunctor_shiftMap_assoc`, `CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁`, `CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app_assoc`, `CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app_assoc`, `CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app`, `CategoryTheory.Functor.map_shift_unop_assoc`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f`, `CategoryTheory.Quotient.liftCommShift_commShiftIso`, `CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app_assoc`, `OfComp.map_iso_hom_app_assoc`, `CategoryTheory.Functor.commShiftIso_zero'`, `CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app`, `CategoryTheory.Functor.commShiftIso_id_inv_app`, `HomotopyCategory.homologyShiftIso_hom_app`, `CategoryTheory.Quotient.LiftCommShift.iso_inv_app`, `CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app`, `CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app`, `CategoryTheory.Functor.mapTriangleRotateIso_inv_app_hom₃`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop`, `CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app_assoc`, `CategoryTheory.NatTrans.app_shift`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc`, `CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂`, `CategoryTheory.NatTrans.shift_app_comm_assoc`, `CategoryTheory.NatTrans.shift_app`, `CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app`, `CategoryTheory.Functor.ShiftSequence.induced_shiftMap`, `CategoryTheory.Functor.commShiftIso_eq_ofInduced`, `CategoryTheory.Functor.map_shiftFunctorComm`, `CategoryTheory.Functor.op_commShiftIso_hom_app`, `HomotopyCategory.homologyFunctor_shiftMap`, `CategoryTheory.Localization.SmallHom.equiv_shift`, `CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁`, `CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app`, `CategoryTheory.NatTrans.shift_app_comm`, `CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc`, `CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc`, `OfComp.map_iso_inv_app`, `CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app`, `CategoryTheory.Localization.SmallShiftedHom.equiv_apply`, `CategoryTheory.Functor.commShift₂_comm_assoc`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app`, `CategoryTheory.Adjunction.rightAdjointCommShift_commShiftIso`, `CategoryTheory.Adjunction.shift_unit_app_assoc`, `CategoryTheory.Functor.commShiftUnop_commShiftIso`, `CategoryTheory.Functor.ShiftSequence.induced_shiftMap_assoc`, `CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift`, `CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop`, `CategoryTheory.NatTrans.CommShiftCore.app_shift_assoc`, `CategoryTheory.SingleFunctors.postcomp_shiftIso_hom_app`, `commShiftIso_zero`, `OfComp.map_iso_hom_app`, `OfComp.map_iso_inv_app_assoc`, `CategoryTheory.Functor.mapTriangle_map_hom₂`, `CategoryTheory.Adjunction.shift_counit_app_assoc`, `CochainComplex.mappingCone.map_δ`
`comp` 📖	CompOp	46 math math: `CategoryTheory.SingleFunctors.postcompPostcompIso_hom_hom_app`, `CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso`, `CategoryTheory.LocalizerMorphism.natTransCommShift_hom`, `CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₂`, `DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso`, `CategoryTheory.NatTrans.CommShift.leftUnitor`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp`, `CategoryTheory.Functor.commShiftIso_comp_hom_app`, `CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₂`, `CategoryTheory.NatTrans.CommShift.verticalComposition`, `CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh`, `CategoryTheory.NatTrans.CommShift.whiskerRight`, `CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app`, `CategoryTheory.NatTrans.CommShift.associator`, `CategoryTheory.Quotient.liftCommShift_compatibility`, `CategoryTheory.NatTrans.CommShift.rightUnitor`, `comp_commShiftIso_inv_app`, `CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃`, `CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₃`, `ofComp_compatibility`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso`, `CategoryTheory.Adjunction.CommShift.commShift_counit`, `CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors`, `CategoryTheory.Functor.commShiftIso_comp_inv_app`, `comp_commShiftIso_hom_app`, `CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app_assoc`, `CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app_assoc`, `CategoryTheory.ShiftedHom.comp_map`, `CategoryTheory.Adjunction.IsTriangulated.comp`, `CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift_assoc`, `CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app_assoc`, `CategoryTheory.Adjunction.CommShift.instComp`, `CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₁`, `CategoryTheory.SingleFunctors.postcompPostcompIso_inv_hom_app`, `CategoryTheory.Functor.mapTriangleCompIso_hom_app_hom₁`, `CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app`, `CategoryTheory.Adjunction.CommShift.commShift_unit`, `CategoryTheory.NatTrans.commShift_iso_hom_of_localization`, `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`, `CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app`, `CategoryTheory.NatTrans.CommShift.whiskerLeft`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`, `CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso`, `CategoryTheory.Functor.IsTriangulated.instComp`, `HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors`
`id` 📖	CompOp	23 math math: `CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₃`, `CategoryTheory.NatTrans.CommShift.leftUnitor`, `CategoryTheory.Adjunction.IsTriangulated.id`, `CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId`, `CategoryTheory.Adjunction.CommShift.instId`, `CategoryTheory.NatTrans.CommShift.rightUnitor`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso`, `CategoryTheory.Adjunction.CommShift.commShift_counit`, `id_commShiftIso_inv_app`, `CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₃`, `id_commShiftIso_hom_app`, `CategoryTheory.Functor.commShiftIso_id_hom_app`, `CategoryTheory.Functor.IsTriangulated.instId`, `CategoryTheory.Functor.commShiftIso_id_inv_app`, `CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁`, `CategoryTheory.ShiftedHom.id_map`, `CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₂`, `CategoryTheory.Adjunction.CommShift.commShift_unit`, `CategoryTheory.TwistShiftData.commShift`, `CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁`, `CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₂`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso`
`iso` 📖	CompOp	—
`isoAdd` 📖	CompOp	5 math math: `isoAdd_hom_app`, `isoAdd_inv_app`, `commShiftIso_add`, `add`, `CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd`
`isoAdd'` 📖	CompOp	6 math math: `CategoryTheory.Functor.commShiftIso_add'`, `isoAdd'_assoc`, `isoAdd'_isoZero`, `isoAdd'_hom_app`, `isoZero_isoAdd'_`, `isoAdd'_inv_app`
`isoZero` 📖	CompOp	8 math math: `zero`, `isoZero_hom_app`, `isoAdd'_isoZero`, `isoZero_inv_app`, `isoZero'_eq_isoZero`, `isoZero_isoAdd'_`, `commShiftIso_zero`, `CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoZero`
`isoZero'` 📖	CompOp	4 math math: `isoZero'_inv_app`, `isoZero'_eq_isoZero`, `CategoryTheory.Functor.commShiftIso_zero'`, `isoZero'_hom_app`
`ofComp` 📖	CompOp	1 math math: `ofComp_compatibility`
`ofHasShiftOfFullyFaithful` 📖	CompOp	1 math math: `CategoryTheory.Functor.shiftFunctorIso_ofHasShiftOfFullyFaithful`
`ofIso` 📖	CompOp	3 math math: `ofIso_commShiftIso_hom_app`, `ofIso_commShiftIso_inv_app`, `ofIso_compatibility`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	—	`commShiftIso` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `isoAdd`	—	`commShiftIso_add`
`commShiftIso_add` 📖	mathematical	—	`commShiftIso` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `isoAdd`	—	—
`commShiftIso_zero` 📖	mathematical	—	`commShiftIso` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `isoZero`	—	—
`comp_commShiftIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`comp_commShiftIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`id_commShiftIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Category.comp_id`
`id_commShiftIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Category.comp_id`
`isoAdd'_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`isoAdd'`	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.naturality_2` `isoAdd'_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.shiftFunctorAdd'_assoc_hom_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.shiftFunctorAdd'_assoc_inv_app`
`isoAdd'_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoAdd'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.shiftFunctorAdd'` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.id_comp`
`isoAdd'_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoAdd'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.hom` `CategoryTheory.shiftFunctorAdd'` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`
`isoAdd'_isoZero` 📖	mathematical	—	`isoAdd'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `add_zero` `isoZero`	—	`CategoryTheory.Iso.ext` `add_zero` `CategoryTheory.NatTrans.ext'` `isoAdd'_hom_app` `CategoryTheory.shiftFunctorAdd'_add_zero_hom_app` `isoZero_hom_app` `CategoryTheory.shiftFunctorAdd'_add_zero_inv_app` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`isoAdd_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoAdd` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.shiftFunctorAdd` `CategoryTheory.Iso.inv`	—	`isoAdd'_hom_app` `CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd`
`isoAdd_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoAdd` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.hom` `CategoryTheory.shiftFunctorAdd` `CategoryTheory.Functor.map`	—	`isoAdd'_inv_app` `CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd`
`isoZero'_eq_isoZero` 📖	mathematical	—	`isoZero'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `isoZero`	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Iso.refl_trans` `CategoryTheory.Category.id_comp` `isoZero_hom_app`
`isoZero'_hom_app` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoZero'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctorZero'` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.id_comp`
`isoZero'_inv_app` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoZero'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.shiftFunctorZero'` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id`
`isoZero_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoZero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctorZero` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.id_comp`
`isoZero_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoZero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.shiftFunctorZero` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id`
`isoZero_isoAdd'_` 📖	mathematical	—	`isoAdd'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `zero_add` `isoZero`	—	`CategoryTheory.Iso.ext` `zero_add` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.naturality` `isoAdd'_hom_app` `CategoryTheory.shiftFunctorAdd'_zero_add_hom_app` `isoZero_hom_app` `CategoryTheory.shiftFunctorAdd'_zero_add_inv_app` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Functor.map_id`
`ofComp_compatibility` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `comp` `ofComp`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `OfComp.map_iso_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_id`
`ofIso_commShiftIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `ofIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.map`	—	—
`ofIso_commShiftIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `commShiftIso` `ofIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc`
`ofIso_compatibility` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ofIso`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`zero` 📖	mathematical	—	`commShiftIso` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `isoZero`	—	`commShiftIso_zero`

CategoryTheory.Functor.CommShift.OfComp

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	4 math math: `map_iso_hom_app_assoc`, `map_iso_inv_app`, `map_iso_hom_app`, `map_iso_inv_app_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_iso_hom_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.map_preimage` `CategoryTheory.Functor.full_whiskeringRight_obj` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.congr_app`
`map_iso_hom_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_iso_hom_app`
`map_iso_inv_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Functor.map_preimage` `CategoryTheory.Functor.full_whiskeringRight_obj` `CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.congr_app`
`map_iso_inv_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_iso_inv_app`

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`CommShift` 📖	CompData	41 math math: `CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso`, `CategoryTheory.LocalizerMorphism.natTransCommShift_hom`, `DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso`, `CommShift.leftUnitor`, `instCommShiftPullbackShiftHomFunctorNatIsoComp`, `CommShift.verticalComposition`, `instCommShiftPullbackShiftHomFunctorNatIsoId`, `CategoryTheory.Functor.CommShift₂.commShift_flip_map`, `CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh`, `CommShift₂.commShift_flipApp`, `commShiftPullback`, `CommShift.whiskerRight`, `CommShift.associator`, `CategoryTheory.Functor.CommShift₂.commShift_map`, `CategoryTheory.Quotient.liftCommShift_compatibility`, `CommShift.of_isIso`, `CommShift.rightUnitor`, `instCommShiftOppositeShiftHomFunctorNatIsoId`, `CommShift.comp`, `commShift_op`, `CategoryTheory.Functor.CommShift.ofComp_compatibility`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso`, `CategoryTheory.Adjunction.CommShift.commShift_counit`, `CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors`, `CategoryTheory.Pretriangulated.Opposite.commShift_natTrans_op_int`, `CommShift.of_iso_symm`, `CategoryTheory.Functor.CommShift.ofIso_compatibility`, `CategoryTheory.Adjunction.CommShift.commShift_unit`, `commShift_iso_hom_of_localization`, `CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor`, `CategoryTheory.TwistShiftData.commShift`, `CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex`, `CommShift.whiskerLeft`, `instCommShiftOppositeShiftHomFunctorNatIsoComp`, `CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex`, `CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso`, `CommShift.id`, `CommShift.of_core`, `CommShift.of_iso_inv`, `CommShift₂.commShift_app`, `HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors`
`CommShiftCore` 📖	CompData	1 math math: `CommShiftCore.zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_shift` 📖	mathematical	—	`app` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`shift_app_comm_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id`
`app_shift_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `app_shift`
`shift_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.obj` `app` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.hom`	—	`shift_app_comm` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`shift_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_app`
`shift_app_comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map`	—	`congr_app` `shift_comm`
`shift_app_comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_app_comm`
`shift_comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.whiskerLeft`	—	`CommShift.shift_comm`
`shift_comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_comm`

CategoryTheory.NatTrans.CommShift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`comp` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Functor.whiskerRight_comp` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.shift_app_comm_assoc` `CategoryTheory.NatTrans.shift_app_comm`
`id` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Functor.whiskerRight_id'` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`leftUnitor` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.leftUnitor` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.CommShift.id`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`of_core` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.NatTrans.CommShift`	—	`CategoryTheory.NatTrans.CommShiftCore.shift_comm`
`of_isIso` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`of_iso_inv`
`of_iso_inv` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.NatTrans.shift_app_comm_assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`of_iso_symm` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Iso.symm`	—	`of_iso_inv`
`rightUnitor` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.rightUnitor` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.CommShift.id`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`shift_comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.whiskerLeft`	—	—
`verticalComposition` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Iso.inv`	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.CommShift.comp`	—	`comp` `whiskerRight` `associator` `whiskerLeft` `of_iso_inv`
`whiskerLeft` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.Functor.whiskerLeft_twice` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.NatTrans.shift_app_comm` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.id_comp`
`whiskerRight` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.whiskerRight_twice` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.NatTrans.shift_app_comm`

CategoryTheory.NatTrans.CommShiftCore

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.CommShift.commShiftIso_add` `CategoryTheory.Functor.CommShift.isoAdd_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_2` `app_shift_assoc` `app_shift` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`app_shift` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`shift_app_comm_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id`
`app_shift_assoc` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `app_shift`
`shift_app` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.Functor.map` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.hom`	—	`shift_app_comm` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`shift_app_assoc` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_app`
`shift_app_comm` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.NatTrans.congr_app` `shift_comm`
`shift_app_comm_assoc` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_app_comm`
`shift_comm` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.whiskerLeft`	—	—
`shift_comm_assoc` 📖	mathematical	`CategoryTheory.NatTrans.CommShiftCore`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Functor.whiskerLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_comm`
`zero` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShiftCore` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.CommShift.commShiftIso_zero` `CategoryTheory.Functor.CommShift.isoZero_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality_assoc`

---

← Back to Index