Whiskering

Given a functor F : C ⥤ D and functors G H : D ⥤ E and a natural transformation α : G ⟶ H, we can construct a new natural transformation F ⋙ G ⟶ F ⋙ H, called whiskerLeft F α. This is the same as the horizontal composition of 𝟙 F with α.

This operation is functorial in F, and we package this as whiskeringLeft. Here (whiskeringLeft.obj F).obj G is F ⋙ G, and (whiskeringLeft.obj F).map α is whiskerLeft F α. (That is, we might have alternatively named this as the "left composition functor".)

We also provide analogues for composition on the right, and for these operations on isomorphisms.

At the end of the file, we provide the left and right unitors, and the associator, for functor composition. (In fact functor composition is definitionally associative, but very often relying on this causes extremely slow elaboration, so it is better to insert it explicitly.) We also show these natural isomorphisms satisfy the triangle and pentagon identities.

@[elab_without_expected_type]

def CategoryTheory.whiskerLeft {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 H : CategoryTheory.Functor D E} (α : G ⟶ H) : F.comp G ⟶ F.comp H

If α : G ⟶ H then whiskerLeft F α : (F ⋙ G) ⟶ (F ⋙ H) has components α.app (F.obj X).

Equations

• CategoryTheory.whiskerLeft F α = { app := fun (X : C) => α.app (F.obj X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.whiskerLeft_app {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 H : CategoryTheory.Functor D E} (α : G ⟶ H) (X : C) : (CategoryTheory.whiskerLeft F α).app X = α.app (F.obj X)

@[elab_without_expected_type]

def CategoryTheory.whiskerRight {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) : G.comp F ⟶ H.comp F

If α : G ⟶ H then whisker_right α F : (G ⋙ F) ⟶ (G ⋙ F) has components F.map (α.app X).

Equations

• CategoryTheory.whiskerRight α F = { app := fun (X : C) => F.map (α.app X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.whiskerRight_app {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)

def CategoryTheory.whiskeringLeft (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor C E))

Left-composition gives a functor (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)).

(whiskeringLeft.obj F).obj G is F ⋙ G, and (whiskeringLeft.obj F).map α is whiskerLeft F α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.whiskeringLeft_obj_map (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 α

@[simp]

theorem CategoryTheory.whiskeringLeft_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) : ((CategoryTheory.whiskeringLeft C D E).obj F).obj G = F.comp G

@[simp]

theorem CategoryTheory.whiskeringLeft_map_app_app (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)

def CategoryTheory.whiskeringRight (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] : CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor C E))

Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)).

(whiskeringRight.obj H).obj F is F ⋙ H, and (whiskeringRight.obj H).map α is whiskerRight α H.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.whiskeringRight_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) (F : CategoryTheory.Functor C D) : ((CategoryTheory.whiskeringRight C D E).obj H).obj F = F.comp H

@[simp]

theorem CategoryTheory.whiskeringRight_map_app_app (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)

@[simp]

theorem CategoryTheory.whiskeringRight_obj_map (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

instance CategoryTheory.faithful_whiskeringRight_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] : ((CategoryTheory.whiskeringRight C D E).obj F).Faithful

def CategoryTheory.Functor.FullyFaithful.whiskeringRight {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : ((CategoryTheory.whiskeringRight C D E).obj F).FullyFaithful

If F : D ⥤ E is fully faithful, then so is (whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] {X✝ Y✝ : CategoryTheory.Functor C D} (f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝) (X : C) : ((hF.whiskeringRight C).preimage f).app X = hF.preimage (f.app X)

theorem CategoryTheory.whiskeringLeft_obj_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor C E)

def CategoryTheory.whiskeringLeftObjIdIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C E)

The isomorphism between left-whiskering on the identity functor and the identity of the functor between the resulting functor categories.

Equations

• CategoryTheory.whiskeringLeftObjIdIso = CategoryTheory.Iso.refl ((CategoryTheory.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C))

theorem CategoryTheory.whiskeringLeft_obj_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : (CategoryTheory.whiskeringLeft C D' E).obj (F.comp G) = ((CategoryTheory.whiskeringLeft D D' E).obj G).comp ((CategoryTheory.whiskeringLeft C D E).obj F)

def CategoryTheory.whiskeringLeftObjCompIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : (CategoryTheory.whiskeringLeft C D' E).obj (F.comp G) ≅ ((CategoryTheory.whiskeringLeft D D' E).obj G).comp ((CategoryTheory.whiskeringLeft C D E).obj F)

