class CategoryTheory.LeftModuleCategoryStruct' (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] : Type (max (max (max u₁ u₂) v₁) v₂)

A primed variant of LeftModuleCategoryStruct used in the development of the module functor formalism: it bundles the bifunctorial action data together with the associator and left unitor isomorphisms, without the coherence axioms.

• actObj : C → M → M
• actWhiskerLeft (X : C) {M₁ M₂ : M} (f : M₁ ⟶ M₂) : actObj X M₁ ⟶ actObj X M₂
• actWhiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (N : M) : actObj X₁ N ⟶ actObj X₂ N
• actTensorHom {X₁ X₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : M₁ ⟶ M₂) : actObj X₁ M₁ ⟶ actObj X₂ M₂
• actAssociator (X Y : C) (N : M) : actObj (MonoidalCategoryStruct.tensorObj X Y) N ≅ actObj X (actObj Y N)
• actLeftUnitor (N : M) : actObj (MonoidalCategoryStruct.tensorUnit C) N ≅ N

def CategoryTheory.ModFun.«term_⊗ᵐ_» : Lean.TrailingParserDescr

def CategoryTheory.ModFun.«term_◁ᵐ_» : Lean.TrailingParserDescr

def CategoryTheory.ModFun.«term_▷ᵐ_» : Lean.TrailingParserDescr

def CategoryTheory.ModFun.«term_⊗ₘᵐ_» : Lean.TrailingParserDescr

def CategoryTheory.ModFun.termActμ_ : Lean.ParserDescr

def CategoryTheory.ModFun.termActℓ_ : Lean.ParserDescr

class CategoryTheory.LeftModuleCategory' (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] extends CategoryTheory.LeftModuleCategoryStruct' C M : Type (max (max (max u₁ u₂) v₁) v₂)

A primed variant of LeftModuleCategory: extends LeftModuleCategoryStruct' with the full set of coherence axioms (bifunctoriality, pentagon, triangle and unitor naturality) for a left C-module category.

• actObj : C → M → M
• actWhiskerLeft (X : C) {M₁ M₂ : M} (f : M₁ ⟶ M₂) : actObj X M₁ ⟶ actObj X M₂
• actWhiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (N : M) : actObj X₁ N ⟶ actObj X₂ N
• actTensorHom {X₁ X₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : M₁ ⟶ M₂) : actObj X₁ M₁ ⟶ actObj X₂ M₂
• actAssociator (X Y : C) (N : M) : actObj (MonoidalCategoryStruct.tensorObj X Y) N ≅ actObj X (actObj Y N)
• actLeftUnitor (N : M) : actObj (MonoidalCategoryStruct.tensorUnit C) N ≅ N
• actTensorHom_def {X₁ X₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : M₁ ⟶ M₂) : LeftModuleCategoryStruct'.actTensorHom f g = CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f M₁) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ g)
• actId_tensorHom_id (X : C) (N : M) : LeftModuleCategoryStruct'.actTensorHom (CategoryStruct.id X) (CategoryStruct.id N) = CategoryStruct.id (LeftModuleCategoryStruct'.actObj X N)
• actTensorHom_comp {X₁ X₂ X₃ : C} {M₁ M₂ M₃ : M} (f₁ : X₁ ⟶ X₂) (g₁ : M₁ ⟶ M₂) (f₂ : X₂ ⟶ X₃) (g₂ : M₂ ⟶ M₃) : CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom f₁ g₁) (LeftModuleCategoryStruct'.actTensorHom f₂ g₂) = LeftModuleCategoryStruct'.actTensorHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)
• actWhiskerLeft_id (X : C) (N : M) : LeftModuleCategoryStruct'.actWhiskerLeft X (CategoryStruct.id N) = CategoryStruct.id (LeftModuleCategoryStruct'.actObj X N)
• actId_whiskerRight (X : C) (N : M) : LeftModuleCategoryStruct'.actWhiskerRight (CategoryStruct.id X) N = CategoryStruct.id (LeftModuleCategoryStruct'.actObj X N)
• actAssociator_naturality {X₁ X₂ Y₁ Y₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : M₁ ⟶ M₂) : CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom (MonoidalCategoryStruct.tensorHom f g) h) (LeftModuleCategoryStruct'.actAssociator X₂ Y₂ M₂).hom = CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X₁ Y₁ M₁).hom (LeftModuleCategoryStruct'.actTensorHom f (LeftModuleCategoryStruct'.actTensorHom g h))
• actLeftUnitor_naturality {M₁ M₂ : M} (f : M₁ ⟶ M₂) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft (MonoidalCategoryStruct.tensorUnit C) f) (LeftModuleCategoryStruct'.actLeftUnitor M₂).hom = CategoryStruct.comp (LeftModuleCategoryStruct'.actLeftUnitor M₁).hom f
• actPentagon (X Y Z : C) (N : M) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight (MonoidalCategoryStruct.associator X Y Z).hom N) (CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X (MonoidalCategoryStruct.tensorObj Y Z) N).hom (LeftModuleCategoryStruct'.actWhiskerLeft X (LeftModuleCategoryStruct'.actAssociator Y Z N).hom)) = CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator (MonoidalCategoryStruct.tensorObj X Y) Z N).hom (LeftModuleCategoryStruct'.actAssociator X Y (LeftModuleCategoryStruct'.actObj Z N)).hom
• actTriangle (X : C) (N : M) : CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X (MonoidalCategoryStruct.tensorUnit C) N).hom (LeftModuleCategoryStruct'.actWhiskerLeft X (LeftModuleCategoryStruct'.actLeftUnitor N).hom) = LeftModuleCategoryStruct'.actWhiskerRight (MonoidalCategoryStruct.rightUnitor X).hom N

