Functors that are linear with respect to an action

Given a monoidal category C acting on the left or on the right on categories D and D', we introduce the following typeclasses on functors F : D ⥤ D' to express compatibility of F with the action of C:

• F.LaxLeftLinear C bundles the "lineator" as a morphism μₗ : c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d).
• F.LaxRightLinear C bundles the "lineator" as a morphism μᵣ : F.obj d ⊙ᵣ c ⟶ F.obj (d ⊙ᵣ c).
• F.OplaxLeftLinear C bundles the "lineator" as a morphism δₗ : F.obj (c ⊙ₗ d) ⟶ c ⊙ₗ F.obj d .
• F.OplaxRightLinear C bundles the "lineator" as a morphism δᵣ : F.obj (d ⊙ᵣ d) ⟶ F.obj d ⊙ᵣ c.
• F.LeftLinear C expresses that F has both a LaxLeftLinear C and an F.OplaxLeftLinear C structure, and that they are compatible, i.e δₗ F is a left and right inverse to μₗ.
• F.RightLinear C expresses that F has both a LaxRightLinear C and an F.OplaxRightLinear C structure, and that they are compatible, i.e δᵣ F is a left and right inverse to μᵣ.

class CategoryTheory.Functor.LaxLeftLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] : Type (max (max u_1 u_3) u_5)

F.LaxLinear C equips F : D ⥤ D' with a family of morphisms μₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d) that is natural in each variable and coherent with respect to left actions of C on D and D'.

• μₗ (c : C) (d : D) : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶ F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)

  The "μₗ" morphism.

• μₗ_naturality_left {c c' : C} (f : c ⟶ c') (d : D) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)) (μₗ F c' d) = CategoryStruct.comp (μₗ F c d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
• μₗ_naturality_right (c : C) {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)) (μₗ F c d') = CategoryStruct.comp (μₗ F c d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
• μₗ_associativity (c c' : C) (d : D) : CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorObj c c') d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (μₗ F c' d)) (μₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)))
• μₗ_unitality (d : D) : (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom = CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorUnit C) d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c : C) {d d' : D} (f : d ⟶ d') {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d') ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)) (CategoryStruct.comp (μₗ F c d') h) = CategoryStruct.comp (μₗ F c d) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)) h)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] {c c' : C} (f : c ⟶ c') (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)) (CategoryStruct.comp (μₗ F c' d) h) = CategoryStruct.comp (μₗ F c d) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)) h)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c c' : C) (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) ⟶ Z) : CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorObj c c') d) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (μₗ F c' d)) (CategoryStruct.comp (μₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) h))

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (d : D) {Z : D'} (h : F.obj d ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom h = CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorUnit C) d) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom) h)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LaxLeftLinear C] (c c' : C) (d : D) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (μₗ F c' d)) (CategoryStruct.comp (μₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv)) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv (μₗ F (MonoidalCategoryStruct.tensorObj c c') d)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LaxLeftLinear C] (c c' : C) (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj (MonoidalCategoryStruct.tensorObj c c') d) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (μₗ F c' d)) (CategoryStruct.comp (μₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv) h)) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv (CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorObj c c') d) h)

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LaxLeftLinear C] (d : D) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv (μₗ F (MonoidalCategoryStruct.tensorUnit C) d) = F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv

@[simp]

theorem CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LaxLeftLinear C] (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj (MonoidalCategoryStruct.tensorUnit C) d) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv (CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorUnit C) d) h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv) h

class CategoryTheory.Functor.OplaxLeftLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] : Type (max (max u_1 u_3) u_5)

F.OplaxLinear C equips F : D ⥤ D' with a family of morphisms δₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d) that is natural in each variable and coherent with respect to left actions of C on D and D'.

• δₗ (c : C) (d : D) : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶ MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d)

  The oplax lineator morphism morphism.

