Mathlib.CategoryTheory.Monoidal.Mod

source

class Mod_Class {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (M : C) [Mon_Class M] (X : D) :

Type v₂

Given an action of a monoidal category C on a category D, an action of a monoid object M in C on an object X in D is the data of a map smul : M ⊙ₗ X ⟶ X that satisfies unitality and associativity with multiplication.

See MulAction for the non-categorical version.

smul : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X
The action map
one_smul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
The identity acts trivially.
mul_smul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.mul X) smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul)
The action map is compatible with multiplication.

Instances

source

theorem Mod_Class.one_smul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : Mon_Class M} (X : D) [self : Mod_Class M X] {Z : D} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h

source

theorem Mod_Class.mul_smul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : Mon_Class M} (X : D) [self : Mod_Class M X] {Z : D} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.mul X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) (CategoryTheory.CategoryStruct.comp smul h))

source

def Mon_Class.termγ :

Lean.ParserDescr

The action map

Equations

Mon_Class.termγ = Lean.ParserDescr.node `Mon_Class.termγ 1024 (Lean.ParserDescr.symbol "γ")

Instances For

source

def Mon_Class.«termγ[_]» :

Lean.ParserDescr

The action map

Equations

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

Instances For

source

def Mon_Class.«termγ[_,_]» :

Lean.ParserDescr

The action map

Equations

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

Instances For

source

@[simp]

theorem Mod_Class.one_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [Mon_Class M] (X : D) [Mod_Class M X] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

source

@[simp]

theorem Mod_Class.one_smul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [Mon_Class M] (X : D) [Mod_Class M X] {Z : D} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h

source

@[reducible, inline]

abbrev Mod_Class.regular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (M : C) [Mon_Class M] :

Mod_Class M M

The action of a monoid object on itself.

Equations

Mod_Class.regular M = { smul := Mon_Class.mul, one_smul' := ⋯, mul_smul' := ⋯ }

Instances For

source

instance Mod_Class.instTensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : D) :

Mod_Class (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X

If C acts monoidally on D, then every object of D is canonically a module over the trivial monoid.

Equations

Mod_Class.instTensorUnit X = { smul := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, one_smul' := ⋯, mul_smul' := ⋯ }

source

@[simp]

theorem Mod_Class.smul_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : D) :

smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

source

theorem Mod_Class.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Mon_Class M] {X : C} (h₁ h₂ : Mod_Class M X) (H : smul = smul) :

h₁ = h₂

source

theorem Mod_Class.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : C} [Mon_Class M] {X : C} {h₁ h₂ : Mod_Class M X} :

h₁ = h₂ ↔ smul = smul

source

class IsMod_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class A N] (f : M ⟶ N) :

Prop

A morphism in D is a morphism of A-module objects if it commutes with the action maps

smul_hom : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul

Instances

source

@[simp]

theorem IsMod_Hom.smul_hom_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : Mon_Class A} {M N : D} {inst✝⁵ : Mod_Class A M} {inst✝⁶ : Mod_Class A N} {f : M ⟶ N} [self : IsMod_Hom A f] {Z : D} (h : N ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mod_Class.smul (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) (CategoryTheory.CategoryStruct.comp Mod_Class.smul h)

source

instance instIsMod_HomId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M : D} [Mod_Class A M] :

IsMod_Hom A (CategoryTheory.CategoryStruct.id M)

source

instance instIsMod_HomComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N O : D} [Mod_Class A M] [Mod_Class A N] [Mod_Class A O] (f : M ⟶ N) (g : N ⟶ O) [IsMod_Hom A f] [IsMod_Hom A g] :

IsMod_Hom A (CategoryTheory.CategoryStruct.comp f g)

source

instance instIsMod_HomInvOfHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class A N] (f : M ≅ N) [IsMod_Hom A f.hom] :

IsMod_Hom A f.inv

source

structure Mod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] :

Type (max u₂ v₂)

A module object for a monoid object in a monoidal category acting on the ambient category.

X : D
The underlying object in the ambient category
mod : Mod_Class A self.X

Instances For

source

structure Mod_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] (M N : Mod_ D A) :

Type v₂

A morphism of module objects.

hom : M.X ⟶ N.X
The underlying morphism
isMod_Hom : IsMod_Hom A self.hom

Instances For

source

theorem Mod_.Hom.ext_iff {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : Mon_Class A} {M N : Mod_ D A} {x y : M.Hom N} :

x = y ↔ x.hom = y.hom

source

theorem Mod_.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst✝² : CategoryTheory.Category.{v₂, u₂} D} {inst✝³ : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : Mon_Class A} {M N : Mod_ D A} {x y : M.Hom N} (hom : x.hom = y.hom) :

x = y

source

def Mod_.Hom.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N : Mod_ D A} (f : M.X ⟶ N.X) (smul_hom : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul := by aesop_cat) :

M.Hom N

An alternative constructor for Hom, taking a morphism without a [isMod_Hom] instance, as well as the relevant equality to put such an instance.

Equations

Mod_.Hom.mk' f smul_hom = { hom := f, isMod_Hom := ⋯ }

Instances For

source

@[simp]

theorem Mod_.Hom.mk'_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N : Mod_ D A} (f : M.X ⟶ N.X) (smul_hom : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul := by aesop_cat) :

(mk' f smul_hom).hom = f

source

def Mod_.Hom.mk'' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class A N] (f : M ⟶ N) (smul_hom : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul := by aesop_cat) :

{ X := M, mod := inst✝ }.Hom { X := N, mod := inst✝¹ }

An alternative constructor for Hom, taking a morphism without a [isMod_Hom] instance, between objects with a Mod_Class instance (rather than bundled as Mod_), as well as the relevant equality to put such an instance.

Equations

Mod_.Hom.mk'' f smul_hom = { hom := f, isMod_Hom := ⋯ }

Instances For

source

@[simp]

theorem Mod_.Hom.mk''_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class A N] (f : M ⟶ N) (smul_hom : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul := by aesop_cat) :

(mk'' f smul_hom).hom = f

source

def Mod_.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] (M : Mod_ D A) :

M.Hom M

The identity morphism on a module object.

Equations

M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isMod_Hom := ⋯ }

Instances For

source

@[simp]

theorem Mod_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] (M : Mod_ D A) :

M.id.hom = CategoryTheory.CategoryStruct.id M.X

source

instance Mod_.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] (M : Mod_ D A) :

Inhabited (M.Hom M)

Equations

M.homInhabited = { default := M.id }

source

def Mod_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N O : Mod_ D A} (f : M.Hom N) (g : N.Hom O) :

M.Hom O

Composition of module object morphisms.

Equations

Mod_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isMod_Hom := ⋯ }

Instances For

source

@[simp]

theorem Mod_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N O : Mod_ D A} (f : M.Hom N) (g : N.Hom O) :

(comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

source

instance Mod_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] :

CategoryTheory.Category.{v₂, max u₂ v₂} (Mod_ D A)

Equations

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

source

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

f₁ = f₂

source

theorem Mod_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N : Mod_ D A} {f₁ f₂ : M ⟶ N} :

f₁ = f₂ ↔ f₁.hom = f₂.hom

source

@[simp]

theorem Mod_.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] (M : Mod_ D A) :

(CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

source

@[simp]

theorem Mod_.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A : C} [Mon_Class A] {M N K : Mod_ D A} (f : M ⟶ N) (g : N ⟶ K) :

(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

source

def Mod_.regular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [Mon_Class A] :

Mod_ C A

A monoid object as a module over itself.

Equations

Mod_.regular A = { X := A, mod := Mod_Class.regular A }

Instances For

source

@[simp]

theorem Mod_.regular_mod_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [Mon_Class A] :

Mod_Class.smul = Mon_Class.mul

source

@[simp]

theorem Mod_.regular_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [Mon_Class A] :

(regular A).X = A

source

instance Mod_.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [Mon_Class A] :

Inhabited (Mod_ C A)

Equations

Mod_.instInhabited A = { default := Mod_.regular A }

source

def Mod_.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] :

CategoryTheory.Functor (Mod_ D A) D

The forgetful functor from module objects to the ambient category.

Equations

Mod_.forget A = { obj := fun (A_1 : Mod_ D A) => A_1.X, map := fun {X Y : Mod_ D A} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem Mod_.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {X✝ Y✝ : Mod_ D A} (f : X✝ ⟶ Y✝) :

(forget A).map f = f.hom

source

@[simp]

theorem Mod_.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] (A✝ : Mod_ D A) :

(forget A).obj A✝ = A✝.X

source

def Mod_.scalarRestriction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M : D) [Mod_Class B M] :

Mod_Class A M

When M is a B-module in D and f : A ⟶ B is a morphism of internal monoid objects, M inherits an A-module structure via "restriction of scalars", i.e γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M].

Equations

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

Instances For

source

@[simp]

theorem Mod_.scalarRestriction_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M : D) [Mod_Class B M] :

Mod_Class.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M) Mod_Class.smul

source

theorem Mod_.scalarRestriction_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M N : D) [Mod_Class B M] [Mod_Class B N] (g : M ⟶ N) [IsMod_Hom B g] :

IsMod_Hom A g

If g : M ⟶ N is a B-linear morphisms of B-modules, then it induces an A-linear morphism when M and N have an A-module structure obtained by restricting scalars along a monoid morphism A ⟶ B.

source