theorem CategoryTheory.LeftModuleCategory'.actTensorHom_def_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] {X₁ X₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : M₁ ⟶ M₂) {Z : M} (h : LeftModuleCategoryStruct'.actObj X₂ M₂ ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom f g) h = CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f M₁) (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X₂ g) h)

theorem CategoryTheory.LeftModuleCategory'.actWhiskerLeft_id_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] (X : C) (N : M) {Z : M} (h : LeftModuleCategoryStruct'.actObj X N ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X (CategoryStruct.id N)) h = h

theorem CategoryTheory.LeftModuleCategory'.actId_whiskerRight_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] (X : C) (N : M) {Z : M} (h : LeftModuleCategoryStruct'.actObj X N ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight (CategoryStruct.id X) N) h = h

@[simp]

theorem CategoryTheory.LeftModuleCategory'.actTensorHom_comp_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] {X₁ X₂ X₃ : C} {M₁ M₂ M₃ : M} (f₁ : X₁ ⟶ X₂) (g₁ : M₁ ⟶ M₂) (f₂ : X₂ ⟶ X₃) (g₂ : M₂ ⟶ M₃) {Z : M} (h : LeftModuleCategoryStruct'.actObj X₃ M₃ ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom f₁ g₁) (CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom f₂ g₂) h) = CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom (CategoryStruct.comp f₁ f₂) (CategoryStruct.comp g₁ g₂)) h

theorem CategoryTheory.LeftModuleCategory'.actAssociator_naturality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] {X₁ X₂ Y₁ Y₂ : C} {M₁ M₂ : M} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : M₁ ⟶ M₂) {Z : M} (h✝ : LeftModuleCategoryStruct'.actObj X₂ (LeftModuleCategoryStruct'.actObj Y₂ M₂) ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X₂ Y₂ M₂).hom h✝) = CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X₁ Y₁ M₁).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actTensorHom f (LeftModuleCategoryStruct'.actTensorHom g h)) h✝)