• δₗ_naturality_left {c c' : C} (f : c ⟶ c') (d : D) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)) (δₗ F c' d) = CategoryStruct.comp (δₗ F c d) (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
• δₗ_naturality_right (c : C) {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)) (δₗ F c d') = CategoryStruct.comp (δₗ F c d) (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
• δₗ_associativity (c c' : C) (d : D) : CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorObj c c') d) (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) (CategoryStruct.comp (δₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (δₗ F c' d)))
• δₗ_unitality_inv (d : D) : (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv) (δₗ F (MonoidalCategoryStruct.tensorUnit C) d)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c : C) {d d' : D} (f : d ⟶ d') {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d') ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)) (CategoryStruct.comp (δₗ F c d') h) = CategoryStruct.comp (δₗ F c d) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)) h)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] {c c' : C} (f : c ⟶ c') (d : D) {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj c' (F.obj d) ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)) (CategoryStruct.comp (δₗ F c' d) h) = CategoryStruct.comp (δₗ F c d) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)) h)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (c c' : C) (d : D) {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' (F.obj d)) ⟶ Z) : CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorObj c c') d) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) (CategoryStruct.comp (δₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (δₗ F c' d)) h))

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] (d : D) {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj (MonoidalCategoryStruct.tensorUnit C) (F.obj d) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv h = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv) (CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorUnit C) d) h)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.OplaxLeftLinear C] (c c' : C) (d : D) : CategoryStruct.comp (δₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (δₗ F c' d)) (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv) (δₗ F (MonoidalCategoryStruct.tensorObj c c') d)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.OplaxLeftLinear C] (c c' : C) (d : D) {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj (MonoidalCategoryStruct.tensorObj c c') (F.obj d) ⟶ Z) : CategoryStruct.comp (δₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (δₗ F c' d)) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv h)) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv) (CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorObj c c') d) h)

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.OplaxLeftLinear C] (d : D) : CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorUnit C) d) (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom = F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom

@[simp]

theorem CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.OplaxLeftLinear C] (d : D) {Z : D'} (h : F.obj d ⟶ Z) : CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorUnit C) d) (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom) h

class CategoryTheory.Functor.LeftLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] extends F.LaxLeftLinear C, F.OplaxLeftLinear C : Type (max (max u_1 u_3) u_5)

F.LeftLinear C asserts that F is both lax and oplax left-linear, in a compatible way, i.e that μₗ is inverse to δₗ.

• μₗ (c : C) (d : D) : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶ F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
• μₗ_naturality_left {c c' : C} (f : c ⟶ c') (d : D) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)) (μₗ F c' d) = CategoryStruct.comp (μₗ F c d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
• μₗ_naturality_right (c : C) {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)) (μₗ F c d') = CategoryStruct.comp (μₗ F c d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
• μₗ_associativity (c c' : C) (d : D) : CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorObj c c') d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (μₗ F c' d)) (μₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)))
• μₗ_unitality (d : D) : (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom = CategoryStruct.comp (μₗ F (MonoidalCategoryStruct.tensorUnit C) d) (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom)
• δₗ (c : C) (d : D) : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶ MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d)
• δₗ_naturality_left {c c' : C} (f : c ⟶ c') (d : D) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)) (δₗ F c' d) = CategoryStruct.comp (δₗ F c d) (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
• δₗ_naturality_right (c : C) {d d' : D} (f : d ⟶ d') : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)) (δₗ F c d') = CategoryStruct.comp (δₗ F c d) (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
• δₗ_associativity (c c' : C) (d : D) : CategoryStruct.comp (δₗ F (MonoidalCategoryStruct.tensorObj c c') d) (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).hom = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom) (CategoryStruct.comp (δₗ F c (MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d)) (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (δₗ F c' d)))
• δₗ_unitality_inv (d : D) : (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).inv = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv) (δₗ F (MonoidalCategoryStruct.tensorUnit C) d)
• μₗ_comp_δₗ (c : C) (d : D) : CategoryStruct.comp (LaxLeftLinear.μₗ F c d) (OplaxLeftLinear.δₗ F c d) = CategoryStruct.id (MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d))
• δₗ_comp_μₗ (c : C) (d : D) : CategoryStruct.comp (OplaxLeftLinear.δₗ F c d) (LaxLeftLinear.μₗ F c d) = CategoryStruct.id (F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))

