Loogle!

Result

Found 21556 declarations mentioning CategoryTheory.Functor.obj. Of these, 2586 have a name containing "_obj". Of these, only the first 200 are shown.

CategoryTheory.Functor.id_obj 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.id C).obj X = X
CategoryTheory.Functor.toPrefunctor_obj 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a✝ : C) : F.toPrefunctor.obj a✝ = F.obj a✝
CategoryTheory.Functor.comp_obj 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : C) : (F.comp G).obj X = G.obj (F.obj X)
CategoryTheory.Functor.flip_obj_obj 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C) : (F.flip.obj k).obj j = (F.obj j).obj k
CategoryTheory.flipFunctor_obj 📋 Mathlib.CategoryTheory.Functor.Category
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) : (CategoryTheory.flipFunctor C D E).obj F = F.flip
CategoryTheory.Functor.flip_obj_map 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.flip.obj k).map f = (F.map f).app k
CategoryTheory.Functor.copyObj_obj 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (a✝ : C) : (F.copyObj obj e).obj a✝ = obj a✝
CategoryTheory.inducedFunctor_obj 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) (a✝ : C) : (CategoryTheory.inducedFunctor F).obj a✝ = F a✝
CategoryTheory.ObjectProperty.prop_map_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
{C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.map F (F.obj X)
CategoryTheory.ObjectProperty.strictMap_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
{C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.strictMap F (F.obj X)
CategoryTheory.ObjectProperty.prop_ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : P (P.ι.obj X)
CategoryTheory.ObjectProperty.ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : P.FullSubcategory} : P.ι.obj X = X.obj
CategoryTheory.ObjectProperty.lift_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((P.lift F hF).obj X).obj = F.obj X
CategoryTheory.ObjectProperty.ιOfLE_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') (X : P.FullSubcategory) : ((CategoryTheory.ObjectProperty.ιOfLE h).obj X).obj = X.obj
CategoryTheory.ObjectProperty.ι_obj_lift_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X
CategoryTheory.ObjectProperty.ι_obj_lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f
CategoryTheory.Functor.faithful_whiskeringRight_obj 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Faithful
CategoryTheory.Functor.whiskeringLeft_obj_id 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor C E)
CategoryTheory.Functor.whiskeringRight_obj_id 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor E C)
CategoryTheory.Functor.full_whiskeringRight_obj 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] [F.Full] : ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Full
CategoryTheory.Functor.whiskeringLeft_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj G = F.comp G
CategoryTheory.Functor.whiskeringRight_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) (F : CategoryTheory.Functor C D) : ((CategoryTheory.Functor.whiskeringRight C D E).obj H).obj F = F.comp H
CategoryTheory.Functor.whiskeringLeft_obj_map 📋 Mathlib.CategoryTheory.Whiskering
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Functor D E} (α : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).map α = F.whiskerLeft α
CategoryTheory.Functor.whiskeringRight_obj_map 📋 Mathlib.CategoryTheory.Whiskering
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) {X✝ Y✝ : CategoryTheory.Functor C D} (α : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.whiskeringRight C D E).obj H).map α = CategoryTheory.Functor.whiskerRight α H
CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (X✝ : C₁) (X✝¹ : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X✝).obj X✝¹ = X.obj ((F.obj X✝).obj X✝¹)
CategoryTheory.Functor.whiskeringLeft_obj_comp 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : (CategoryTheory.Functor.whiskeringLeft C D' E).obj (F.comp G) = ((CategoryTheory.Functor.whiskeringLeft D D' E).obj G).comp ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
CategoryTheory.Functor.whiskeringRight_obj_comp 📋 Mathlib.CategoryTheory.Whiskering
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : ((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp ((CategoryTheory.Functor.whiskeringRight E D D').obj G) = (CategoryTheory.Functor.whiskeringRight E C D').obj (F.comp G)
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)
CategoryTheory.Functor.postcompose₂_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).obj X✝).map f = X.map ((F.obj X✝).map f)
CategoryTheory.Functor.whiskeringLeft₃ObjObj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) : (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).obj F₃ = CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X✝ : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).obj X✝¹ = (X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).obj X✝¹).obj X✝² = X.obj (((F.obj X✝).obj X✝¹).obj X✝²)
CategoryTheory.Functor.postcompose₂_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).obj F).map f).app X✝¹ = X.map ((F.map f).app X✝¹)
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).map f = (X.obj (F₁.obj X✝)).map (F₂.map f)
CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).obj X✝¹).map f = X.map (((F.obj X✝).obj X✝¹).map f)
CategoryTheory.Functor.whiskeringLeft₃Obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) : (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).obj F₂ = CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂
CategoryTheory.Functor.postcompose₂_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') {X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) : (((CategoryTheory.Functor.postcompose₂.obj X).map α).app X✝¹).app X✝² = X.map ((α.app X✝¹).app X✝²)
CategoryTheory.Functor.postcompose₃_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).obj X✝).map f).app X✝² = X.map (((F.obj X✝).map f).app X✝²)
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).map f).app X✝¹ = (X.map (F₁.map f)).app (F₂.obj X✝¹)
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)
CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).obj F).map f).app X✝¹).app X✝² = X.map (((F.map f).app X✝¹).app X✝²)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)
CategoryTheory.Functor.whiskeringLeft₂_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {X✝ Y✝ : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).obj F₂).map f).app X).app X✝¹ = (f.app (F₁.obj X)).app (F₂.obj X✝¹)
CategoryTheory.Functor.postcompose₃_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{v_7, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E') {X✝ Y✝ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) (X✝³ : C₃) : ((((CategoryTheory.Functor.postcompose₃.obj X).map α).app X✝¹).app X✝²).app X✝³ = X.map (((α.app X✝¹).app X✝²).app X✝³)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)
CategoryTheory.Functor.whiskeringLeft₂_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (φ : X✝ ⟶ Y✝) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X✝¹ : C₁) (c : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).map φ).app X).app X✝¹).app c = (X.obj (F₁.obj X✝¹)).map (φ.app c)
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_map_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {X✝ Y✝ : CategoryTheory.Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X : C₁) (X✝¹ : C₂) (c : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).map τ₃).app F).app X).app X✝¹).app c = ((F.obj (F₁.obj X)).obj (F₂.obj X✝¹)).map (τ₃.app c)
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) {X✝ Y✝ : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)
CategoryTheory.Functor.whiskeringLeft₃_obj_map_app_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Category.{v_4, u_4} D₁] [CategoryTheory.Category.{v_5, u_5} D₂] [CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X✝¹ : C₁) (c : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).map τ₂).app F₃).app X).app X✝¹).app c).app X✝² = ((X.obj (F₁.obj X✝¹)).map (τ₂.app c)).app (F₃.obj X✝²)
CategoryTheory.Functor.toEssImage_obj_obj 📋 Mathlib.CategoryTheory.EssentialImage
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (F.toEssImage.obj X).obj = F.obj X
CategoryTheory.Functor.essImage.liftFunctor_obj 📋 Mathlib.CategoryTheory.EssentialImage
{J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Category.{v_3, u_3} D] (G : CategoryTheory.Functor J D) (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (hG : ∀ (j : J), F.essImage (G.obj j)) (j : J) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).obj j = F.toEssImage.objPreimage { obj := G.obj j, property := ⋯ }
CategoryTheory.Equivalence.functorFunctor_obj 📋 Mathlib.CategoryTheory.Equivalence
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (f : C ≌ D) : (CategoryTheory.Equivalence.functorFunctor C D).obj f = f.functor
CategoryTheory.Equivalence.congrRightFunctor_obj 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) : (CategoryTheory.Equivalence.congrRightFunctor E).obj e = e.congrRight
CategoryTheory.opOp_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)
CategoryTheory.unopUnop_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.unopUnop C).obj X = Opposite.unop (Opposite.unop X)
CategoryTheory.Functor.op_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : Cᵒᵖ) : F.op.obj X = Opposite.op (F.obj (Opposite.unop X))
CategoryTheory.Functor.leftOp_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : Cᵒᵖ) : F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))
CategoryTheory.Functor.rightOp_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : C) : F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))
CategoryTheory.Functor.unop_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : C) : F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))
CategoryTheory.Equivalence.leftOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.functor.obj X = Opposite.unop (e.functor.obj (Opposite.unop X))
CategoryTheory.Equivalence.leftOp_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.inverse.obj X = Opposite.op (e.inverse.obj (Opposite.op X))
CategoryTheory.Equivalence.rightOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.functor.obj X = Opposite.op (e.functor.obj (Opposite.op X))
CategoryTheory.Equivalence.rightOp_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.inverse.obj X = Opposite.unop (e.inverse.obj (Opposite.unop X))
CategoryTheory.Functor.opHom_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor C D)ᵒᵖ) : (CategoryTheory.Functor.opHom C D).obj F = (Opposite.unop F).op
CategoryTheory.Functor.opInv_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) : (CategoryTheory.Functor.opInv C D).obj F = Opposite.op F.unop
CategoryTheory.Functor.leftOpRightOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp
CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) (X : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.op X))
CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op
CategoryTheory.Functor.congr_obj 📋 Mathlib.CategoryTheory.EqToHom
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) (X : C) : F.obj X = G.obj X
CategoryTheory.Equivalence.induced_inverse_obj 📋 Mathlib.CategoryTheory.EqToHom
{D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) (a : D) : (CategoryTheory.Equivalence.induced e).inverse.obj a = e.symm a
CategoryTheory.Functor.const_obj_obj 📋 Mathlib.CategoryTheory.Functor.Const
(J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) (x✝ : J) : ((CategoryTheory.Functor.const J).obj X).obj x✝ = X
CategoryTheory.Functor.const_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
(J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) {X✝ Y✝ : J} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.const J).obj X).map x✝ = CategoryTheory.CategoryStruct.id X
CategoryTheory.Functor.const.unop_functor_op_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) : (Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = CategoryTheory.CategoryStruct.id (Opposite.unop X)
CategoryTheory.Functor.diag_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (a : C) : (CategoryTheory.Functor.diag C).obj a = (a, a)
CategoryTheory.Prod.fst_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.fst C D).obj X = X.1
CategoryTheory.Prod.snd_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.snd C D).obj X = X.2
CategoryTheory.Prod.sectL_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (Z : D) (X : C) : (CategoryTheory.Prod.sectL C Z).obj X = (X, Z)
CategoryTheory.Prod.sectR_obj 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : D) : (CategoryTheory.Prod.sectR Z D).obj X = (Z, X)
CategoryTheory.Prod.swap_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.swap C D).obj X = (X.2, X.1)
CategoryTheory.Functor.prod'_obj 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) (a : A) : (F.prod' G).obj a = (F.obj a, G.obj a)
CategoryTheory.evaluationUncurried_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (p : C × CategoryTheory.Functor C D) : (CategoryTheory.evaluationUncurried C D).obj p = p.2.obj p.1
CategoryTheory.evaluation_obj_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (F : CategoryTheory.Functor C D) : ((CategoryTheory.evaluation C D).obj X).obj F = F.obj X
CategoryTheory.Functor.prod_obj 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D) (X : A × C) : (F.prod G).obj X = (F.obj X.1, G.obj X.2)
CategoryTheory.prodOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (x✝ : Cᵒᵖ × Dᵒᵖ) : (CategoryTheory.prodOpEquiv C).inverse.obj x✝ = Opposite.op (Opposite.unop x✝.1, Opposite.unop x✝.2)
CategoryTheory.prodOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)
CategoryTheory.evaluation_obj_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) {X✝ Y✝ : CategoryTheory.Functor C D} (α : X✝ ⟶ Y✝) : ((CategoryTheory.evaluation C D).obj X).map α = α.app X
CategoryTheory.prodFunctorToFunctorProd_obj 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B × CategoryTheory.Functor A C) : (CategoryTheory.prodFunctorToFunctorProd A B C).obj F = F.1.prod' F.2
CategoryTheory.functorProdToProdFunctor_obj 📋 Mathlib.CategoryTheory.Products.Basic
(A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (B × C)) : (CategoryTheory.functorProdToProdFunctor A B C).obj F = (F.comp (CategoryTheory.Prod.fst B C), F.comp (CategoryTheory.Prod.snd B C))
CategoryTheory.prodFunctor_obj 📋 Mathlib.CategoryTheory.Products.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (FG : CategoryTheory.Functor A B × CategoryTheory.Functor C D) : CategoryTheory.prodFunctor.obj FG = FG.1.prod FG.2
CategoryTheory.Pi.eval_obj 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) (f : (i : I) → C i) : (CategoryTheory.Pi.eval C i).obj f = f i
CategoryTheory.Pi.comap_obj 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (f : (i : I) → C i) (i : J) : (CategoryTheory.Pi.comap C h).obj f i = f (h i)
CategoryTheory.Functor.pi'_obj 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (a : A) (i : I) : (CategoryTheory.Functor.pi' f).obj a i = (f i).obj a
CategoryTheory.Functor.pi_obj 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) (f : (i : I) → C i) (i : I) : (CategoryTheory.Functor.pi F).obj f i = (F i).obj (f i)
CategoryTheory.Pi.sum_obj_obj 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).obj Y s = match s with | Sum.inl i => X i | Sum.inr j => Y j
CategoryTheory.Pi.sum_obj_map 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀} {D : J → Type u₁} [(j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] (X : (i : I) → C i) {x✝ x✝¹ : (j : J) → D j} (f : x✝ ⟶ x✝¹) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).obj X).map f s = match s with | Sum.inl i => CategoryTheory.CategoryStruct.id (X i) | Sum.inr j => f j
CategoryTheory.Discrete.functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I) : (CategoryTheory.Discrete.functor F).obj { as := i } = F i
CategoryTheory.Discrete.functor_obj_eq_as 📋 Mathlib.CategoryTheory.Discrete.Basic
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functor F).obj X = F X.as
CategoryTheory.Discrete.opposite_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
(α : Type u₁) (a✝ : CategoryTheory.Discrete α) : (CategoryTheory.Discrete.opposite α).inverse.obj a✝ = Opposite.op a✝
CategoryTheory.Discrete.opposite_functor_obj_as 📋 Mathlib.CategoryTheory.Discrete.Basic
(α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ) : ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
(J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : J → C) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
(J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }
CategoryTheory.prod.leftUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Discrete PUnit.{w + 1} × C) : (CategoryTheory.prod.leftUnitor C).obj X = X.2
CategoryTheory.prod.rightUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] (X : C × CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.prod.rightUnitor C).obj X = X.1
CategoryTheory.prod.leftInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
CategoryTheory.prod.rightInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
CategoryTheory.Comma.fst_obj 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.fst L R).obj X = X.left
CategoryTheory.Comma.snd_obj 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.snd L R).obj X = X.right
CategoryTheory.Comma.fromProd_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).left = X.1
CategoryTheory.Comma.fromProd_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).right = X.2
CategoryTheory.Comma.equivProd_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).left = X.1
CategoryTheory.Comma.equivProd_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).right = X.2
CategoryTheory.Comma.mapLeft_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).left = X.left
CategoryTheory.Comma.mapLeft_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).right = X.right
CategoryTheory.Comma.mapRight_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRight L r).obj X).left = X.left
CategoryTheory.Comma.mapRight_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRight L r).obj X).right = X.right
CategoryTheory.Comma.equivProd_functor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (a : CategoryTheory.Comma L R) : (CategoryTheory.Comma.equivProd L R).functor.obj a = (a.left, a.right)
CategoryTheory.Comma.preLeft_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right
CategoryTheory.Comma.preRight_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).left = X.left
CategoryTheory.Comma.fromProd_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).hom = CategoryTheory.Discrete.eqToHom ⋯
CategoryTheory.Comma.preLeft_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).left = F.obj X.left
CategoryTheory.Comma.preRight_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right
CategoryTheory.Comma.mapLeftIso_functor_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).left = X.left
CategoryTheory.Comma.mapLeftIso_functor_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).right = X.right
CategoryTheory.Comma.mapLeftIso_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).left = X.left
CategoryTheory.Comma.mapLeftIso_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).right = X.right
CategoryTheory.Comma.mapRightIso_functor_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).left = X.left
CategoryTheory.Comma.mapRightIso_functor_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).right = X.right
CategoryTheory.Comma.mapRightIso_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).left = X.left
CategoryTheory.Comma.mapRightIso_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).right = X.right
CategoryTheory.Comma.post_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).left = X.left
CategoryTheory.Comma.post_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).right = X.right
CategoryTheory.Comma.preLeft_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R) : ((CategoryTheory.Comma.preLeft F L R).obj X).hom = X.hom
CategoryTheory.Comma.preRight_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)) : ((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom
CategoryTheory.Comma.map_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
CategoryTheory.Comma.map_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
CategoryTheory.Comma.mapLeft_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeft R l).obj X).hom = CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom
CategoryTheory.Comma.mapRight_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRight L r).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
CategoryTheory.Comma.post_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.post L R F).obj X).hom = F.map X.hom
CategoryTheory.Comma.mapLeftIso_functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R) : ((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
CategoryTheory.Comma.mapLeftIso_inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
CategoryTheory.Comma.mapRightIso_functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁) : ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
CategoryTheory.Comma.mapRightIso_inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂) : ((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
CategoryTheory.Comma.opFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
CategoryTheory.Comma.unopFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }
CategoryTheory.Comma.map_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
CategoryTheory.Comma.map_obj_hom' 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (α.app X.left) (F.map X.hom)) (β.app X.right)
CategoryTheory.Arrow.leftFunc_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.leftFunc.obj X = X.left
CategoryTheory.Arrow.rightFunc_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)) : CategoryTheory.Arrow.rightFunc.obj X = X.right
CategoryTheory.Functor.mapArrowFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.mapArrowFunctor C D).obj F = F.mapArrow
CategoryTheory.Functor.mapArrow_obj 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C) : F.mapArrow.obj a = CategoryTheory.Arrow.mk (F.map a.hom)
CategoryTheory.Groupoid.invFunctor_obj 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] (unop : C) : (CategoryTheory.Groupoid.invFunctor C).obj unop = Opposite.op unop
CategoryTheory.Groupoid.invEquivalence_functor_obj 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] (unop : C) : (CategoryTheory.Groupoid.invEquivalence C).functor.obj unop = Opposite.op unop
CategoryTheory.Groupoid.invEquivalence_inverse_obj 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] (self : Cᵒᵖ) : (CategoryTheory.Groupoid.invEquivalence C).inverse.obj self = Opposite.unop self
CategoryTheory.uliftFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
(X : Type u) : CategoryTheory.uliftFunctor.{v, u}.obj X = ULift.{v, u} X
CategoryTheory.ofTypeFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
(m : Type u → Type v) [Functor m] [LawfulFunctor m] (x : Type u) : (CategoryTheory.ofTypeFunctor m).obj x = m x
CategoryTheory.Functor.sectionsFunctor_obj 📋 Mathlib.CategoryTheory.Types.Basic
(J : Type u) [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)) : (CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections
CategoryTheory.forget_obj 📋 Mathlib.CategoryTheory.ConcreteCategory.Forget
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
AddCommMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : AddCommMonCat) : ↑(AddCommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
AddMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : AddMonCat) : ↑(AddMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
CommMonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : CommMonCat) : ↑(CommMonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
MonCat.uliftFunctor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : MonCat) : ↑(MonCat.uliftFunctor.obj X) = ULift.{u, v} ↑X
AddCommMonCat.equivalence_functor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : AddCommMonCat) : ↑(AddCommMonCat.equivalence.functor.obj X) = Multiplicative ↑X
AddCommMonCat.equivalence_inverse_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : CommMonCat) : ↑(AddCommMonCat.equivalence.inverse.obj X) = Additive ↑X
AddMonCat.equivalence_functor_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : AddMonCat) : ↑(AddMonCat.equivalence.functor.obj X) = Multiplicative ↑X
AddMonCat.equivalence_inverse_obj_coe 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : MonCat) : ↑(AddMonCat.equivalence.inverse.obj X) = Additive ↑X
AddCommMonCat.coe_forget₂_obj 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : AddCommMonCat) : ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X) = ↑X
CommMonCat.coe_forget₂_obj 📋 Mathlib.Algebra.Category.MonCat.Basic
(X : CommMonCat) : ↑((CategoryTheory.forget₂ CommMonCat MonCat).obj X) = ↑X
AddCommGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
(X : AddCommGrpCat) : AddCommGrpCat.uliftFunctor.obj X = AddCommGrpCat.of (ULift.{u, v} ↑X)
AddGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
(X : AddGrpCat) : AddGrpCat.uliftFunctor.obj X = AddGrpCat.of (ULift.{u, v} ↑X)
CommGrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
(X : CommGrpCat) : CommGrpCat.uliftFunctor.obj X = CommGrpCat.of (ULift.{u, v} ↑X)
GrpCat.uliftFunctor_obj 📋 Mathlib.Algebra.Category.Grp.Basic
(X : GrpCat) : GrpCat.uliftFunctor.obj X = GrpCat.of (ULift.{u, v} ↑X)
CommRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
CommSemiRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
RingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
SemiRingCat.forget_obj 📋 Mathlib.Algebra.Category.Ring.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (X : C) : (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
CommRingCat.forgetToRingCat_obj 📋 Mathlib.Algebra.Category.Ring.Basic
{R : CommRingCat} : ↑((CategoryTheory.forget₂ CommRingCat RingCat).obj R) = ↑R
CommRingCat.commMon_forget₂_obj_coe 📋 Mathlib.Algebra.Category.Ring.Basic
(M : CommRingCat) : ↑(CategoryTheory.HasForget₂.forget₂.obj M) = ↑M
CategoryTheory.Functor.hom_obj 📋 Mathlib.CategoryTheory.Functor.Hom
(C : Type u) [CategoryTheory.Category.{v, u} C] (p : Cᵒᵖ × C) : (CategoryTheory.Functor.hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
CategoryTheory.yoneda_obj_obj 📋 Mathlib.CategoryTheory.Yoneda
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ) : (CategoryTheory.yoneda.obj X).obj Y = (Opposite.unop Y ⟶ X)
CategoryTheory.uliftYoneda_obj_obj 📋 Mathlib.CategoryTheory.Yoneda
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) : (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).obj X✝ = ULift.{w, v₁} (Opposite.unop X✝ ⟶ X)
CategoryTheory.yoneda_obj_map 📋 Mathlib.CategoryTheory.Yoneda
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.yoneda.obj X).map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g
CategoryTheory.uliftYoneda_obj_map 📋 Mathlib.CategoryTheory.Yoneda
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).map f = TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp f.unop x.down }
CategoryTheory.Adjunction.leftAdjointOfEquiv_obj 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) (he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) (a✝ : C) : (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a✝ = F_obj a✝
CategoryTheory.Adjunction.rightAdjointOfEquiv_obj 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)) (he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)) (a✝ : D) : (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a✝ = G_obj a✝
CategoryTheory.Limits.Cocone.forget_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.forget F).obj t = t.pt
CategoryTheory.Limits.Cone.forget_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.forget F).obj t = t.pt
CategoryTheory.Functor.cocones_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : C) : F.cocones.obj X = (F ⟶ (CategoryTheory.Functor.const J).obj X)
CategoryTheory.Functor.cones_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : F.cones.obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
CategoryTheory.Limits.Cocone.precompose_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : G ⟶ F) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.precompose α).obj c).pt = c.pt
CategoryTheory.Limits.Cone.postcompose_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.postcompose α).obj c).pt = c.pt
CategoryTheory.Limits.Cocone.whiskering_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.whiskering E).obj c = CategoryTheory.Limits.Cocone.whisker E c
CategoryTheory.Limits.Cone.whiskering_obj 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whiskering E).obj c = CategoryTheory.Limits.Cone.whisker E c
CategoryTheory.cones_obj_obj 📋 Mathlib.CategoryTheory.Limits.Cones
(J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ((CategoryTheory.cones J C).obj F).obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
CategoryTheory.cocones_obj_obj 📋 Mathlib.CategoryTheory.Limits.Cones
(J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (F : (CategoryTheory.Functor J C)ᵒᵖ) (X : C) : ((CategoryTheory.cocones J C).obj F).obj X = (Opposite.unop F ⟶ (CategoryTheory.Functor.const J).obj X)
CategoryTheory.Limits.Cocone.functoriality_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.functoriality F G).obj A).pt = G.obj A.pt
CategoryTheory.Limits.Cone.functoriality_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.functoriality F G).obj A).pt = G.obj A.pt

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision a114d38 serving mathlib revision e568743