Structures · Category theory
CategoryTheory.Adjunction.CommShift
The property for CommShift structures on F and G to be compatible with an
adjunction F ⊣ G.
- Defined in
- Mathlib.CategoryTheory.Shift.Adjunction
- Shape
- 2 explicit arguments · adds commShift_unit, commShift_counit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.OppositeShift
- CategoryTheory.PullbackShift
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- CategoryTheory.Adjunction.isTriangulated_rightAdjoint
- CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift
- CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app
- CategoryTheory.Adjunction.shift_counit_app
- CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app
- CategoryTheory.Adjunction.shift_unit_app_assoc
- CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app
- CategoryTheory.Adjunction.isTriangulated_leftAdjoint
- CategoryTheory.Adjunction.shift_unit_app
- CategoryTheory.Adjunction.IsTriangulated.mk''
- CategoryTheory.Adjunction.CommShift.instComp
- CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app_assoc
- CategoryTheory.Adjunction.IsTriangulated.comp
- CategoryTheory.Adjunction.commShiftIso_hom_app_counit_app_shift_assoc
- CategoryTheory.Adjunction.unit_app_commShiftIso_hom_app_assoc
- CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int
- CategoryTheory.Adjunction.shift_counit_app_assoc
- CategoryTheory.Adjunction.commShift_op
- CategoryTheory.Adjunction.commShiftPullback
- CategoryTheory.Adjunction.CommShift.commShift_counit
- CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app_assoc
- CategoryTheory.Adjunction.CommShift.commShift_unit
- CategoryTheory.Adjunction.IsTriangulated.mk'
Ancestors0
No ancestors.