theorem CategoryTheory.LeftModuleCategory'.actLeftUnitor_naturality_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] {M₁ M₂ : M} (f : M₁ ⟶ M₂) {Z : M} (h : M₂ ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft (MonoidalCategoryStruct.tensorUnit C) f) (CategoryStruct.comp (LeftModuleCategoryStruct'.actLeftUnitor M₂).hom h) = CategoryStruct.comp (LeftModuleCategoryStruct'.actLeftUnitor M₁).hom (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.LeftModuleCategory'.actPentagon_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] (X Y Z : C) (N : M) {Z✝ : M} (h : LeftModuleCategoryStruct'.actObj X (LeftModuleCategoryStruct'.actObj Y (LeftModuleCategoryStruct'.actObj Z N)) ⟶ Z✝) : CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight (MonoidalCategoryStruct.associator X Y Z).hom N) (CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X (MonoidalCategoryStruct.tensorObj Y Z) N).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X (LeftModuleCategoryStruct'.actAssociator Y Z N).hom) h)) = CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator (MonoidalCategoryStruct.tensorObj X Y) Z N).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X Y (LeftModuleCategoryStruct'.actObj Z N)).hom h)

@[simp]

theorem CategoryTheory.LeftModuleCategory'.actTriangle_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M : Type u₂} {inst✝² : Category.{v₂, u₂} M} [self : LeftModuleCategory' C M] (X : C) (N : M) {Z : M} (h : LeftModuleCategoryStruct'.actObj X N ⟶ Z) : CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X (MonoidalCategoryStruct.tensorUnit C) N).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X (LeftModuleCategoryStruct'.actLeftUnitor N).hom) h) = CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight (MonoidalCategoryStruct.rightUnitor X).hom N) h

structure CategoryTheory.ModuleFunctor' (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M₁ : Type u₂) [Category.{v₂, u₂} M₁] [LeftModuleCategory' C M₁] (M₂ : Type u₃) [Category.{v₃, u₃} M₂] [LeftModuleCategory' C M₂] : Type (max (max (max (max u₁ u₂) u₃) v₂) v₃)

A primed variant of ModuleFunctor between left C-module categories: an underlying functor together with a natural isomorphism F(X ⊗ N) ≅ X ⊗ F(N) satisfying compatibility with the associator and left unitor of the module structure.

• toFunctor : Functor M₁ M₂
• strIso (X : C) (N : M₁) : self.toFunctor.obj (LeftModuleCategoryStruct'.actObj X N) ≅ LeftModuleCategoryStruct'.actObj X (self.toFunctor.obj N)
• strIso_natural {X₁ X₂ : C} {N₁ N₂ : M₁} (f : X₁ ⟶ X₂) (g : N₁ ⟶ N₂) : CategoryStruct.comp (self.toFunctor.map (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f N₁) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ g))) (self.strIso X₂ N₂).hom = CategoryStruct.comp (self.strIso X₁ N₁).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f (self.toFunctor.obj N₁)) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ (self.toFunctor.map g)))
• strIso_assoc (X Y : C) (N : M₁) : CategoryStruct.comp (self.toFunctor.map (LeftModuleCategoryStruct'.actAssociator X Y N).hom) (CategoryStruct.comp (self.strIso X (LeftModuleCategoryStruct'.actObj Y N)).hom (LeftModuleCategoryStruct'.actWhiskerLeft X (self.strIso Y N).hom)) = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorObj X Y) N).hom (LeftModuleCategoryStruct'.actAssociator X Y (self.toFunctor.obj N)).hom
• strIso_unit (N : M₁) : self.toFunctor.map (LeftModuleCategoryStruct'.actLeftUnitor N).hom = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorUnit C) N).hom (LeftModuleCategoryStruct'.actLeftUnitor (self.toFunctor.obj N)).hom

