Documentation Verification Report

Adjunction

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

Statistics

Metric	Count
Definitions `CompatibilityCounit`, `CompatibilityUnit`, `iso`, `iso'`, `iso`, `iso'`, `leftAdjointCommShift`, `rightAdjointCommShift`, `instCommShiftFunctorRefl`, `instCommShiftFunctorSymm`, `instCommShiftFunctorTrans`, `instCommShiftInverseRefl`, `instCommShiftInverseSymm`, `instCommShiftInverseTrans`, `commShiftFunctor`, `commShiftInverse`	16
Theorems `commShift_counit`, `commShift_unit`, `compatibilityCounit_left`, `compatibilityCounit_of_compatibilityUnit`, `compatibilityUnit_isoAdd`, `compatibilityUnit_isoZero`, `compatibilityUnit_right`, `compatibilityUnit_unique_left`, `compatibilityUnit_unique_right`, `instComp`, `instId`, `mk'`, `compatibilityUnit_iso`, `iso_hom_app`, `iso_hom_app_assoc`, `iso_inv_app`, `iso_inv_app_assoc`, `compatibilityUnit_iso`, `iso_hom_app`, `iso_hom_app_assoc`, `iso_inv_app`, `iso_inv_app_assoc`, `commShiftIso_hom_app_counit_app_shift`, `commShiftIso_hom_app_counit_app_shift_assoc`, `commShiftIso_inv_app_counit_app`, `commShiftIso_inv_app_counit_app_assoc`, `commShift_of_leftAdjoint`, `commShift_of_rightAdjoint`, `leftAdjointCommShift_commShiftIso`, `rightAdjointCommShift_commShiftIso`, `shift_counit_app`, `shift_counit_app_assoc`, `shift_unit_app`, `shift_unit_app_assoc`, `unit_app_commShiftIso_hom_app`, `unit_app_commShiftIso_hom_app_assoc`, `unit_app_shift_commShiftIso_inv_app`, `unit_app_shift_commShiftIso_inv_app_assoc`, `instCommShiftHomFunctorCounitIso`, `instCommShiftHomFunctorUnitIso`, `instRefl`, `instSymm`, `instTrans`, `mk'`, `mk''`, `commShift_of_functor`, `commShift_of_inverse`	47
Total	63

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`leftAdjointCommShift` 📖	CompOp	2 math math: `leftAdjointCommShift_commShiftIso`, `commShift_of_rightAdjoint`
`rightAdjointCommShift` 📖	CompOp	2 math math: `commShift_of_leftAdjoint`, `rightAdjointCommShift_commShiftIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftIso_hom_app_counit_app_shift` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.map` `counit`	—	`CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.shift_app_comm` `CommShift.commShift_counit`
`commShiftIso_hom_app_counit_app_shift_assoc` 📖	mathematical	—	`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.CommShift.comp` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShiftIso_hom_app_counit_app_shift`
`commShiftIso_inv_app_counit_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp` `counit` `CategoryTheory.Functor.map`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Iso.hom_inv_id_app_assoc` `commShiftIso_hom_app_counit_app_shift`
`commShiftIso_inv_app_counit_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.id` `counit` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShiftIso_inv_app_counit_app`
`commShift_of_leftAdjoint` 📖	mathematical	—	`CommShift` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `rightAdjointCommShift`	—	`CommShift.mk'` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `RightAdjointCommShift.compatibilityUnit_iso`
`commShift_of_rightAdjoint` 📖	mathematical	—	`CommShift` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `leftAdjointCommShift`	—	`CommShift.mk'` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `LeftAdjointCommShift.compatibilityUnit_iso`
`leftAdjointCommShift_commShiftIso` 📖	mathematical	—	`CategoryTheory.Functor.CommShift.commShiftIso` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `leftAdjointCommShift` `LeftAdjointCommShift.iso`	—	—
`rightAdjointCommShift_commShiftIso` 📖	mathematical	—	`CategoryTheory.Functor.CommShift.commShiftIso` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `rightAdjointCommShift` `RightAdjointCommShift.iso`	—	—
`shift_counit_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.NatTrans.shift_app_comm` `CommShift.commShift_counit` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.comp_id` `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`
`shift_counit_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `counit` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_counit_app`
`shift_unit_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.NatTrans.shift_app_comm` `CommShift.commShift_unit`
`shift_unit_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_unit_app`
`unit_app_commShiftIso_hom_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.shift_app_comm` `CommShift.commShift_unit`
`unit_app_commShiftIso_hom_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit_app_commShiftIso_hom_app`
`unit_app_shift_commShiftIso_inv_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id` `unit_app_commShiftIso_hom_app`
`unit_app_shift_commShiftIso_inv_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit_app_shift_commShiftIso_inv_app`

CategoryTheory.Adjunction.CommShift

Definitions

Name	Category	Theorems
`CompatibilityCounit` 📖	MathDef	1 math math: `compatibilityCounit_of_compatibilityUnit`
`CompatibilityUnit` 📖	MathDef	3 math math: `CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso`, `CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso`, `compatibilityUnit_isoZero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_counit` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.CommShift.id`	—	—
`commShift_unit` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.CommShift.id` `CategoryTheory.Functor.CommShift.comp`	—	—
`compatibilityCounit_left` 📖	mathematical	`CompatibilityCounit`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.unit` `CategoryTheory.Iso.inv` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Functor.comp_map` `CategoryTheory.Adjunction.left_triangle_components` `CategoryTheory.Category.comp_id`
`compatibilityCounit_of_compatibilityUnit` 📖	mathematical	`CompatibilityUnit`	`CompatibilityCounit`	—	`Equiv.injective` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.cancel_mono` `CategoryTheory.mono_comp` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Adjunction.right_triangle_components` `CategoryTheory.Category.id_comp`
`compatibilityUnit_isoAdd` 📖	mathematical	`CompatibilityUnit`	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `CategoryTheory.Functor.CommShift.isoAdd`	—	`CategoryTheory.Functor.CommShift.isoAdd_hom_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality_assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.NatTrans.naturality`
`compatibilityUnit_isoZero` 📖	mathematical	—	`CompatibilityUnit` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Functor.CommShift.isoZero`	—	`CategoryTheory.Functor.CommShift.isoZero_hom_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Category.comp_id`
`compatibilityUnit_right` 📖	mathematical	`CompatibilityUnit`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.NatTrans.naturality` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.right_triangle_components` `CategoryTheory.Functor.map_id`
`compatibilityUnit_unique_left` 📖	—	`CompatibilityUnit`	—	—	`CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `compatibilityCounit_left` `compatibilityCounit_of_compatibilityUnit`
`compatibilityUnit_unique_right` 📖	—	`CompatibilityUnit`	—	—	`CategoryTheory.Iso.symm_eq_iff` `CategoryTheory.Iso.ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Iso.symm_hom` `compatibilityUnit_right`
`instComp` 📖	mathematical	—	`CategoryTheory.Adjunction.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Adjunction.comp` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.Adjunction.comp_unit` `CategoryTheory.NatTrans.CommShift.comp` `commShift_unit` `CategoryTheory.NatTrans.CommShift.whiskerRight` `CategoryTheory.NatTrans.CommShift.of_iso_inv` `CategoryTheory.NatTrans.CommShift.rightUnitor` `CategoryTheory.NatTrans.CommShift.whiskerLeft` `CategoryTheory.NatTrans.CommShift.associator` `CategoryTheory.Adjunction.comp_counit` `commShift_counit`
`instId` 📖	mathematical	—	`CategoryTheory.Adjunction.CommShift` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.id` `CategoryTheory.Functor.CommShift.id`	—	`CategoryTheory.NatTrans.CommShift.of_iso_inv` `CategoryTheory.NatTrans.CommShift.leftUnitor`
`mk'` 📖	mathematical	—	`CategoryTheory.Adjunction.CommShift`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Functor.commShiftIso_comp_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.comp_id` `compatibilityCounit_of_compatibilityUnit` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.shift_app_comm`

