structure CategoryTheory.Definition_2_9_5 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] (M : C) : Type v

Definition 2.9.5 (EGNO): A right module structure on M : C over an algebra object A consists of an action morphism act : M ⊗ A ⟶ M that is associative with respect to the multiplication of A and unital with respect to the unit of A.

• act : MonoidalCategoryStruct.tensorObj M A ⟶ M
• act_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.act A) self.act = CategoryStruct.comp (MonoidalCategoryStruct.associator M A A).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M MonObj.mul) self.act)
• act_unit : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M MonObj.one) self.act = (MonoidalCategoryStruct.rightUnitor M).hom

@[simp]

theorem CategoryTheory.Definition_2_9_5.act_unit_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M : C} (self : Definition_2_9_5 A M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M MonObj.one) (CategoryStruct.comp self.act h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor M).hom h

@[simp]

theorem CategoryTheory.Definition_2_9_5.act_assoc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M : C} (self : Definition_2_9_5 A M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.act A) (CategoryStruct.comp self.act h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M A A).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M MonObj.mul) (CategoryStruct.comp self.act h))

def CategoryTheory.IsAModuleHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ : C} (p₁ : Definition_2_9_5 A M₁) (p₂ : Definition_2_9_5 A M₂) (l : M₁ ⟶ M₂) : Prop

The predicate that a morphism l : M₁ ⟶ M₂ commutes with the right A-module actions on M₁ and M₂, i.e. p₁.act ≫ l = (l ▷ A) ≫ p₂.act.

structure CategoryTheory.AModuleHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ : C} (p₁ : Definition_2_9_5 A M₁) (p₂ : Definition_2_9_5 A M₂) : Type v

A bundled module hom between two A-modules (M₁, p₁) and (M₂, p₂): a morphism hom : M₁ ⟶ M₂ together with the commutativity condition with the actions.

• hom : M₁ ⟶ M₂
• comm : CategoryStruct.comp p₁.act self.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.hom A) p₂.act

theorem CategoryTheory.AModuleHom.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : MonoidalCategory C} {A : C} {inst✝² : MonObj A} {M₁ M₂ : C} {p₁ : Definition_2_9_5 A M₁} {p₂ : Definition_2_9_5 A M₂} {x y : AModuleHom p₁ p₂} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.AModuleHom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : MonoidalCategory C} {A : C} {inst✝² : MonObj A} {M₁ M₂ : C} {p₁ : Definition_2_9_5 A M₁} {p₂ : Definition_2_9_5 A M₂} {x y : AModuleHom p₁ p₂} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.AModuleHom.comm_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ : C} {p₁ : Definition_2_9_5 A M₁} {p₂ : Definition_2_9_5 A M₂} (self : AModuleHom p₁ p₂) {Z : C} (h : M₂ ⟶ Z) : CategoryStruct.comp p₁.act (CategoryStruct.comp self.hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.hom A) (CategoryStruct.comp p₂.act h)

@[reducible, inline]

abbrev CategoryTheory.Definition_2_9_6 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ : C} (p₁ : Definition_2_9_5 A M₁) (p₂ : Definition_2_9_5 A M₂) : Type v

Alias for AModuleHom matching the textbook numbering of Definition 2.9.6 (morphisms of right A-modules) in EGNO.

def CategoryTheory.AModuleHom.id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ : C} (p : Definition_2_9_5 A M₁) : AModuleHom p p

The identity module hom on an A-module (M₁, p), given by the identity morphism.

@[simp]

theorem CategoryTheory.AModuleHom.id_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ : C} (p : Definition_2_9_5 A M₁) : (id p).hom = CategoryStruct.id M₁

def CategoryTheory.AModuleHom.comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ M₃ : C} {p₁ : Definition_2_9_5 A M₁} {p₂ : Definition_2_9_5 A M₂} {p₃ : Definition_2_9_5 A M₃} (f : AModuleHom p₁ p₂) (g : AModuleHom p₂ p₃) : AModuleHom p₁ p₃

Composition of module homs: the underlying morphisms are composed and the compatibility square with the actions is verified.

@[simp]

theorem CategoryTheory.AModuleHom.comp_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M₁ M₂ M₃ : C} {p₁ : Definition_2_9_5 A M₁} {p₂ : Definition_2_9_5 A M₂} {p₃ : Definition_2_9_5 A M₃} (f : AModuleHom p₁ p₂) (g : AModuleHom p₂ p₃) : (f.comp g).hom = CategoryStruct.comp f.hom g.hom

@[reducible, inline]

abbrev CategoryTheory.Definition_2_9_6_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] {M N : C} [ModObj A M] [ModObj A N] (f : M ⟶ N) : Prop

Alias for IsMod_Hom matching the textbook numbering of Definition 2.9.6 in the left-module setting, expressed via Mathlib's ModObj typeclass.