Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adj.left_triangle_components

∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₁.obj),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.adj.unit.toNatTrans.app X))
      (α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.id (α.l.toFunctor.obj X)

Defined in: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Cited by: 1 results in Mathlib
Foundations: Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
CategoryTheory.CategoryStruct.compstatement · cited by 17,999
CategoryTheory.Functor.mapstatement · cited by 8,698
CategoryTheory.NatTrans.appstatement · cited by 7,406
CategoryTheory.CategoryStruct.idstatement and proof · cited by 6,235
CategoryTheory.Catstatement and proof · cited by 884
CategoryTheory.Bundled.αstatement and proof · cited by 736
CategoryTheory.Cat.Hom.toFunctorstatement and proof · cited by 531
CategoryTheory.Cat.Hom₂.toNatTransstatement · cited by 277
CategoryTheory.Bicategory.Adjstatement and proof · cited by 131

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Bicategory.Adj.left_triangle_components_assocproof · cited by 0