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

The data of a right A-module structure on an object M : C: a right action act : M ⊗ A → M compatible with the unit and multiplication of the algebra A.

• act : MonoidalCategoryStruct.tensorObj M A ⟶ M
• act_unit : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M MonObj.one) self.act = (MonoidalCategoryStruct.rightUnitor M).hom
• 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)

@[simp]

theorem CategoryTheory.RightModObj.act_unit_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M : C} (self : RightModObj 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.RightModObj.act_assoc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M : C} (self : RightModObj 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))

@[reducible, inline]

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

A right module over an algebra (A, m, u) is a pair (M, p) with M : C and p : M ⊗ A → M satisfying the unit and associativity axioms.

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

A right module over the algebra A packaged as a bundled structure: an underlying object X : C together with a right action mod : RightModObj A X.

• X : C
• mod : RightModObj A self.X

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

A morphism l : M₁ → M₂ between right A-modules (M₁, p₁) and (M₂, p₂) is an A-module homomorphism if it intertwines the right actions.

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

A morphism in the category of right A-modules: an underlying morphism hom in C that intertwines the right A-actions on the source and target.

• hom : M.X ⟶ N.X
• comm : CategoryStruct.comp M.mod.act self.hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.hom A) N.mod.act

theorem CategoryTheory.RightMod_.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : MonoidalCategory C} {A : C} {inst✝² : MonObj A} {M N : RightMod_ A} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.RightMod_.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : MonoidalCategory C} {A : C} {inst✝² : MonObj A} {M N : RightMod_ A} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

@[simp]

theorem CategoryTheory.RightMod_.Hom.comm_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N : RightMod_ A} (self : M.Hom N) {Z : C} (h : N.X ⟶ Z) : CategoryStruct.comp M.mod.act (CategoryStruct.comp self.hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.hom A) (CategoryStruct.comp N.mod.act h)

def CategoryTheory.RightMod_.id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M : RightMod_ A) : M.Hom M

The identity morphism on a right A-module M.

@[simp]

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

def CategoryTheory.RightMod_.comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N K : RightMod_ A} (f : M.Hom N) (g : N.Hom K) : M.Hom K

Composition of two right A-module morphisms.

@[simp]

theorem CategoryTheory.RightMod_.comp_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N K : RightMod_ A} (f : M.Hom N) (g : N.Hom K) : (comp f g).hom = CategoryStruct.comp f.hom g.hom

@[implicit_reducible]

instance CategoryTheory.RightMod_.instCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] : Category.{v, max u v} (RightMod_ A)

The category structure on right A-modules, with morphisms RightMod_.Hom, identities and composition as defined above.

theorem CategoryTheory.RightMod_.hom_ext {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N : RightMod_ A} (f₁ f₂ : M ⟶ N) (h : f₁.hom = f₂.hom) : f₁ = f₂

Two morphisms of right A-modules are equal iff their underlying morphisms in C are equal.

theorem CategoryTheory.RightMod_.hom_ext_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N : RightMod_ A} {f₁ f₂ : M ⟶ N} : f₁ = f₂ ↔ f₁.hom = f₂.hom

@[simp]

theorem CategoryTheory.RightMod_.id_hom' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M : RightMod_ A) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

The underlying morphism of the identity in RightMod_ A is the identity in C.

@[simp]

theorem CategoryTheory.RightMod_.comp_hom' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {M N K : RightMod_ A} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

The underlying morphism of a composition f ≫ g of right A-module morphisms is the composition of the underlying morphisms.

def CategoryTheory.RightMod_.regular {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] : RightMod_ A

The right regular A-module, namely the algebra A viewed as a right module over itself via its multiplication.

@[simp]

theorem CategoryTheory.RightMod_.regular_mod_act {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] : (regular A).mod.act = MonObj.mul

@[simp]

theorem CategoryTheory.RightMod_.regular_X {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] : (regular A).X = A

def CategoryTheory.RightMod_.forget {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] : Functor (RightMod_ A) C

The forgetful functor from right A-modules to C, sending a module to its underlying object.

@[simp]

theorem CategoryTheory.RightMod_.forget_obj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M : RightMod_ A) : forget.obj M = M.X

@[simp]

theorem CategoryTheory.RightMod_.forget_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {X✝ Y✝ : RightMod_ A} (f : X✝ ⟶ Y✝) : forget.map f = f.hom

def CategoryTheory.RightMod_.tensorModObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X : C) (M : RightMod_ A) : RightModObj A (MonoidalCategoryStruct.tensorObj X M.X)

For X : C and a right A-module M, the object X ⊗ M.X carries a right A-module structure with action (α_).hom ≫ X ◁ M.mod.act.

