Theorems · Inductive type · category theory

CategoryTheory.MonoidalCategory.MonoidalLeftAction

(C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory C] → Type (max (max (max u_1 u_2) v_1) v_2)

A MonoidalLeftAction C D is the data of: - For every object c : C and d : D, an object c ⊙ₗ d of D. - For every morphism f : (c : C) ⟶ c' and every d : D, a morphism f ⊵ₗ d : c ⊙ₗ d ⟶ c' ⊙ₗ d. - For every morphism f : (d : D) ⟶ d' and every c : C, a morphism c ⊴ₗ f : c ⊙ₗ d ⟶ c ⊙ₗ d'. - For every pair of morphisms f : (c : C) ⟶ c' and f : (d : D) ⟶ d', a morphism f ⊙ₗ f' : c ⊙ₗ d ⟶ c' ⊙ₗ d'. - A structure isomorphism αₗ c c' d : c ⊗ c' ⊙ₗ d ≅ c ⊙ₗ c' ⊙ₗ d. - A structure isomorphism λₗ d : (𝟙_ C) ⊙ₗ d ≅ d. Furthermore, we require identities that turn - ⊙ₗ - into a bifunctor, ensure naturality of αₗ and λₗ, and ensure compatibilities with the associator and unitor isomorphisms in C.

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Cited by

215 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory