Theorems · Definition · category theory
CategoryTheory.Adjunction.ofIsLeftAdjoint
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{D : Type u₂} →
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
(left : CategoryTheory.Functor C D) → [inst_2 : left.IsLeftAdjoint] → left ⊣ left.rightAdjointThe adjunction associated to a functor known to be a left adjoint.
- Defined in
- Mathlib.CategoryTheory.Adjunction.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Adjunctionstatement · cited by 524
- Nonempty.someproof · cited by 340
- CategoryTheory.Functor.IsLeftAdjointstatement and proof · cited by 28
- CategoryTheory.Functor.rightAdjointstatement · cited by 5
Cited by11
Results whose statement or proof uses this declaration.
- CategoryTheory.constantSheafΓAdjproof · cited by 6
- CategoryTheory.Functor.isLeftAdjoint_of_isoproof · cited by 2
- CategoryTheory.isLeftAdjoint_triangle_liftproof · cited by 1
- CategoryTheory.isLeftAdjoint_triangle_lift_comonadicproof · cited by 1
- CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrowproof · cited by 1
- CategoryTheory.isLeftAdjoint_square_liftstatement and proof · cited by 0
- CategoryTheory.isLeftAdjoint_square_lift_comonadicproof · cited by 0
- CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjointproof · cited by 0
- CategoryTheory.Functor.functorCategoryClosedproof · cited by 0
- CategoryTheory.Functor.isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_topproof · cited by 0
- CategoryTheory.IsCofiltered.of_isLeftAdjointproof · cited by 0