theorem CategoryTheory.ModuleFunctor'.strIso_natural_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory' C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory' C M₂] (self : ModuleFunctor' C M₁ M₂) {X₁ X₂ : C} {N₁ N₂ : M₁} (f : X₁ ⟶ X₂) (g : N₁ ⟶ N₂) {Z : M₂} (h : LeftModuleCategoryStruct'.actObj X₂ (self.toFunctor.obj N₂) ⟶ Z) : CategoryStruct.comp (self.toFunctor.map (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f N₁) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ g))) (CategoryStruct.comp (self.strIso X₂ N₂).hom h) = CategoryStruct.comp (self.strIso X₁ N₁).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f (self.toFunctor.obj N₁)) (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X₂ (self.toFunctor.map g)) h))

@[simp]

theorem CategoryTheory.ModuleFunctor'.strIso_assoc_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory' C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory' C M₂] (self : ModuleFunctor' C M₁ M₂) (X Y : C) (N : M₁) {Z : M₂} (h : LeftModuleCategoryStruct'.actObj X (LeftModuleCategoryStruct'.actObj Y (self.toFunctor.obj N)) ⟶ Z) : CategoryStruct.comp (self.toFunctor.map (LeftModuleCategoryStruct'.actAssociator X Y N).hom) (CategoryStruct.comp (self.strIso X (LeftModuleCategoryStruct'.actObj Y N)).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerLeft X (self.strIso Y N).hom) h)) = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorObj X Y) N).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actAssociator X Y (self.toFunctor.obj N)).hom h)

@[simp]

theorem CategoryTheory.ModuleFunctor'.strIso_unit_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] [LeftModuleCategory' C M₁] {M₂ : Type u₃} [Category.{v₃, u₃} M₂] [LeftModuleCategory' C M₂] (self : ModuleFunctor' C M₁ M₂) (N : M₁) {Z : M₂} (h : self.toFunctor.obj N ⟶ Z) : CategoryStruct.comp (self.toFunctor.map (LeftModuleCategoryStruct'.actLeftUnitor N).hom) h = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorUnit C) N).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actLeftUnitor (self.toFunctor.obj N)).hom h)

structure CategoryTheory.ModuleEquivalence' (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M₁ : Type u₂) [Category.{v₂, u₂} M₁] [LeftModuleCategory' C M₁] (M₂ : Type u₃) [Category.{v₃, u₃} M₂] [LeftModuleCategory' C M₂] extends CategoryTheory.ModuleFunctor' C M₁ M₂ : Type (max (max (max (max u₁ u₂) u₃) v₂) v₃)

A primed variant of ModuleEquivalence: a ModuleFunctor' whose underlying functor is an equivalence of categories, giving an equivalence of left C-module categories.

• toFunctor : Functor M₁ M₂
• strIso (X : C) (N : M₁) : self.toFunctor.obj (LeftModuleCategoryStruct'.actObj X N) ≅ LeftModuleCategoryStruct'.actObj X (self.toFunctor.obj N)
• strIso_natural {X₁ X₂ : C} {N₁ N₂ : M₁} (f : X₁ ⟶ X₂) (g : N₁ ⟶ N₂) : CategoryStruct.comp (self.toFunctor.map (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f N₁) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ g))) (self.strIso X₂ N₂).hom = CategoryStruct.comp (self.strIso X₁ N₁).hom (CategoryStruct.comp (LeftModuleCategoryStruct'.actWhiskerRight f (self.toFunctor.obj N₁)) (LeftModuleCategoryStruct'.actWhiskerLeft X₂ (self.toFunctor.map g)))
• strIso_assoc (X Y : C) (N : M₁) : CategoryStruct.comp (self.toFunctor.map (LeftModuleCategoryStruct'.actAssociator X Y N).hom) (CategoryStruct.comp (self.strIso X (LeftModuleCategoryStruct'.actObj Y N)).hom (LeftModuleCategoryStruct'.actWhiskerLeft X (self.strIso Y N).hom)) = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorObj X Y) N).hom (LeftModuleCategoryStruct'.actAssociator X Y (self.toFunctor.obj N)).hom
• strIso_unit (N : M₁) : self.toFunctor.map (LeftModuleCategoryStruct'.actLeftUnitor N).hom = CategoryStruct.comp (self.strIso (MonoidalCategoryStruct.tensorUnit C) N).hom (LeftModuleCategoryStruct'.actLeftUnitor (self.toFunctor.obj N)).hom
• isEquivalence : self.toFunctor.IsEquivalence