The isomorphism between left-whiskering on the composition of functors and the composition of two left-whiskering applications.

Equations

• CategoryTheory.whiskeringLeftObjCompIso F G = CategoryTheory.Iso.refl ((CategoryTheory.whiskeringLeft C D' E).obj (F.comp G))

theorem CategoryTheory.whiskeringRight_obj_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Functor E C)

def CategoryTheory.wiskeringRightObjIdIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] : (CategoryTheory.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor E C)

The isomorphism between right-whiskering on the identity functor and the identity of the functor between the resulting functor categories.

Equations

• CategoryTheory.wiskeringRightObjIdIso = CategoryTheory.Iso.refl ((CategoryTheory.whiskeringRight E C C).obj (CategoryTheory.Functor.id C))

theorem CategoryTheory.whiskeringRight_obj_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : ((CategoryTheory.whiskeringRight E C D).obj F).comp ((CategoryTheory.whiskeringRight E D D').obj G) = (CategoryTheory.whiskeringRight E C D').obj (F.comp G)

def CategoryTheory.whiskeringRightObjCompIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') : ((CategoryTheory.whiskeringRight E C D).obj F).comp ((CategoryTheory.whiskeringRight E D D').obj G) ≅ (CategoryTheory.whiskeringRight E C D').obj (F.comp G)

The isomorphism between right-whiskering on the composition of functors and the composition of two right-whiskering applications.

Equations

• CategoryTheory.whiskeringRightObjCompIso F G = CategoryTheory.Iso.refl (((CategoryTheory.whiskeringRight E C D).obj F).comp ((CategoryTheory.whiskeringRight E D D').obj G))

instance CategoryTheory.full_whiskeringRight_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [F.Faithful] [F.Full] : ((CategoryTheory.whiskeringRight C D E).obj F).Full

@[simp]

theorem CategoryTheory.whiskerLeft_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} : CategoryTheory.whiskerLeft F (CategoryTheory.NatTrans.id G) = CategoryTheory.NatTrans.id (F.comp G)

@[simp]

theorem CategoryTheory.whiskerLeft_id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} : CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (F.comp G)

@[simp]

theorem CategoryTheory.whiskerRight_id {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 : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E) : CategoryTheory.whiskerRight (CategoryTheory.NatTrans.id G) F = CategoryTheory.NatTrans.id (G.comp F)

@[simp]

theorem CategoryTheory.whiskerRight_id' {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 : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E) : CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.id G) F = CategoryTheory.CategoryStruct.id (G.comp F)

@[simp]

theorem CategoryTheory.whiskerLeft_comp {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 H K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K) : CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F α) (CategoryTheory.whiskerLeft F β)

theorem CategoryTheory.whiskerLeft_comp_assoc {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 H K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K) {Z : CategoryTheory.Functor C E} (h : F.comp K ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F β) h)

@[simp]

theorem CategoryTheory.whiskerRight_comp {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 K : CategoryTheory.Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : CategoryTheory.Functor D E) : CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α F) (CategoryTheory.whiskerRight β F)

theorem CategoryTheory.whiskerRight_comp_assoc {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 K : CategoryTheory.Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : CategoryTheory.Functor D E) {Z : CategoryTheory.Functor C E} (h : K.comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight β F) h)

def CategoryTheory.isoWhiskerLeft {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 H : CategoryTheory.Functor D E} (α : G ≅ H) : F.comp G ≅ F.comp H

If α : G ≅ H is a natural isomorphism then iso_whisker_left F α : (F ⋙ G) ≅ (F ⋙ H) has components α.app (F.obj X).

Equations

• CategoryTheory.isoWhiskerLeft F α = ((CategoryTheory.whiskeringLeft C D E).obj F).mapIso α

@[simp]

theorem CategoryTheory.isoWhiskerLeft_hom {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 H : CategoryTheory.Functor D E} (α : G ≅ H) : (CategoryTheory.isoWhiskerLeft F α).hom = CategoryTheory.whiskerLeft F α.hom

@[simp]

theorem CategoryTheory.isoWhiskerLeft_inv {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 H : CategoryTheory.Functor D E} (α : G ≅ H) : (CategoryTheory.isoWhiskerLeft F α).inv = CategoryTheory.whiskerLeft F α.inv

def CategoryTheory.isoWhiskerRight {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) : G.comp F ≅ H.comp F