def CategoryTheory.RightMod_.actWhiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (M : RightMod_ A) : { X := MonoidalCategoryStruct.tensorObj X₁ M.X, mod := tensorModObj X₁ M } ⟶ { X := MonoidalCategoryStruct.tensorObj X₂ M.X, mod := tensorModObj X₂ M }

Right whiskering of f : X₁ ⟶ X₂ by a right A-module M, viewed as a morphism in RightMod_ A between the modules X₁ ⊗ M and X₂ ⊗ M.

def CategoryTheory.RightMod_.actWhiskerLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X : C) {M N : RightMod_ A} (g : M ⟶ N) : { X := MonoidalCategoryStruct.tensorObj X M.X, mod := tensorModObj X M } ⟶ { X := MonoidalCategoryStruct.tensorObj X N.X, mod := tensorModObj X N }

Left whiskering of a right A-module morphism g : M ⟶ N by an object X : C, giving a morphism X ⊗ M ⟶ X ⊗ N in RightMod_ A.

def CategoryTheory.RightMod_.actAssociator {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X Y : C) (M : RightMod_ A) : { X := MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) M.X, mod := tensorModObj (MonoidalCategoryStruct.tensorObj X Y) M } ≅ { X := MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y M.X), mod := tensorModObj X { X := MonoidalCategoryStruct.tensorObj Y M.X, mod := tensorModObj Y M } }

The associator isomorphism (X ⊗ Y) ⊗ M ≅ X ⊗ (Y ⊗ M) in RightMod_ A for the C-action on right A-modules.

def CategoryTheory.RightMod_.actLeftUnitor {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (M : RightMod_ A) : { X := MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) M.X, mod := tensorModObj (MonoidalCategoryStruct.tensorUnit C) M } ≅ M

The left unitor isomorphism 𝟙_ C ⊗ M ≅ M in RightMod_ A for the C-action.

def CategoryTheory.RightMod_.actTensorHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] {X₁ X₂ : C} {M₁ M₂ : RightMod_ A} (f : X₁ ⟶ X₂) (g : M₁ ⟶ M₂) : { X := MonoidalCategoryStruct.tensorObj X₁ M₁.X, mod := tensorModObj X₁ M₁ } ⟶ { X := MonoidalCategoryStruct.tensorObj X₂ M₂.X, mod := tensorModObj X₂ M₂ }

The tensor of a morphism f : X₁ ⟶ X₂ in C with a morphism g : M₁ ⟶ M₂ of right A-modules, giving a morphism X₁ ⊗ M₁ ⟶ X₂ ⊗ M₂ in RightMod_ A.

@[implicit_reducible]

instance CategoryTheory.RightMod_.actLeftModuleCategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] : LeftModuleCategory C (RightMod_ A)

The category RightMod_ A of right A-modules carries a canonical structure of a left C-module category, with action (X, M) ↦ X ⊗ M and the natural associativity and unit constraints.

def CategoryTheory.RightMod_.Proposition_2_9_10 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] : LeftModuleCategory C (RightMod_ A)

Proposition 2.9.10: the category Mod_C(A) together with the functor ⊗̃ and the associativity and unit constraints ã, l̃ is a left module category over C.

noncomputable def CategoryTheory.RightMod_.Lemma_2_9_12 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X : C) (M : RightMod_ A) : { X := MonoidalCategoryStruct.tensorObj X A, mod := tensorModObj X (regular A) }.Hom M ≃ (X ⟶ M.X)

Lemma 2.9.12: for any X ∈ C, the canonical isomorphism Hom_A(X ⊗ A, M) ≃ Hom(X, M) exhibits · ⊗ A as left adjoint to the forgetful functor.

def CategoryTheory.MoritaEquivalent {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [MonObj A] [MonObj B] : Prop

Two algebras A and B in C are Morita equivalent if there is a module equivalence between their categories of right modules RightMod_ A and RightMod_ B.

noncomputable def CategoryTheory.TensorOverAlgebra {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasCoequalizers C] {A M N : C} (actR : MonoidalCategoryStruct.tensorObj M A ⟶ M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : C

Tensor product over an algebra A: for a right A-module (M, actR) and a left A-module (N, actL), the object M ⊗_A N is the coequalizer of the two natural maps M ⊗ A ⊗ N ⇒ M ⊗ N.

noncomputable def CategoryTheory.TensorOverAlgebra.π {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasCoequalizers C] {A M N : C} (actR : MonoidalCategoryStruct.tensorObj M A ⟶ M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : MonoidalCategoryStruct.tensorObj M N ⟶ TensorOverAlgebra actR actL

The canonical projection M ⊗ N ⟶ M ⊗_A N exhibiting M ⊗_A N as the coequalizer.