@[simp]

theorem CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D) {Z : D'} (h : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶ Z) : CategoryStruct.comp (LaxLeftLinear.μₗ F c d) (CategoryStruct.comp (OplaxLeftLinear.δₗ F c d) h) = h

@[simp]

theorem CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalLeftAction C D} {inst✝⁵ : MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶ Z) : CategoryStruct.comp (OplaxLeftLinear.δₗ F c d) (CategoryStruct.comp (LaxLeftLinear.μₗ F c d) h) = h

@[reducible, inline]

abbrev CategoryTheory.Functor.LeftLinear.μₗIso {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LeftLinear C] (c : C) (d : D) : MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ≅ F.obj (MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)

A shorthand to bundle the μₗ as an isomorphism

Equations

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

instance CategoryTheory.Functor.LeftLinear.instIsIsoμₗ {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LeftLinear C] (c : C) (d : D) : IsIso (LaxLeftLinear.μₗ F c d)

instance CategoryTheory.Functor.LeftLinear.instIsIsoδₗ {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LeftLinear C] (c : C) (d : D) : IsIso (OplaxLeftLinear.δₗ F c d)

@[simp]

theorem CategoryTheory.Functor.LeftLinear.inv_μₗ {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LeftLinear C] (c : C) (d : D) : CategoryTheory.inv (LaxLeftLinear.μₗ F c d) = OplaxLeftLinear.δₗ F c d

@[simp]

theorem CategoryTheory.Functor.LeftLinear.inv_δₗ {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalLeftAction C D] [MonoidalCategory.MonoidalLeftAction C D'] [F.LeftLinear C] (c : C) (d : D) : CategoryTheory.inv (OplaxLeftLinear.δₗ F c d) = LaxLeftLinear.μₗ F c d

class CategoryTheory.Functor.LaxRightLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] : Type (max (max u_1 u_3) u_5)

F.LaxLinear C equips F : D ⥤ D' with a family of morphisms μₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d) that is natural in each variable and coherent with respect to left actions of C on D and D'.

• μᵣ (d : D) (c : C) : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶ F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c)

  The "μᵣ" morphism.

• μᵣ_naturality_right (d : D) {c c' : C} (f : c ⟶ c') : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f) (μᵣ F d c') = CategoryStruct.comp (μᵣ F d c) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f))
• μᵣ_naturality_left {d d' : D} (f : d ⟶ d') (c : C) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c) (μᵣ F d' c) = CategoryStruct.comp (μᵣ F d c) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c))
• μᵣ_associativity (d : D) (c c' : C) : CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) = CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ F d c) c') (μᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c'))
• μᵣ_unitality (d : D) : (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom = CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom)

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) {c c' : C} (f : c ⟶ c') {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c') ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f) (CategoryStruct.comp (μᵣ F d c') h) = CategoryStruct.comp (μᵣ F d c) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)) h)

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] {d d' : D} (f : d ⟶ d') (c : C) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d' c) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c) (CategoryStruct.comp (μᵣ F d' c) h) = CategoryStruct.comp (μᵣ F d c) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)) h)

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) (c c' : C) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') ⟶ Z) : CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) h) = CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ F d c) c') (CategoryStruct.comp (μᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') h))

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) {Z : D'} (h : F.obj d ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom h = CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom) h)

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.LaxRightLinear C] (d : D) (c c' : C) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ F d c) c') (CategoryStruct.comp (μᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv)) = CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv (μᵣ F d (MonoidalCategoryStruct.tensorObj c c'))

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.LaxRightLinear C] (d : D) (c c' : C) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d (MonoidalCategoryStruct.tensorObj c c')) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ F d c) c') (CategoryStruct.comp (μᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv) h)) = CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv (CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorObj c c')) h)

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.LaxRightLinear C] (d : D) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv (μᵣ F d (MonoidalCategoryStruct.tensorUnit C)) = F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv

@[simp]

theorem CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.LaxRightLinear C] (d : D) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv (CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorUnit C)) h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv) h

class CategoryTheory.Functor.OplaxRightLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] : Type (max (max u_1 u_3) u_5)

F.OplaxLinear C equips F : D ⥤ D' with a family of morphisms δₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d) that is natural in each variable and coherent with respect to left actions of C on D and D'.

• δᵣ (d : D) (c : C) : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) ⟶ MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c

  The oplax lineator morphism morphism.

• δᵣ_naturality_right (d : D) {c c' : C} (f : c ⟶ c') : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)) (δᵣ F d c') = CategoryStruct.comp (δᵣ F d c) (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
• δᵣ_naturality_left {d d' : D} (f : d ⟶ d') (c : C) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)) (δᵣ F d' c) = CategoryStruct.comp (δᵣ F d c) (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
• δᵣ_associativity (d : D) (c c' : C) : CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) (CategoryStruct.comp (δᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (δᵣ F d c) c'))
• δᵣ_unitality_inv (d : D) : (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv) (δᵣ F d (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) {c c' : C} (f : c ⟶ c') {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c' ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)) (CategoryStruct.comp (δᵣ F d c') h) = CategoryStruct.comp (δᵣ F d c) (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f) h)

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] {d d' : D} (f : d ⟶ d') (c : C) {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d') c ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)) (CategoryStruct.comp (δᵣ F d' c) h) = CategoryStruct.comp (δᵣ F d c) (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c) h)

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) (c c' : C) {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c) c' ⟶ Z) : CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) (CategoryStruct.comp (δᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (δᵣ F d c) c') h))

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv h = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv) (CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorUnit C)) h)

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.OplaxRightLinear C] (d : D) (c c' : C) : CategoryStruct.comp (δᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (δᵣ F d c) c') (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv) (δᵣ F d (MonoidalCategoryStruct.tensorObj c c'))

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.OplaxRightLinear C] (d : D) (c c' : C) {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) (MonoidalCategoryStruct.tensorObj c c') ⟶ Z) : CategoryStruct.comp (δᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (δᵣ F d c) c') (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv h)) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv) (CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorObj c c')) h)

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.OplaxRightLinear C] (d : D) : CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom = F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom

@[simp]

