Loogle!
Result
Found 6675 declarations mentioning CategoryTheory.Functor.map. Of these, 2196 have a name containing "_map". Of these, only the first 200 are shown.
- CategoryTheory.Functor.id_map 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Functor.id C).map f = f - CategoryTheory.Functor.toPrefunctor_map 📋 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) {X Y : C} (a✝ : X ⟶ Y) : F.toPrefunctor.map a✝ = F.map a✝ - CategoryTheory.Functor.congr_map 📋 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) {X Y : C} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g - CategoryTheory.Functor.comp_map 📋 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 Y : C} (f : X ⟶ Y) : (F.comp G).map f = G.map (F.map f) - 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.flip_map_app 📋 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)) {d d' : D} (f : d ⟶ d') (c : C) : (F.flip.map f).app c = (F.obj c).map f - CategoryTheory.flipFunctor_map_app_app 📋 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₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) : (((CategoryTheory.flipFunctor C D E).map φ).app Y).app X = (φ.app X).app Y - CategoryTheory.NatIso.isIso_map_iff 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso (F₁.map f) ↔ CategoryTheory.IsIso (F₂.map f) - CategoryTheory.NatIso.inv_map_inv_app 📋 Mathlib.CategoryTheory.NatIso
{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)) {X Y : C} (e : X ≅ Y) (Z : D) : CategoryTheory.inv ((F.map e.inv).app Z) = (F.map e.hom).app Z - CategoryTheory.Functor.FullyFaithful.preimage_map 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) : self.preimage (F.map f) = f - CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso f - CategoryTheory.Functor.preimage_map 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{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.Full] [F.Faithful] (f : X ⟶ Y) : F.preimage (F.map f) = f - CategoryTheory.inducedFunctor_map 📋 Mathlib.CategoryTheory.InducedCategory
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : C → D) {X✝ Y✝ : CategoryTheory.InducedCategory D F} (f : X✝ ⟶ Y✝) : (CategoryTheory.inducedFunctor F).map f = f.hom - CategoryTheory.ObjectProperty.ι_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} {f : X ⟶ Y} : P.ι.map f = f.hom - CategoryTheory.ObjectProperty.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.lift F hF).map f = CategoryTheory.ObjectProperty.homMk (F.map f) - CategoryTheory.ObjectProperty.ιOfLE_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') {X✝ Y✝ : P.FullSubcategory} (f : X✝ ⟶ Y✝) : (CategoryTheory.ObjectProperty.ιOfLE h).map f = CategoryTheory.ObjectProperty.homMk f.hom - 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.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_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₃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₃ObjObj_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₂) {X✝ Y✝ : CategoryTheory.Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) : (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).map τ₃ = CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃ - 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.whiskeringRight_map_app_app 📋 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] {X✝ Y✝ : CategoryTheory.Functor D E} (τ : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C D) (c : C) : (((CategoryTheory.Functor.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c) - 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.whiskeringLeft_map_app_app 📋 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] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) (H : CategoryTheory.Functor D E) (c : C) : (((CategoryTheory.Functor.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c) - 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.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.whiskeringLeft₃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₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) : (CategoryTheory.Functor.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).map τ₂ = CategoryTheory.Functor.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂ - 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.postcompose₂_map_app_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✝ Y✝ : CategoryTheory.Functor E E'} (f : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) (c : C₁) (c✝ : C₂) : (((CategoryTheory.Functor.postcompose₂.map f).app F).app c).app c✝ = f.app ((F.obj c).obj c✝) - 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₃ObjObjObj_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₃ObjObjObj E F₁ F₂ F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²) - CategoryTheory.Functor.postcompose₃_map_app_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✝ Y✝ : CategoryTheory.Functor E E'} (f : X✝ ⟶ Y✝) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (c : C₁) (c✝ : C₂) (c✝¹ : C₃) : ((((CategoryTheory.Functor.postcompose₃.map f).app F).app c).app c✝).app c✝¹ = f.app (((F.obj c).obj c✝).obj c✝¹) - CategoryTheory.Functor.whiskeringLeft₂_map_app_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] {X✝ Y✝ : CategoryTheory.Functor C₁ D₁} (ψ : X✝ ⟶ Y✝) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (c : C₁) (X✝¹ : C₂) : (((((CategoryTheory.Functor.whiskeringLeft₂ E).map ψ).app F₂).app X).app c).app X✝¹ = (X.map (ψ.app c)).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.whiskeringLeft₃_map_app_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] {X✝ Y✝ : CategoryTheory.Functor C₁ D₁} (τ₁ : X✝ ⟶ Y✝) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (c : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((CategoryTheory.Functor.whiskeringLeft₃ E).map τ₁).app F₂).app F₃).app X).app c).app X✝¹).app X✝² = ((X.map (τ₁.app c)).app (F₂.obj X✝¹)).app (F₃.obj X✝²) - CategoryTheory.Functor.toEssImage_map_hom 📋 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✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.toEssImage.map f).hom = F.map f - CategoryTheory.Functor.essImage.liftFunctor_map 📋 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)) {i j : J} (f : i ⟶ j) : (CategoryTheory.Functor.essImage.liftFunctor G F hG).map f = F.preimage (CategoryTheory.CategoryStruct.comp (F.toEssImage.objObjPreimageIso { obj := G.obj i, property := ⋯ }).hom.hom (CategoryTheory.CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv.hom)) - CategoryTheory.Equivalence.functorFunctor_map 📋 Mathlib.CategoryTheory.Equivalence
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C ≌ D} (α : X✝ ⟶ Y✝) : (CategoryTheory.Equivalence.functorFunctor C D).map α = CategoryTheory.Equivalence.asNatTrans α - CategoryTheory.Equivalence.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y)) - CategoryTheory.Equivalence.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y)) - CategoryTheory.Equivalence.congrRightFunctor_map 📋 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 f : C ≌ D} (α : e ⟶ f) : (CategoryTheory.Equivalence.congrRightFunctor E).map α = CategoryTheory.Equivalence.mkHom ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans α)) - CategoryTheory.Equivalence.fun_inv_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h)) - CategoryTheory.Equivalence.inv_fun_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h)) - CategoryTheory.Functor.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : C) (f : X ⟶ Y) : F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y)) - CategoryTheory.Functor.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : D) (f : X ⟶ Y) : F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y)) - CategoryTheory.opOp_map 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.opOp C).map f = f.op.op - CategoryTheory.unopUnop_map 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.unopUnop C).map f = f.unop.unop - CategoryTheory.Functor.op_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✝) : F.op.map f = (F.map f.unop).op - CategoryTheory.Functor.rightOp_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✝) : F.rightOp.map f = (F.map f.op).op - CategoryTheory.Functor.leftOp_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✝) : F.leftOp.map f = (F.map f.unop).unop - CategoryTheory.Functor.rightOp_map_unop 📋 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) : (F.rightOp.map f).unop = F.map f.op - CategoryTheory.Functor.unop_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✝) : F.unop.map f = (F.map f.op).unop - CategoryTheory.Functor.opHom_map_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : (CategoryTheory.Functor C D)ᵒᵖ} (α : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((CategoryTheory.Functor.opHom C D).map α).app X = (α.unop.app (Opposite.unop X)).op - 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.Equivalence.leftOp_inverse_map 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : e.leftOp.inverse.map f = (e.inverse.map f.op).op - CategoryTheory.Equivalence.leftOp_functor_map 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : e.leftOp.functor.map f = (e.functor.map f.unop).unop - CategoryTheory.Functor.leftOpRightOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C Dᵒᵖ} (η : X✝ ⟶ Y✝) : (CategoryTheory.Functor.leftOpRightOpEquiv C D).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op - CategoryTheory.Equivalence.rightOp_functor_map 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : e.rightOp.functor.map f = (e.functor.map f.op).op - CategoryTheory.Functor.opInv_map 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X✝ ⟶ Y✝) : (CategoryTheory.Functor.opInv C D).map α = Quiver.Hom.op { app := fun X => (α.app (Opposite.op X)).unop, naturality := ⋯ } - CategoryTheory.Equivalence.rightOp_inverse_map 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : e.rightOp.inverse.map f = (e.inverse.map f.unop).unop - CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app 📋 Mathlib.CategoryTheory.Opposites
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ} (η : X✝ ⟶ Y✝) (x✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.map η).app x✝ = (η.unop.app (Opposite.op x✝)).op - 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_map_app 📋 Mathlib.CategoryTheory.Functor.Const
(J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : J) : ((CategoryTheory.Functor.const J).map f).app x✝ = f - 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.Prod.fst_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.fst C D).map f = f.1 - CategoryTheory.Prod.snd_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.snd C D).map f = f.2 - CategoryTheory.Prod.sectL_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (Z : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectL C Z).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Z) - CategoryTheory.Prod.sectR_map 📋 Mathlib.CategoryTheory.Products.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectR Z D).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id Z) f - 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.Functor.diag_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Functor.diag C).map f = CategoryTheory.Prod.mkHom f f - CategoryTheory.Functor.prod'_map 📋 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) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : (F.prod' G).map f = CategoryTheory.Prod.mkHom (F.map f) (G.map f) - CategoryTheory.Prod.swap_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C × D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.swap C D).map f = CategoryTheory.Prod.mkHom f.2 f.1 - CategoryTheory.evaluation_map_app 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) (F : CategoryTheory.Functor C D) : ((CategoryTheory.evaluation C D).map f).app F = F.map f - CategoryTheory.Functor.prod_map 📋 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✝ Y✝ : A × C} (f : X✝ ⟶ Y✝) : (F.prod G).map f = CategoryTheory.Prod.mkHom (F.map f.1) (G.map f.2) - CategoryTheory.evaluationUncurried_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {x y : C × CategoryTheory.Functor C D} (f : x ⟶ y) : (CategoryTheory.evaluationUncurried C D).map f = CategoryTheory.CategoryStruct.comp (x.2.map f.1) (f.2.app y.1) - CategoryTheory.prodOpEquiv_inverse_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : Cᵒᵖ × Dᵒᵖ} (x✝ : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).inverse.map x✝ = Opposite.op (CategoryTheory.Prod.mkHom x✝.1.unop x✝.2.unop) - CategoryTheory.prodFunctorToFunctorProd_map 📋 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 G : CategoryTheory.Functor A B × CategoryTheory.Functor A C} (f : F ⟶ G) : (CategoryTheory.prodFunctorToFunctorProd A B C).map f = CategoryTheory.NatTrans.prod' f.1 f.2 - CategoryTheory.prodOpEquiv_functor_map 📋 Mathlib.CategoryTheory.Products.Basic
(C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {X✝ Y✝ : (C × D)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.prodOpEquiv C).functor.map f = CategoryTheory.Prod.mkHom f.unop.1.op f.unop.2.op - CategoryTheory.prodFunctor_map 📋 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] {X✝ Y✝ : CategoryTheory.Functor A B × CategoryTheory.Functor C D} (nm : X✝ ⟶ Y✝) : CategoryTheory.prodFunctor.map nm = CategoryTheory.NatTrans.prod nm.1 nm.2 - CategoryTheory.functorProdToProdFunctor_map 📋 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] {X✝ Y✝ : CategoryTheory.Functor A (B × C)} (α : X✝ ⟶ Y✝) : (CategoryTheory.functorProdToProdFunctor A B C).map α = CategoryTheory.Prod.mkHom (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.fst B C)) (CategoryTheory.Functor.whiskerRight α (CategoryTheory.Prod.snd B C)) - CategoryTheory.eqToHom_map 📋 Mathlib.CategoryTheory.EqToHom
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y) : F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯ - CategoryTheory.eqToHom_map_comp 📋 Mathlib.CategoryTheory.EqToHom
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (F.map (CategoryTheory.eqToHom q)) = F.map (CategoryTheory.eqToHom ⋯) - CategoryTheory.eqToHom_map_comp_assoc 📋 Mathlib.CategoryTheory.EqToHom
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {Z✝ : D} (h : F.obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom q)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯)) h - CategoryTheory.Functor.precomp_map_heq 📋 Mathlib.CategoryTheory.EqToHom
{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 G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor E C) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) {X Y : E} (f : X ⟶ Y) : (H.comp F).map f ≍ (H.comp G).map f - CategoryTheory.Functor.postcomp_map_heq' 📋 Mathlib.CategoryTheory.EqToHom
{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 G : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y} (H : CategoryTheory.Functor D E) (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) : (F.comp H).map f ≍ (G.comp H).map f - CategoryTheory.Functor.postcomp_map_heq 📋 Mathlib.CategoryTheory.EqToHom
{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 G : CategoryTheory.Functor C D} {X Y : C} {f : X ⟶ Y} (H : CategoryTheory.Functor D E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : F.map f ≍ G.map f) : (F.comp H).map f ≍ (G.comp H).map f - CategoryTheory.Equivalence.induced_inverse_map 📋 Mathlib.CategoryTheory.EqToHom
{D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Equivalence.induced e).inverse.map f = CategoryTheory.InducedCategory.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) - CategoryTheory.Pi.eval_map 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) : (CategoryTheory.Pi.eval C i).map α = α i - CategoryTheory.Pi.comap_map 📋 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) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) (i : J) : (CategoryTheory.Pi.comap C h).map α i = α (h i) - CategoryTheory.Functor.pi'_map 📋 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)) {X✝ Y✝ : A} (h : X✝ ⟶ Y✝) (i : I) : (CategoryTheory.Functor.pi' f).map h i = (f i).map h - CategoryTheory.Functor.pi_map 📋 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)) {X✝ Y✝ : (i : I) → C i} (α : X✝ ⟶ Y✝) (i : I) : (CategoryTheory.Functor.pi F).map α i = (F i).map (α i) - 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.Pi.sum_map_app 📋 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 X' : (i : I) → C i} (f : X ⟶ X') (Y : (j : J) → D j) (s : I ⊕ J) : ((CategoryTheory.Pi.sum C).map f).app Y s = match s with | Sum.inl i => f i | Sum.inr j => CategoryTheory.CategoryStruct.id (Y j) - CategoryTheory.Discrete.functor_map_id 📋 Mathlib.CategoryTheory.Discrete.Basic
{J : Type v₁} {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) {j : CategoryTheory.Discrete J} (f : j ⟶ j) : F.map f = CategoryTheory.CategoryStruct.id (F.obj j) - CategoryTheory.Discrete.functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
{C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : CategoryTheory.Discrete I} (f : i ⟶ i) : (CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as) - CategoryTheory.piEquivalenceFunctorDiscrete_functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
(J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as - CategoryTheory.piEquivalenceFunctorDiscrete_inverse_map 📋 Mathlib.CategoryTheory.Discrete.Basic
(J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete J) C} (f : X✝ ⟶ Y✝) (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.map f j = f.app { as := j } - CategoryTheory.prod.leftUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1} × C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.leftUnitor C).map f = f.2 - CategoryTheory.prod.rightUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C × CategoryTheory.Discrete PUnit.{w + 1}} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.rightUnitor C).map f = f.1 - CategoryTheory.prod.leftInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.leftInverseUnitor C).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id { as := PUnit.unit }) f - CategoryTheory.prod.rightInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
(C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.rightInverseUnitor C).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id { as := PUnit.unit }) - CategoryTheory.Comma.fst_map 📋 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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.fst L R).map f = f.left - CategoryTheory.Comma.snd_map 📋 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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.snd L R).map f = f.right - CategoryTheory.Comma.fromProd_map_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 Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.fromProd L R).map f).left = f.1 - CategoryTheory.Comma.fromProd_map_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 Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.fromProd L R).map f).right = f.2 - CategoryTheory.Comma.equivProd_inverse_map_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 Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.equivProd L R).inverse.map f).left = f.1 - CategoryTheory.Comma.equivProd_inverse_map_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 Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.equivProd L R).inverse.map f).right = f.2 - CategoryTheory.Comma.preLeft_map_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✝ Y✝ : CategoryTheory.Comma (F.comp L) R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.preLeft F L R).map f).right = f.right - CategoryTheory.Comma.preRight_map_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) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) {X✝ Y✝ : CategoryTheory.Comma L (F.comp R)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.preRight L F R).map f).left = f.left - CategoryTheory.Comma.post_map_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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.post L R F).map f).left = f.left - CategoryTheory.Comma.post_map_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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.post L R F).map f).right = f.right - CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_right 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.toIdPUnitEquiv L R).inverse.map f).right = f - CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_left 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.toPUnitIdEquiv L R).inverse.map f).left = f - CategoryTheory.Comma.toIdPUnitEquiv_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
{B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.toIdPUnitEquiv L R).functor.map f = f.right - CategoryTheory.Comma.toPUnitIdEquiv_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.toPUnitIdEquiv L R).functor.map f = f.left - CategoryTheory.Comma.mapLeft_map_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✝ Y✝ : CategoryTheory.Comma L₂ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeft R l).map f).left = f.left - CategoryTheory.Comma.mapLeft_map_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✝ Y✝ : CategoryTheory.Comma L₂ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeft R l).map f).right = f.right - CategoryTheory.Comma.mapRight_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₁} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRight L r).map f).left = f.left - CategoryTheory.Comma.mapRight_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₁} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRight L r).map f).right = f.right - CategoryTheory.Comma.preLeft_map_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✝ Y✝ : CategoryTheory.Comma (F.comp L) R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.preLeft F L R).map f).left = F.map f.left - CategoryTheory.Comma.preRight_map_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) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) {X✝ Y✝ : CategoryTheory.Comma L (F.comp R)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.preRight L F R).map f).right = F.map f.right - CategoryTheory.Comma.mapLeftIso_functor_map_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✝ Y✝ : CategoryTheory.Comma L₁ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).left = f.left - CategoryTheory.Comma.mapLeftIso_functor_map_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✝ Y✝ : CategoryTheory.Comma L₁ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).right = f.right - CategoryTheory.Comma.mapLeftIso_inverse_map_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✝ Y✝ : CategoryTheory.Comma L₂ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).left = f.left - CategoryTheory.Comma.mapLeftIso_inverse_map_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✝ Y✝ : CategoryTheory.Comma L₂ R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).right = f.right - CategoryTheory.Comma.mapRightIso_functor_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₁} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRightIso L i).functor.map f).left = f.left - CategoryTheory.Comma.mapRightIso_functor_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₁} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRightIso L i).functor.map f).right = f.right - CategoryTheory.Comma.mapRightIso_inverse_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₂} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).left = f.left - CategoryTheory.Comma.mapRightIso_inverse_map_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] (L : CategoryTheory.Functor A T) {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {X✝ Y✝ : CategoryTheory.Comma L R₂} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).right = f.right - CategoryTheory.Comma.equivProd_functor_map 📋 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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right - CategoryTheory.Comma.map_map_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 Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) : ((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left - CategoryTheory.Comma.map_map_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 Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) : ((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right - CategoryTheory.Comma.unopFunctor_map 📋 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✝ Y✝ : CategoryTheory.Comma L.op R.op} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.unopFunctor L R).map f = Opposite.op { left := f.right.unop, right := f.left.unop, w := ⋯ } - CategoryTheory.Comma.opFunctor_map 📋 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✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.opFunctor L R).map f = Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := ⋯ } - CategoryTheory.Arrow.leftFunc_map 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X✝ ⟶ Y✝) : CategoryTheory.Arrow.leftFunc.map f = f.left - CategoryTheory.Arrow.rightFunc_map 📋 Mathlib.CategoryTheory.Comma.Arrow
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X✝ ⟶ Y✝) : CategoryTheory.Arrow.rightFunc.map f = f.right - CategoryTheory.Functor.mapArrowFunctor_map_app_left 📋 Mathlib.CategoryTheory.Comma.Arrow
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) (f : CategoryTheory.Arrow C) : (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).left = τ.app ((CategoryTheory.Functor.id C).obj f.left) - CategoryTheory.Functor.mapArrowFunctor_map_app_right 📋 Mathlib.CategoryTheory.Comma.Arrow
(C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) (f : CategoryTheory.Arrow C) : (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).right = τ.app ((CategoryTheory.Functor.id C).obj f.right) - CategoryTheory.Functor.mapArrow_map_left 📋 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) {X✝ Y✝ : CategoryTheory.Arrow C} (f : X✝ ⟶ Y✝) : (F.mapArrow.map f).left = F.map f.left - CategoryTheory.Functor.mapArrow_map_right 📋 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) {X✝ Y✝ : CategoryTheory.Arrow C} (f : X✝ ⟶ Y✝) : (F.mapArrow.map f).right = F.map f.right - CategoryTheory.MorphismProperty.map_mem_map 📋 Mathlib.CategoryTheory.MorphismProperty.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (hf : P f) : P.map F (F.map f) - CategoryTheory.Groupoid.invFunctor_map 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (CategoryTheory.Groupoid.invFunctor C).map f = (CategoryTheory.Groupoid.inv f).op - CategoryTheory.Groupoid.invEquivalence_functor_map 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (CategoryTheory.Groupoid.invEquivalence C).functor.map f = (CategoryTheory.Groupoid.inv f).op - CategoryTheory.Groupoid.invEquivalence_inverse_map 📋 Mathlib.CategoryTheory.Groupoid
(C : Type u) [CategoryTheory.Groupoid C] {x y : Cᵒᵖ} (f : x ⟶ y) : (CategoryTheory.Groupoid.invEquivalence C).inverse.map f = CategoryTheory.Groupoid.inv f.unop - CategoryTheory.uliftFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
{X Y : Type u} (f : X ⟶ Y) (x : ULift.{v, u} X) : CategoryTheory.uliftFunctor.{v, u}.map f x = { down := f x.down } - CategoryTheory.ofTypeFunctor_map 📋 Mathlib.CategoryTheory.Types.Basic
(m : Type u → Type v) [Functor m] [LawfulFunctor m] {α β : Type u} (f : α → β) : (CategoryTheory.ofTypeFunctor m).map f = Functor.map f - CategoryTheory.FunctorToTypes.map_hom_map_inv_apply 📋 Mathlib.CategoryTheory.Types.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y : C} (f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y - CategoryTheory.FunctorToTypes.map_inv_map_hom_apply 📋 Mathlib.CategoryTheory.Types.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y : C} (f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x - CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply 📋 Mathlib.CategoryTheory.Types.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y Z : C} (p : X = Y) (q : Y = Z) (x : F.obj X) : F.map (CategoryTheory.eqToHom q) (F.map (CategoryTheory.eqToHom p) x) = F.map (CategoryTheory.eqToHom ⋯) x - CategoryTheory.Functor.sectionsFunctor_map_coe 📋 Mathlib.CategoryTheory.Types.Basic
(J : Type u) [CategoryTheory.Category.{v, u} J] {F G : CategoryTheory.Functor J (Type w)} (φ : F ⟶ G) (x : ↑F.sections) (j : J) : ↑((CategoryTheory.Functor.sectionsFunctor J).map φ x) j = φ.app j (↑x j) - CategoryTheory.forget_map_eq_coe 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasForget C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.forget C).map f = ⇑f - CategoryTheory.ConcreteCategory.forget_map_eq_coe 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.forget C).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - AddMonCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{x✝ x✝¹ : AddMonCat} (f : x✝ ⟶ x✝¹) : AddMonCat.uliftFunctor.map f = AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)) - MonCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{x✝ x✝¹ : MonCat} (f : x✝ ⟶ x✝¹) : MonCat.uliftFunctor.map f = MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((MonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) - AddCommMonCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{x✝ x✝¹ : AddCommMonCat} (f : x✝ ⟶ x✝¹) : AddCommMonCat.uliftFunctor.map f = AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommMonCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)) - CommMonCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{x✝ x✝¹ : CommMonCat} (f : x✝ ⟶ x✝¹) : CommMonCat.uliftFunctor.map f = CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommMonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) - AddMonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : AddMonCat} (f : X ⟶ Y) : (CategoryTheory.forget AddMonCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - MonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : MonCat} (f : X ⟶ Y) : (CategoryTheory.forget MonCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - AddMonCat.equivalence_functor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X✝ Y✝ : AddMonCat} (f : X✝ ⟶ Y✝) : AddMonCat.equivalence.functor.map f = MonCat.ofHom (AddMonoidHom.toMultiplicative (AddMonCat.Hom.hom f)) - AddMonCat.equivalence_inverse_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X✝ Y✝ : MonCat} (f : X✝ ⟶ Y✝) : AddMonCat.equivalence.inverse.map f = AddMonCat.ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f)) - AddCommMonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : AddCommMonCat} (f : X ⟶ Y) : (CategoryTheory.forget AddCommMonCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - CommMonCat.forget_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : CommMonCat} (f : X ⟶ Y) : (CategoryTheory.forget CommMonCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - AddCommMonCat.equivalence_functor_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X✝ Y✝ : AddCommMonCat} (f : X✝ ⟶ Y✝) : AddCommMonCat.equivalence.functor.map f = CommMonCat.ofHom (AddMonoidHom.toMultiplicative (AddCommMonCat.Hom.hom f)) - AddCommMonCat.equivalence_inverse_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X✝ Y✝ : CommMonCat} (f : X✝ ⟶ Y✝) : AddCommMonCat.equivalence.inverse.map f = AddCommMonCat.ofHom (MonoidHom.toAdditive (CommMonCat.Hom.hom f)) - AddCommMonCat.forget₂_map_ofHom 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).map (AddCommMonCat.ofHom f) = AddMonCat.ofHom f - CommMonCat.forget₂_map_ofHom 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : (CategoryTheory.forget₂ CommMonCat MonCat).map (CommMonCat.ofHom f) = MonCat.ofHom f - AddCommMonCat.hom_forget₂_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : AddCommMonCat} (f : X ⟶ Y) : AddMonCat.Hom.hom ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).map f) = AddCommMonCat.Hom.hom f - CommMonCat.hom_forget₂_map 📋 Mathlib.Algebra.Category.MonCat.Basic
{X Y : CommMonCat} (f : X ⟶ Y) : MonCat.Hom.hom ((CategoryTheory.forget₂ CommMonCat MonCat).map f) = CommMonCat.Hom.hom f - AddGrpCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.Grp.Basic
{x✝ x✝¹ : AddGrpCat} (f : x✝ ⟶ x✝¹) : AddGrpCat.uliftFunctor.map f = AddGrpCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)) - GrpCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.Grp.Basic
{x✝ x✝¹ : GrpCat} (f : x✝ ⟶ x✝¹) : GrpCat.uliftFunctor.map f = GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((GrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) - AddCommGrpCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.Grp.Basic
{x✝ x✝¹ : AddCommGrpCat} (f : x✝ ⟶ x✝¹) : AddCommGrpCat.uliftFunctor.map f = AddCommGrpCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom)) - CommGrpCat.uliftFunctor_map 📋 Mathlib.Algebra.Category.Grp.Basic
{x✝ x✝¹ : CommGrpCat} (f : x✝ ⟶ x✝¹) : CommGrpCat.uliftFunctor.map f = CommGrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommGrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)) - GrpCat.forget_map 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : GrpCat} (f : X ⟶ Y) : (CategoryTheory.forget GrpCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - AddGrpCat.forget₂_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [AddGroup X] [AddGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddGrpCat AddMonCat).map (AddGrpCat.ofHom f) = AddMonCat.ofHom f - GrpCat.forget₂_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [Group X] [Group Y] (f : X →* Y) : (CategoryTheory.forget₂ GrpCat MonCat).map (GrpCat.ofHom f) = MonCat.ofHom f - AddCommGrpCat.forget_map 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : AddCommGrpCat} (f : X ⟶ Y) : (CategoryTheory.forget AddCommGrpCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - CommGrpCat.forget_map 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : CommGrpCat} (f : X ⟶ Y) : (CategoryTheory.forget CommGrpCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - AddCommGrpCat.forget₂_commMonCat_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).map (AddCommGrpCat.ofHom f) = AddCommMonCat.ofHom f - CommGrpCat.forget₂_commMonCat_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (CategoryTheory.forget₂ CommGrpCat CommMonCat).map (CommGrpCat.ofHom f) = CommMonCat.ofHom f - AddCommGrpCat.forget₂_addGrp_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [AddCommGroup X] [AddCommGroup Y] (f : X →+ Y) : (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).map (AddCommGrpCat.ofHom f) = AddGrpCat.ofHom f - CommGrpCat.forget₂_grp_map_ofHom 📋 Mathlib.Algebra.Category.Grp.Basic
{X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : (CategoryTheory.forget₂ CommGrpCat GrpCat).map (CommGrpCat.ofHom f) = GrpCat.ofHom f - SemiRingCat.forget_map 📋 Mathlib.Algebra.Category.Ring.Basic
{R S : SemiRingCat} (f : R ⟶ S) : (CategoryTheory.forget SemiRingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - CommRingCat.forget₂_map 📋 Mathlib.Algebra.Category.Ring.Basic
{X✝ Y✝ : CommRingCat} (f : X✝ ⟶ Y✝) : CategoryTheory.HasForget₂.forget₂.map f = CommMonCat.ofHom ↑(CommRingCat.Hom.hom f) - RingCat.forget_map_apply 📋 Mathlib.Algebra.Category.Ring.Basic
{R S : RingCat} (f : R ⟶ S) (x : (CategoryTheory.forget RingCat).obj R) : (CategoryTheory.forget RingCat).map f x = (CategoryTheory.ConcreteCategory.hom f) x - CommSemiRingCat.forget_map 📋 Mathlib.Algebra.Category.Ring.Basic
{R S : CommSemiRingCat} (f : R ⟶ S) : (CategoryTheory.forget CommSemiRingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - RingCat.forget_map 📋 Mathlib.Algebra.Category.Ring.Basic
{R S : RingCat} (f : R ⟶ S) : (CategoryTheory.forget RingCat).map f = ⇑(CategoryTheory.ConcreteCategory.hom f) - CommRingCat.forget_map_apply 📋 Mathlib.Algebra.Category.Ring.Basic
{R S : CommRingCat} (f : R ⟶ S) (x : (CategoryTheory.forget CommRingCat).obj R) : (CategoryTheory.forget CommRingCat).map f x = (CategoryTheory.ConcreteCategory.hom f) x
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. 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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
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.
This is Loogle revision 6ff4759 serving mathlib revision 519f454