Adjunction

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

Statistics

Metric	Count
Definitions Adjunction, IsTriangulated, IsTriangulated	3
Theorems commShift, comp, id, leftAdjoint_isTriangulated, mk', mk'', rightAdjoint_isTriangulated, isTriangulated_leftAdjoint, isTriangulated_rightAdjoint, instIsTriangulatedFunctor, instIsTriangulatedFunctorSymmOfInverse, instIsTriangulatedInverse, instIsTriangulatedInverseSymmOfFunctor, mk', mk'', refl, trans	17
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
Adjunction 📖	CompData	2 math math: Functor.IsLeftAdjoint.exists_rightAdjoint, Functor.IsRightAdjoint.exists_leftAdjoint

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
IsTriangulated 📖	CompData	4 math math: IsTriangulated.id, IsTriangulated.mk'', IsTriangulated.comp, IsTriangulated.mk'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTriangulated_leftAdjoint 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated	—	CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt isTriangulated_rightAdjoint CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op CategoryTheory.Functor.isTriangulated_of_op
isTriangulated_rightAdjoint 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated	—	right_adjoint_additive CategoryTheory.Functor.IsTriangulated.instAdditive CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism CategoryTheory.Functor.map_distinguished counit_naturality CategoryTheory.Functor.map_comp unit_naturality_assoc right_triangle_components_assoc DFunLike.congr_arg Equiv.injective homEquiv_counit CategoryTheory.Category.assoc homEquiv_unit counit_naturality_assoc shift_counit_app CategoryTheory.Iso.hom_inv_id_app_assoc left_triangle_components_assoc CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃ CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.zero_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.comp_zero CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ right_triangle_components CategoryTheory.Category.comp_id CategoryTheory.isIso_of_yoneda_map_bijective CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₁ CategoryTheory.Functor.commShiftIso_hom_naturality CategoryTheory.Functor.map_comp_assoc CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁ CategoryTheory.Preadditive.sub_comp CategoryTheory.Iso.isIso_hom sub_eq_zero CategoryTheory.Iso.hom_inv_id_app Equiv.apply_symm_apply CategoryTheory.Preadditive.add_comp add_sub_cancel CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id shift_unit_app_assoc

CategoryTheory.Adjunction.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commShift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Adjunction.CommShift	—	—
comp 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Adjunction.IsTriangulated CategoryTheory.Functor.comp CategoryTheory.Adjunction.comp CategoryTheory.Functor.CommShift.comp	—	CategoryTheory.Adjunction.CommShift.instComp CategoryTheory.Functor.IsTriangulated.instComp leftAdjoint_isTriangulated rightAdjoint_isTriangulated
id 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Adjunction.IsTriangulated CategoryTheory.Functor.id CategoryTheory.Adjunction.id CategoryTheory.Functor.CommShift.id	—	CategoryTheory.Adjunction.CommShift.instId CategoryTheory.Functor.IsTriangulated.instId
leftAdjoint_isTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Adjunction.IsTriangulated	—	CategoryTheory.Adjunction.isTriangulated_rightAdjoint
mk'' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Adjunction.IsTriangulated	—	CategoryTheory.Adjunction.isTriangulated_leftAdjoint
rightAdjoint_isTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
IsTriangulated 📖	MathDef	6 math math: CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence, IsTriangulated.trans, IsTriangulated.mk', IsTriangulated.symm, IsTriangulated.refl, IsTriangulated.mk''

CategoryTheory.Equivalence.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTriangulatedFunctor 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Equivalence.functor	—	CategoryTheory.Adjunction.IsTriangulated.leftAdjoint_isTriangulated
instIsTriangulatedFunctorSymmOfInverse 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.CommShift.instCommShiftFunctorSymm	—	—
instIsTriangulatedInverse 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Equivalence.inverse	—	CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated
instIsTriangulatedInverseSymmOfFunctor 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm CategoryTheory.Equivalence.CommShift.instCommShiftInverseSymm	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.IsTriangulated	—	CategoryTheory.Adjunction.isTriangulated_rightAdjoint
mk'' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.IsTriangulated	—	CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated mk' CategoryTheory.Equivalence.CommShift.instSymm
refl 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.IsTriangulated CategoryTheory.Equivalence.refl CategoryTheory.Equivalence.CommShift.instCommShiftFunctorRefl CategoryTheory.Equivalence.CommShift.instCommShiftInverseRefl	—	CategoryTheory.Equivalence.refl_toAdjunction CategoryTheory.Adjunction.IsTriangulated.id
trans 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.IsTriangulated CategoryTheory.Equivalence.trans CategoryTheory.Equivalence.CommShift.instCommShiftFunctorTrans CategoryTheory.Equivalence.CommShift.instCommShiftInverseTrans	—	CategoryTheory.Equivalence.trans_toAdjunction CategoryTheory.Adjunction.IsTriangulated.comp

---

← Back to Index