theorem CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom_assoc {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.OplaxRightLinear C] (d : D) {Z : D'} (h : F.obj d ⟶ Z) : CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom h) = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom) h

class CategoryTheory.Functor.RightLinear {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') (C : Type u_3) [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] extends F.LaxRightLinear C, F.OplaxRightLinear C : Type (max (max u_1 u_3) u_5)

F.RightLinear C asserts that F is both lax and oplax left-linear, in a compatible way, i.e that μᵣ is inverse to δᵣ.

• μᵣ (d : D) (c : C) : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶ F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
• μᵣ_naturality_right (d : D) {c c' : C} (f : c ⟶ c') : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f) (μᵣ F d c') = CategoryStruct.comp (μᵣ F d c) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f))
• μᵣ_naturality_left {d d' : D} (f : d ⟶ d') (c : C) : CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c) (μᵣ F d' c) = CategoryStruct.comp (μᵣ F d c) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c))
• μᵣ_associativity (d : D) (c c' : C) : CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) = CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom (CategoryStruct.comp (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ F d c) c') (μᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c'))
• μᵣ_unitality (d : D) : (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom = CategoryStruct.comp (μᵣ F d (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom)
• δᵣ (d : D) (c : C) : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) ⟶ MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c
• δᵣ_naturality_right (d : D) {c c' : C} (f : c ⟶ c') : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)) (δᵣ F d c') = CategoryStruct.comp (δᵣ F d c) (MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
• δᵣ_naturality_left {d d' : D} (f : d ⟶ d') (c : C) : CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)) (δᵣ F d' c) = CategoryStruct.comp (δᵣ F d c) (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
• δᵣ_associativity (d : D) (c c' : C) : CategoryStruct.comp (δᵣ F d (MonoidalCategoryStruct.tensorObj c c')) (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) (CategoryStruct.comp (δᵣ F (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') (MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (δᵣ F d c) c'))
• δᵣ_unitality_inv (d : D) : (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv = CategoryStruct.comp (F.map (MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv) (δᵣ F d (MonoidalCategoryStruct.tensorUnit C))
• μᵣ_comp_δᵣ (d : D) (c : C) : CategoryStruct.comp (LaxRightLinear.μᵣ F d c) (OplaxRightLinear.δᵣ F d c) = CategoryStruct.id (MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c)
• δᵣ_comp_μᵣ (d : D) (c : C) : CategoryStruct.comp (OplaxRightLinear.δᵣ F d c) (LaxRightLinear.μᵣ F d c) = CategoryStruct.id (F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c))

@[simp]

theorem CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C) {Z : D'} (h : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶ Z) : CategoryStruct.comp (LaxRightLinear.μᵣ F d c) (CategoryStruct.comp (OplaxRightLinear.δᵣ F d c) h) = h

@[simp]

theorem CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc {D : Type u_1} {D' : Type u_2} {inst✝ : Category.{u_4, u_1} D} {inst✝¹ : Category.{u_5, u_2} D'} (F : Functor D D') {C : Type u_3} {inst✝² : Category.{u_6, u_3} C} {inst✝³ : MonoidalCategory C} {inst✝⁴ : MonoidalCategory.MonoidalRightAction C D} {inst✝⁵ : MonoidalCategory.MonoidalRightAction C D'} [self : F.RightLinear C] (d : D) (c : C) {Z : D'} (h : F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c) ⟶ Z) : CategoryStruct.comp (OplaxRightLinear.δᵣ F d c) (CategoryStruct.comp (LaxRightLinear.μᵣ F d c) h) = h

@[reducible, inline]

abbrev CategoryTheory.Functor.RightLinear.μᵣIso {D : Type u_1} {D' : Type u_2} [Category.{u_4, u_1} D] [Category.{u_5, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.RightLinear C] (d : D) (c : C) : MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ≅ F.obj (MonoidalCategory.MonoidalRightActionStruct.actionObj d c)

A shorthand to bundle the μᵣ as an isomorphism

Equations

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

instance CategoryTheory.Functor.RightLinear.instIsIsoμᵣ {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.RightLinear C] (c : C) (d : D) : IsIso (LaxRightLinear.μᵣ F d c)

instance CategoryTheory.Functor.RightLinear.instIsIsoδᵣ {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.RightLinear C] (c : C) (d : D) : IsIso (OplaxRightLinear.δᵣ F d c)

@[simp]

theorem CategoryTheory.Functor.RightLinear.inv_μᵣ {D : Type u_1} {D' : Type u_2} [Category.{u_5, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_6, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.RightLinear C] (c : C) (d : D) : CategoryTheory.inv (LaxRightLinear.μᵣ F d c) = OplaxRightLinear.δᵣ F d c

@[simp]

theorem CategoryTheory.Functor.RightLinear.inv_δᵣ {D : Type u_1} {D' : Type u_2} [Category.{u_6, u_1} D] [Category.{u_4, u_2} D'] (F : Functor D D') {C : Type u_3} [Category.{u_5, u_3} C] [MonoidalCategory C] [MonoidalCategory.MonoidalRightAction C D] [MonoidalCategory.MonoidalRightAction C D'] [F.RightLinear C] (c : C) (d : D) : CategoryTheory.inv (OplaxRightLinear.δᵣ F d c) = LaxRightLinear.μᵣ F d c