If α : G ≅ H then iso_whisker_right α F : (G ⋙ F) ≅ (H ⋙ F) has components F.map_iso (α.app X).

Equations

• CategoryTheory.isoWhiskerRight α F = ((CategoryTheory.whiskeringRight C D E).obj F).mapIso α

@[simp]

theorem CategoryTheory.isoWhiskerRight_hom {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) : (CategoryTheory.isoWhiskerRight α F).hom = CategoryTheory.whiskerRight α.hom F

@[simp]

theorem CategoryTheory.isoWhiskerRight_inv {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) : (CategoryTheory.isoWhiskerRight α F).inv = CategoryTheory.whiskerRight α.inv F

instance CategoryTheory.isIso_whiskerLeft {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 H : CategoryTheory.Functor D E} (α : G ⟶ H) [CategoryTheory.IsIso α] : CategoryTheory.IsIso (CategoryTheory.whiskerLeft F α)

instance CategoryTheory.isIso_whiskerRight {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) [CategoryTheory.IsIso α] : CategoryTheory.IsIso (CategoryTheory.whiskerRight α F)

@[simp]

theorem CategoryTheory.whiskerLeft_twice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {H K : CategoryTheory.Functor D E} (α : H ⟶ K) : CategoryTheory.whiskerLeft F (CategoryTheory.whiskerLeft G α) = CategoryTheory.whiskerLeft (F.comp G) α

@[simp]

theorem CategoryTheory.whiskerRight_twice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (α : H ⟶ K) : CategoryTheory.whiskerRight (CategoryTheory.whiskerRight α F) G = CategoryTheory.whiskerRight α (F.comp G)

theorem CategoryTheory.whiskerRight_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D} (α : G ⟶ H) (K : CategoryTheory.Functor D E) : CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft F α) K = CategoryTheory.whiskerLeft F (CategoryTheory.whiskerRight α K)

def CategoryTheory.Functor.leftUnitor {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) : (CategoryTheory.Functor.id A).comp F ≅ F

The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.leftUnitor_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) : F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.leftUnitor_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) : F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.rightUnitor {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) : F.comp (CategoryTheory.Functor.id B) ≅ F

The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.rightUnitor_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) : F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Functor.rightUnitor_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) : F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Functor.associator {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) : (F.comp G).comp H ≅ F.comp (G.comp H)

The associator for functors, a natural isomorphism ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)).

(In fact, iso.refl _ will work here, but it tends to make Lean slow later, and it's usually best to insert explicit associators.)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.associator_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) (x✝ : A) : (F.associator G H).inv.app x✝ = CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x✝)

@[simp]

theorem CategoryTheory.Functor.associator_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) (x✝ : A) : (F.associator G H).hom.app x✝ = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x✝)

theorem CategoryTheory.Functor.assoc {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) : (F.comp G).comp H = F.comp (G.comp H)

theorem CategoryTheory.Functor.triangle {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) : CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom (CategoryTheory.whiskerLeft F G.leftUnitor.hom) = CategoryTheory.whiskerRight F.rightUnitor.hom G

theorem CategoryTheory.Functor.pentagon {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) (K : CategoryTheory.Functor D E) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (F.associator G H).hom K) (CategoryTheory.CategoryStruct.comp (F.associator (G.comp H) K).hom (CategoryTheory.whiskerLeft F (G.associator H K).hom)) = CategoryTheory.CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom

def CategoryTheory.whiskeringLeft₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} E] : CategoryTheory.Functor (CategoryTheory.Functor C₁ D₁) (CategoryTheory.Functor (CategoryTheory.Functor C₂ D₂) (CategoryTheory.Functor (CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))))

The obvious functor (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.whiskeringLeft₂_obj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} 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)

@[simp]

theorem CategoryTheory.whiskeringLeft₂_obj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} 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)

@[simp]

theorem CategoryTheory.whiskeringLeft₂_obj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} 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✝¹)

@[simp]

theorem CategoryTheory.whiskeringLeft₂_obj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} 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✝¹)

@[simp]

theorem CategoryTheory.whiskeringLeft₂_obj_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X✝ : C₁) (X✝ : C₂) : (((((CategoryTheory.whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).obj X✝ = (X.obj (F₁.obj X✝)).obj (F₂.obj X✝)

@[simp]

theorem CategoryTheory.whiskeringLeft₂_map_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_3} D₁] [CategoryTheory.Category.{u_9, u_4} D₂] (E : Type u_5) [CategoryTheory.Category.{u_10, u_5} 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✝¹)