CategoryTheory.Adjunction.LeftAdjointCommShift

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	6 math math: `iso_hom_app_assoc`, `iso_inv_app_assoc`, `compatibilityUnit_iso`, `CategoryTheory.Adjunction.leftAdjointCommShift_commShiftIso`, `iso_inv_app`, `iso_hom_app`
`iso'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatibilityUnit_iso` 📖	mathematical	—	`CategoryTheory.Adjunction.CommShift.CompatibilityUnit` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `iso` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`add_neg_cancel` `iso_hom_app` `CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.Adjunction.right_triangle_components_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.shift_shiftFunctorCompIsoId_inv_app` `CategoryTheory.Functor.comp_map` `neg_add_cancel` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.comp_id`
`iso_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.unit` `CategoryTheory.Iso.inv` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`add_neg_cancel` `CategoryTheory.conjugateEquiv_symm_apply_app` `CategoryTheory.Adjunction.comp_unit_app` `CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.comp_counit_app` `CategoryTheory.Category.assoc` `Mathlib.Tactic.CategoryTheory.CancelIso.hom_inv_id_of_eq_assoc` `CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsIso.Iso.inv_inv` `eq_neg_of_add_eq_zero_right`
`iso_hom_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`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` `iso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `CategoryTheory.Iso.inv` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_app`
`iso_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit` `CategoryTheory.Iso.hom`	—	`add_neg_cancel` `CategoryTheory.conjugateEquiv_symm_apply_app` `CategoryTheory.Adjunction.comp_unit_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.comp_counit_app` `CategoryTheory.Category.assoc` `eq_neg_of_add_eq_zero_right`
`iso_inv_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.map` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_app`

CategoryTheory.Adjunction.RightAdjointCommShift

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	6 math math: `iso_hom_app_assoc`, `compatibilityUnit_iso`, `iso_inv_app`, `iso_inv_app_assoc`, `iso_hom_app`, `CategoryTheory.Adjunction.rightAdjointCommShift_commShiftIso`
`iso'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatibilityUnit_iso` 📖	mathematical	—	`CategoryTheory.Adjunction.CommShift.CompatibilityUnit` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `CategoryTheory.Functor.CommShift.commShiftIso` `iso`	—	`CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_app` `neg_add_cancel` `iso_inv_app` `Equiv.injective` `CategoryTheory.Adjunction.homEquiv_counit` `CategoryTheory.Functor.map_comp` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.counit_naturality_assoc` `CategoryTheory.Adjunction.left_triangle_components_assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.shift_shiftFunctorCompIsoId_hom_app` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Functor.commShiftIso_hom_naturality_assoc` `CategoryTheory.Adjunction.left_triangle_components` `CategoryTheory.Functor.map_id`
`iso_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`neg_add_cancel` `CategoryTheory.conjugateEquiv_apply_app` `CategoryTheory.Adjunction.comp_unit_app` `CategoryTheory.Adjunction.comp_counit_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `AddRightCancelSemigroup.toIsRightCancelAdd`
`iso_hom_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`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` `iso` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Functor.map` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_app`
`iso_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.map` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`neg_add_cancel` `CategoryTheory.conjugateEquiv_apply_app` `CategoryTheory.Adjunction.comp_unit_app` `CategoryTheory.Adjunction.comp_counit_app` `CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `AddRightCancelSemigroup.toIsRightCancelAdd`
`iso_inv_app_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `iso` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.unit` `CategoryTheory.Functor.map` `CategoryTheory.shiftFunctorCompIsoId` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Adjunction.counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_app`

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`commShiftFunctor` 📖	CompOp	1 math math: `commShift_of_inverse`
`commShiftInverse` 📖	CompOp	1 math math: `commShift_of_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_of_functor` 📖	mathematical	—	`CommShift` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `commShiftInverse`	—	`CommShift.mk'` `CategoryTheory.Adjunction.CommShift.commShift_unit` `CategoryTheory.Adjunction.commShift_of_leftAdjoint`
`commShift_of_inverse` 📖	mathematical	—	`CommShift` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `commShiftFunctor`	—	`commShift_of_functor` `CommShift.instSymm`

