Loogle!

Result

Found 5542 declarations mentioning Prefunctor.map. Of these, only the first 200 are shown.

Prefunctor.id_map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
(V : Type u_1) [Quiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) : (𝟭q V).map f = f
Prefunctor.map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{V : Type u₁} [Quiver V] {W : Type u₂} [Quiver W] (self : V ⥤q W) {X Y : V} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
Prefunctor.congr_map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g
Prefunctor.mk_map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X Y : V} {f : X ⟶ Y} : { obj := obj, map := map }.map f = map f
Prefunctor.comp_map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {W : Type u_3} [Quiver W] (F : U ⥤q V) (G : V ⥤q W) {X✝ Y✝ : U} (f : X✝ ⟶ Y✝) : (F ⋙q G).map f = G.map (F.map f)
Prefunctor.congr_hom 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U} (f : X ⟶ Y) : Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f
Prefunctor.homOfEq_map 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y) {X' Y' : U} (hX : X = X') (hY : Y = Y') : F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯
Prefunctor.ext' 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{V W : Type u} [Quiver V] [Quiver W] {F G : V ⥤q W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯) : F = G
Prefunctor.ext 📋 Mathlib.Combinatorics.Quiver.Prefunctor
{V : Type u} [Quiver V] {W : Type u₂} [Quiver W] {F G : V ⥤q W} (h_obj : ∀ (X : V), F.obj X = G.obj X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) : F = G
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.map_id 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) (X : C) : self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
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.map_comp 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
CategoryTheory.Functor.map_dite 📋 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} {P : Prop} [Decidable P] (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)) : F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
CategoryTheory.Functor.mk 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (toPrefunctor : C ⥤q D) (map_id : ∀ (X : C), toPrefunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toPrefunctor.obj X) := by aesop_cat) (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toPrefunctor.map f) (toPrefunctor.map g) := by aesop_cat) : CategoryTheory.Functor C D
CategoryTheory.Functor.map_comp_assoc 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{u_1, u₁} C] {D : Type u₂} [CategoryTheory.Category.{u_2, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)
CategoryTheory.Functor.mk.sizeOf_spec 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [SizeOf C] [SizeOf D] (toPrefunctor : C ⥤q D) (map_id : ∀ (X : C), toPrefunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toPrefunctor.obj X) := by aesop_cat) (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toPrefunctor.map f) (toPrefunctor.map g) := by aesop_cat) : sizeOf { toPrefunctor := toPrefunctor, map_id := map_id, map_comp := map_comp } = 1 + sizeOf toPrefunctor
CategoryTheory.Functor.mk.injEq 📋 Mathlib.CategoryTheory.Functor.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (toPrefunctor : C ⥤q D) (map_id : ∀ (X : C), toPrefunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toPrefunctor.obj X) := by aesop_cat) (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toPrefunctor.map f) (toPrefunctor.map g) := by aesop_cat) (toPrefunctor✝ : C ⥤q D) (map_id✝ : ∀ (X : C), toPrefunctor✝.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toPrefunctor✝.obj X) := by aesop_cat) (map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toPrefunctor✝.map f) (toPrefunctor✝.map g) := by aesop_cat) : ({ toPrefunctor := toPrefunctor, map_id := map_id, map_comp := map_comp } = { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }) = (toPrefunctor = toPrefunctor✝)
CategoryTheory.NatTrans.naturality 📋 Mathlib.CategoryTheory.NatTrans
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
CategoryTheory.NatTrans.mk 📋 Mathlib.CategoryTheory.NatTrans
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ⟶ G.obj X) (naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f) := by aesop_cat) : CategoryTheory.NatTrans F G
CategoryTheory.NatTrans.naturality_assoc 📋 Mathlib.CategoryTheory.NatTrans
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app Y) h) = CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (G.map f) h)
CategoryTheory.NatTrans.mk.sizeOf_spec 📋 Mathlib.CategoryTheory.NatTrans
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} [SizeOf C] [SizeOf D] (app : (X : C) → F.obj X ⟶ G.obj X) (naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f) := by aesop_cat) : sizeOf { app := app, naturality := naturality } = 1
CategoryTheory.NatTrans.mk.injEq 📋 Mathlib.CategoryTheory.NatTrans
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ⟶ G.obj X) (naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f) := by aesop_cat) (app✝ : (X : C) → F.obj X ⟶ G.obj X) (naturality✝ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app✝ Y) = CategoryTheory.CategoryStruct.comp (app✝ X) (G.map f) := by aesop_cat) : ({ app := app, naturality := naturality } = { app := app✝, naturality := naturality✝ }) = (app = app✝)
CategoryTheory.Functor.map_isIso 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (F.map f)
CategoryTheory.Functor.mapIso_hom 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y) : (F.mapIso i).hom = F.map i.hom
CategoryTheory.Functor.mapIso_inv 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y) : (F.mapIso i).inv = F.map i.inv
CategoryTheory.Functor.map_inv 📋 Mathlib.CategoryTheory.Iso
{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.IsIso f] : F.map (CategoryTheory.inv f) = CategoryTheory.inv (F.map f)
CategoryTheory.Iso.map_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Iso.map_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
CategoryTheory.Functor.map_hom_inv 📋 Mathlib.CategoryTheory.Iso
{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.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.map_inv_hom 📋 Mathlib.CategoryTheory.Iso
{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.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (F.map f) = CategoryTheory.CategoryStruct.id (F.obj Y)
CategoryTheory.Iso.map_hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (F.map e.inv) h) = h
CategoryTheory.Iso.map_inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Iso
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (F.map e.hom) h) = h
CategoryTheory.Functor.map_hom_inv_assoc 📋 Mathlib.CategoryTheory.Iso
{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.IsIso f] {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) h) = h
CategoryTheory.Functor.map_inv_hom_assoc 📋 Mathlib.CategoryTheory.Iso
{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.IsIso f] {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (CategoryTheory.CategoryStruct.comp (F.map f) h) = h
CategoryTheory.NatTrans.hcomp_id_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 G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} (α : F ⟶ G) (X : C) : (α ◫ CategoryTheory.CategoryStruct.id H).app X = H.map (α.app X)
CategoryTheory.NatTrans.hcomp_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 G : CategoryTheory.Functor C D} {H I : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : (α ◫ β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))
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.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.Iso.map_hom_inv_id_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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
CategoryTheory.Iso.map_inv_hom_id_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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)
CategoryTheory.Iso.map_hom_inv_id_app_assoc 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj X).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) h) = h
CategoryTheory.Iso.map_inv_hom_id_app_assoc 📋 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] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj Y).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) h) = h
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)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : (F.flip.map f).app j = (F.obj j).map f
CategoryTheory.NatTrans.app_naturality 📋 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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
CategoryTheory.NatTrans.naturality_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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)
CategoryTheory.NatTrans.app_naturality_assoc 📋 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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) {Z✝ : E} (h : (G.obj X).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.obj X).map f) (CategoryTheory.CategoryStruct.comp ((T.app X).app Z) h) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) (CategoryTheory.CategoryStruct.comp ((G.obj X).map f) h)
CategoryTheory.NatTrans.naturality_app_assoc 📋 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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) {Z✝ : E} (h : (G.obj Y).obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((F.map f).app Z) (CategoryTheory.CategoryStruct.comp ((T.app Y).app Z) h) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) (CategoryTheory.CategoryStruct.comp ((G.map f).app Z) h)
CategoryTheory.NatTrans.naturality_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] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (((α.app Y₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (((G.map f).app X₂).app X₃)
CategoryTheory.NatTrans.naturality_app_app_assoc 📋 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] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj Y₁).obj X₂).obj X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((α.app Y₁).app X₂).app X₃) h) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((G.map f).app X₂).app X₃) h)
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.Functor.copyObj.eq_1 📋 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) : F.copyObj obj e = { obj := obj, map := fun {X Y} f => CategoryTheory.CategoryStruct.comp (e X).inv (CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom), map_id := ⋯, map_comp := ⋯ }
CategoryTheory.NatIso.naturality_1 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (F.map f) (α.hom.app Y)) = G.map f
CategoryTheory.NatIso.naturality_2 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (α.inv.app Y)) = F.map f
CategoryTheory.NatIso.naturality_1' 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : CategoryTheory.IsIso (α.app X)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app X)) (CategoryTheory.CategoryStruct.comp (F.map f) (α.app Y)) = G.map f
CategoryTheory.NatIso.naturality_2' 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : CategoryTheory.IsIso (α.app Y)} : CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.inv (α.app Y))) = F.map f
CategoryTheory.NatIso.ofComponents 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by aesop_cat) : F ≅ G
CategoryTheory.NatIso.ofComponents.app 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app' : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app' Y).hom = CategoryTheory.CategoryStruct.comp (app' X).hom (G.map f)) (X : C) : (CategoryTheory.NatIso.ofComponents app' naturality).app X = app' X
CategoryTheory.NatIso.naturality_2'_assoc 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x✝ : CategoryTheory.IsIso (α.app Y)} {Z : D} (h : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app Y)) h)) = CategoryTheory.CategoryStruct.comp (F.map f) h
CategoryTheory.NatIso.ofComponents_hom_app 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by aesop_cat) (X : C) : (CategoryTheory.NatIso.ofComponents app naturality).hom.app X = (app X).hom
CategoryTheory.NatIso.ofComponents_inv_app 📋 Mathlib.CategoryTheory.NatIso
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f) := by aesop_cat) (X : C) : (CategoryTheory.NatIso.ofComponents app naturality).inv.app X = (app X).inv
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.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.Functor.map_injective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} (F : CategoryTheory.Functor C D) [F.Faithful] : Function.Injective F.map
CategoryTheory.Functor.map_surjective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X Y : C} (F : CategoryTheory.Functor C D) [F.Full] : Function.Surjective F.map
CategoryTheory.Functor.Faithful.map_injective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.Faithful] {X Y : C} : Function.Injective F.map
CategoryTheory.Functor.Full.map_surjective 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.Full] {X Y : C} : Function.Surjective F.map
CategoryTheory.Functor.Full.mk 📋 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} (map_surjective : ∀ {X Y : C}, Function.Surjective F.map) : F.Full
CategoryTheory.Functor.FullyFaithful.map_bijective 📋 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) : Function.Bijective F.map
CategoryTheory.Functor.FullyFaithful.map_surjective 📋 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} : Function.Surjective F.map
CategoryTheory.Functor.Faithful.mk 📋 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} (map_injective : ∀ {X Y : C}, Function.Injective F.map := by aesop_cat) : F.Faithful
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.isIso_of_fully_faithful 📋 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) [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso f
CategoryTheory.Functor.FullyFaithful.map_injective 📋 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 g : X ⟶ Y} (h : F.map f = F.map g) : f = g
CategoryTheory.Functor.map_injective_iff 📋 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) [F.Faithful] {X Y : C} (f g : X ⟶ Y) : F.map f = F.map g ↔ f = g
CategoryTheory.Functor.map_preimage 📋 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) [F.Full] {X Y : C} (f : F.obj X ⟶ F.obj Y) : F.map (F.preimage f) = f
CategoryTheory.Functor.FullyFaithful.map_preimage 📋 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 : F.obj X ⟶ F.obj Y) : F.map (self.preimage f) = f
CategoryTheory.Functor.FullyFaithful.mk 📋 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} (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) (map_preimage : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f := by aesop_cat) (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f := by aesop_cat) : F.FullyFaithful
CategoryTheory.Functor.Faithful.div 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{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 E) (G : CategoryTheory.Functor D E) [G.Faithful] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : CategoryTheory.Functor C D
CategoryTheory.Functor.Faithful.div_faithful 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{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 E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful
CategoryTheory.Functor.FullyFaithful.mk.sizeOf_spec 📋 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} [SizeOf C] [SizeOf D] (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) (map_preimage : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f := by aesop_cat) (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f := by aesop_cat) : sizeOf { preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } = 1
CategoryTheory.Functor.Faithful.div_comp 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
{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 E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
CategoryTheory.Functor.FullyFaithful.homEquiv_apply 📋 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} (a✝ : X ⟶ Y) : hF.homEquiv a✝ = F.map a✝
CategoryTheory.Functor.FullyFaithful.mk.injEq 📋 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} (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) (map_preimage : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f := by aesop_cat) (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f := by aesop_cat) (preimage✝ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) (map_preimage✝ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage✝ f) = f := by aesop_cat) (preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), preimage✝ (F.map f) = f := by aesop_cat) : ({ preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } = { preimage := preimage✝, map_preimage := map_preimage✝, preimage_map := preimage_map✝ }) = (preimage = preimage✝)
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
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 = f
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 = F.map f
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
CategoryTheory.fullSubcategoryInclusion.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
CategoryTheory.fullSubcategoryInclusion_map_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.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.whiskerRight_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] {G H : CategoryTheory.Functor C D} (α : G ⟶ H) (F : CategoryTheory.Functor D E) (X : C) : (CategoryTheory.whiskerRight α F).app X = F.map (α.app X)
CategoryTheory.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.whiskeringLeft C D E).obj F).map α = CategoryTheory.whiskerLeft F α
CategoryTheory.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.whiskeringRight C D E).obj H).map α = CategoryTheory.whiskerRight α H
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {X✝ Y✝ : CategoryTheory.Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) : (CategoryTheory.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).map τ₃ = CategoryTheory.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃
CategoryTheory.Functor.postcompose₂_obj_obj_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{u_11, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_12, 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.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.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
CategoryTheory.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.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.postcompose₂_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{u_11, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_12, 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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_4} D₁] [CategoryTheory.Category.{u_11, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{u_12, 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.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).map f = (X.obj (F₁.obj X✝)).map (F₂.map f)
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {X✝ Y✝ : CategoryTheory.Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) : (CategoryTheory.whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).map τ₂ = CategoryTheory.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂
CategoryTheory.Functor.postcompose₂_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{u_11, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_12, 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_obj_map 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] [CategoryTheory.Category.{u_11, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{u_12, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_13, 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_obj_obj_map_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] [CategoryTheory.Category.{u_11, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{u_12, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_13, 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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_4} D₁] [CategoryTheory.Category.{u_11, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{u_12, 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.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).map f).app X✝¹ = (X.map (F₁.map f)).app (F₂.obj X✝¹)
CategoryTheory.Functor.postcompose₂_map_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] {E : Type u_7} [CategoryTheory.Category.{u_11, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_12, 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.postcompose₃_obj_obj_map_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] [CategoryTheory.Category.{u_11, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{u_12, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_13, 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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_4} D₁] [CategoryTheory.Category.{u_11, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{u_12, 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.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.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] [CategoryTheory.Category.{u_11, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{u_12, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_13, 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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_4} D₁] [CategoryTheory.Category.{u_11, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{u_12, 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.whiskeringLeft₂ E).obj F₁).map φ).app X).app X✝¹).app c = (X.obj (F₁.obj X✝¹)).map (φ.app c)
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.whiskeringLeft₃ObjObjMap_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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) {F₃ F₃' : CategoryTheory.Functor C₃ D₃} (τ₃ : F₃ ⟶ F₃') (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) : (CategoryTheory.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃).app F = CategoryTheory.whiskerLeft F₁ (CategoryTheory.whiskerLeft F (((CategoryTheory.whiskeringLeft₂ E).obj F₂).map τ₃))
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.postcompose₃_map_app_app_app_app 📋 Mathlib.CategoryTheory.Whiskering
{C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [CategoryTheory.Category.{u_9, u_1} C₁] [CategoryTheory.Category.{u_10, u_2} C₂] [CategoryTheory.Category.{u_11, u_3} C₃] {E : Type u_7} [CategoryTheory.Category.{u_12, u_7} E] {E' : Type u_8} [CategoryTheory.Category.{u_13, 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.whiskeringLeft₃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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, u_7} E] {F₁ F₁' : CategoryTheory.Functor C₁ D₁} (τ₁ : F₁ ⟶ F₁') (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) : ((CategoryTheory.whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁).app F₂).app F₃ = CategoryTheory.whiskerLeft ((CategoryTheory.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)) (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj (((CategoryTheory.whiskeringLeft₂ E).obj F₂).obj F₃)) ((CategoryTheory.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map τ₁)
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_4} D₁] [CategoryTheory.Category.{u_11, u_5} D₂] (E : Type u_7) [CategoryTheory.Category.{u_12, 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.whiskeringLeft₂ E).map ψ).app F₂).app X).app c).app X✝¹ = (X.map (ψ.app c)).app (F₂.obj X✝¹)
CategoryTheory.whiskeringLeft₃ObjMap_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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁) {F₂ F₂' : CategoryTheory.Functor C₂ D₂} (τ₂ : F₂ ⟶ F₂') (F₃ : CategoryTheory.Functor C₃ D₃) : (CategoryTheory.whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂).app F₃ = CategoryTheory.whiskerRight ((CategoryTheory.whiskeringRight D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)) (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).map (((CategoryTheory.whiskeringLeft₂ E).map τ₂).app F₃)) ((CategoryTheory.whiskeringLeft C₁ D₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))).obj F₁)
CategoryTheory.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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.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.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_11, u_4} D₁] [CategoryTheory.Category.{u_12, u_5} D₂] [CategoryTheory.Category.{u_13, u_6} D₃] (E : Type u_7) [CategoryTheory.Category.{u_14, 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.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 📋 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 = F.map f
CategoryTheory.Functor.essImage_ext 📋 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 : F.EssImageSubcategory} (f g : X ⟶ Y) (h : F.essImage.ι.map f = F.essImage.ι.map g) : f = g
CategoryTheory.Functor.essImage.liftFunctor_map 📋 Mathlib.CategoryTheory.EssentialImage
{J : Type u_1} {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_1} J] [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Category.{u_6, 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 (CategoryTheory.CategoryStruct.comp (G.map f) (F.toEssImage.objObjPreimageIso { obj := G.obj j, property := ⋯ }).inv))
CategoryTheory.Equivalence.funInvIdAssoc_hom_app 📋 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) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
CategoryTheory.Equivalence.funInvIdAssoc_inv_app 📋 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) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)
CategoryTheory.Equivalence.invFunIdAssoc_hom_app 📋 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) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
CategoryTheory.Equivalence.invFunIdAssoc_inv_app 📋 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) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)
CategoryTheory.Equivalence.counitInv_app_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
CategoryTheory.Equivalence.counit_app_functor 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
CategoryTheory.Equivalence.unitInv_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
CategoryTheory.Equivalence.unit_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
CategoryTheory.Equivalence.changeInverse_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
CategoryTheory.Equivalence.changeInverse_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
CategoryTheory.Equivalence.counitInv_naturality 📋 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) : CategoryTheory.CategoryStruct.comp (e.counitInv.app X) (e.functor.map (e.inverse.map f)) = CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y)
CategoryTheory.Equivalence.unit_naturality 📋 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) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.inverse.map (e.functor.map f)) = CategoryTheory.CategoryStruct.comp f (e.unit.app Y)
CategoryTheory.Equivalence.counitInv_functor_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h
CategoryTheory.Equivalence.functor_unit_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h
CategoryTheory.Equivalence.inverse_counitInv_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h
CategoryTheory.Equivalence.unit_inverse_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h
CategoryTheory.Equivalence.adjointify_η_ε_assoc 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.obj X)) h) = h
CategoryTheory.Equivalence.counit_naturality 📋 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) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (e.counit.app Y) = CategoryTheory.CategoryStruct.comp (e.counit.app X) f
CategoryTheory.Equivalence.unitInv_naturality 📋 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) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) f
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.functor_unit_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
CategoryTheory.Equivalence.inverse_counitInv_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
CategoryTheory.Equivalence.counitInv_naturality_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.counitInv.app X) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h)
CategoryTheory.Equivalence.counit_naturality_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 : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Equivalence.unitInv_naturality_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 : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) h) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f h)
CategoryTheory.Equivalence.unit_naturality_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.unit.app X) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h)
CategoryTheory.Equivalence.counitInv_functor_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
CategoryTheory.Equivalence.unit_inverse_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
CategoryTheory.Equivalence.mk' 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by aesop_cat) : C ≌ D
CategoryTheory.Equivalence.adjointify_η_ε 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Iso.inverseCompIso_hom_app 📋 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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
CategoryTheory.Iso.inverseCompIso_inv_app 📋 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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))
CategoryTheory.Iso.isoInverseComp_hom_app 📋 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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
CategoryTheory.Iso.isoInverseComp_inv_app 📋 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] {F : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
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.Iso.compInverseIso_hom_app 📋 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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
CategoryTheory.Iso.compInverseIso_inv_app 📋 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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
CategoryTheory.Iso.isoCompInverse_hom_app 📋 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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
CategoryTheory.Iso.isoCompInverse_inv_app 📋 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] {F : CategoryTheory.Functor C E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))
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.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.Equivalence.functor_unitIso_comp 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)
CategoryTheory.Equivalence.Equivalence_mk'_counit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom
CategoryTheory.Equivalence.Equivalence_mk'_counitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv
CategoryTheory.Equivalence.Equivalence_mk'_unit 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom
CategoryTheory.Equivalence.Equivalence_mk'_unitInv 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv
CategoryTheory.Equivalence.mk'.sizeOf_spec 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [SizeOf C] [SizeOf D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by aesop_cat) : sizeOf { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso, functor_unitIso_comp := functor_unitIso_comp } = 1 + sizeOf functor + sizeOf inverse + sizeOf unitIso + sizeOf counitIso
CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X))) (G'.inverse.map (G.counitIso.hom.app X)))
CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X))) (G'.unitIso.inv.app (G.inverse.obj X)))
CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.hom.app X = CategoryTheory.CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X))) (G'.functor.map (G.unitIso.inv.app X)))
CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.inv.app X = CategoryTheory.CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X))) (G'.counitIso.hom.app (G.functor.obj X)))
CategoryTheory.Equivalence.mk'.injEq 📋 Mathlib.CategoryTheory.Equivalence
{C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by aesop_cat) (functor✝ : CategoryTheory.Functor C D) (inverse✝ : CategoryTheory.Functor D C) (unitIso✝ : CategoryTheory.Functor.id C ≅ functor✝.comp inverse✝) (counitIso✝ : inverse✝.comp functor✝ ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp✝ : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor✝.map (unitIso✝.hom.app X)) (counitIso✝.hom.app (functor✝.obj X)) = CategoryTheory.CategoryStruct.id (functor✝.obj X) := by aesop_cat) : ({ functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso, functor_unitIso_comp := functor_unitIso_comp } = { functor := functor✝, inverse := inverse✝, unitIso := unitIso✝, counitIso := counitIso✝, functor_unitIso_comp := functor_unitIso_comp✝ }) = (functor = functor✝ ∧ inverse = inverse✝ ∧ HEq unitIso unitIso✝ ∧ HEq counitIso counitIso✝)
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.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.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.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.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_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.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

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 ?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.

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 19971e9 serving mathlib revision 40fea08