CategoryTheory.Equivalence.CommShift

Definitions

Name	Category	Theorems
`instCommShiftFunctorRefl` 📖	CompOp	2 math math: `instRefl`, `CategoryTheory.Equivalence.IsTriangulated.refl`
`instCommShiftFunctorSymm` 📖	CompOp	3 math math: `CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse`, `CategoryTheory.Equivalence.IsTriangulated.symm`, `instSymm`
`instCommShiftFunctorTrans` 📖	CompOp	2 math math: `instTrans`, `CategoryTheory.Equivalence.IsTriangulated.trans`
`instCommShiftInverseRefl` 📖	CompOp	2 math math: `instRefl`, `CategoryTheory.Equivalence.IsTriangulated.refl`
`instCommShiftInverseSymm` 📖	CompOp	3 math math: `CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor`, `CategoryTheory.Equivalence.IsTriangulated.symm`, `instSymm`
`instCommShiftInverseTrans` 📖	CompOp	2 math math: `instTrans`, `CategoryTheory.Equivalence.IsTriangulated.trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCommShiftHomFunctorCounitIso` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.functor` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `CategoryTheory.Functor.CommShift.comp` `CategoryTheory.Functor.CommShift.id`	—	`CategoryTheory.Adjunction.CommShift.commShift_counit`
`instCommShiftHomFunctorUnitIso` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.Functor.CommShift.id` `CategoryTheory.Functor.CommShift.comp`	—	`CategoryTheory.Adjunction.CommShift.commShift_unit`
`instRefl` 📖	mathematical	—	`CategoryTheory.Equivalence.CommShift` `CategoryTheory.Equivalence.refl` `instCommShiftFunctorRefl` `instCommShiftInverseRefl`	—	`CategoryTheory.Adjunction.CommShift.instId`
`instSymm` 📖	mathematical	—	`CategoryTheory.Equivalence.CommShift` `CategoryTheory.Equivalence.symm` `instCommShiftFunctorSymm` `instCommShiftInverseSymm`	—	`mk'` `CategoryTheory.NatTrans.CommShift.of_iso_inv` `instCommShiftHomFunctorCounitIso`
`instTrans` 📖	mathematical	—	`CategoryTheory.Equivalence.CommShift` `CategoryTheory.Equivalence.trans` `instCommShiftFunctorTrans` `instCommShiftInverseTrans`	—	`CategoryTheory.Adjunction.CommShift.instComp`
`mk'` 📖	mathematical	—	`CategoryTheory.Equivalence.CommShift`	—	`CategoryTheory.Adjunction.CommShift.commShift_counit` `CategoryTheory.Adjunction.CommShift.mk'`
`mk''` 📖	mathematical	—	`CategoryTheory.Equivalence.CommShift`	—	`mk'` `CategoryTheory.NatTrans.CommShift.of_iso_inv` `instSymm`

---

← Back to Index