The category of R-modules

Module.{v} R is the category of bundled R-modules with carrier in the universe v. We show that it is preadditive and show that being an isomorphism, monomorphism and epimorphism is equivalent to being a linear equivalence, an injective linear map and a surjective linear map, respectively.

Implementation details

To construct an object in the category of R-modules from a type M with an instance of the Module typeclass, write of R M. There is a coercion in the other direction.

Similarly, there is a coercion from morphisms in Module R to linear maps.

Porting note: the next two paragraphs should be revised.

Unfortunately, Lean is not smart enough to see that, given an object M : Module R, the expression of R M, where we coerce M to the carrier type, is definitionally equal to M itself. This means that to go the other direction, i.e., from linear maps/equivalences to (iso)morphisms in the category of R-modules, we have to take care not to inadvertently end up with an of R M where M is already an object. Hence, given f : M →ₗ[R] N,

• if M N : Module R, simply use f;
• if M : Module R and N is an unbundled R-module, use ↿f or asHomLeft f;
• if M is an unbundled R-module and N : Module R, use ↾f or asHomRight f;
• if M and N are unbundled R-modules, use ↟f or asHom f.

Similarly, given f : M ≃ₗ[R] N, use toModuleIso, toModuleIso'Left, toModuleIso'Right or toModuleIso', respectively.

The arrow notations are localized, so you may have to open ModuleCat (or open scoped ModuleCat) to use them. Note that the notation for asHomLeft clashes with the notation used to promote functions between types to morphisms in the category Type, so to avoid confusion, it is probably a good idea to avoid having the locales Module and CategoryTheory.Type open at the same time.

If you get an error when trying to apply a theorem and the convert tactic produces goals of the form M = of R M, then you probably used an incorrect variant of asHom or toModuleIso.

structure ModuleCat (R : Type u) [Ring R] : Type (max u (v + 1))

The category of R-modules and their morphisms.

Note that in the case of R = ℤ, we can not impose here that the ℤ-multiplication field from the module structure is defeq to the one coming from the isAddCommGroup structure (contrary to what we do for all module structures in mathlib), which creates some difficulties down the road.

• carrier : Type v

  the underlying type of an object in ModuleCat R

• isAddCommGroup : AddCommGroup ↑self
• isModule : Module R ↑self

@[inline, reducible]

abbrev ModuleCatMax (R : Type u₁) [Ring R] : Type (max u₁ ((max v₁ v₂) + 1))

An alias for ModuleCat.{max u₁ u₂}, to deal around unification issues. Since the universe the ring lives in can be inferred, we put that last.

Equations

• ModuleCatMax R = ModuleCat R

instance ModuleCat.instCoeSortModuleCatType (R : Type u) [Ring R] : CoeSort (ModuleCat R) (Type v)

Equations

• ModuleCat.instCoeSortModuleCatType R = { coe := ModuleCat.carrier }

instance ModuleCat.moduleCategory (R : Type u) [Ring R] : CategoryTheory.Category.{v, max (v + 1) u} (ModuleCat R)

Equations

• ModuleCat.moduleCategory R = CategoryTheory.Category.mk

instance ModuleCat.instFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrier (R : Type u) [Ring R] {M : ModuleCat R} {N : ModuleCat R} : FunLike (M ⟶ N) ↑M ↑N

Equations

• ModuleCat.instFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrier R = LinearMap.instFunLike

instance ModuleCat.instLinearMapClassHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierToSemiringToAddCommMonoidIsAddCommGroupIsModuleInstFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrier (R : Type u) [Ring R] {M : ModuleCat R} {N : ModuleCat R} : LinearMapClass (M ⟶ N) R ↑M ↑N

Equations

• (_ : LinearMapClass (M ⟶ N) R ↑M ↑N) = (_ : SemilinearMapClass (↑M →ₗ[R] ↑N) (RingHom.id R) ↑M ↑N)

instance ModuleCat.moduleConcreteCategory (R : Type u) [Ring R] : CategoryTheory.ConcreteCategory (ModuleCat R)

Equations

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

instance ModuleCat.instAddCommGroupObjModuleCatToQuiverToCategoryStructModuleCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetModuleConcreteCategory (R : Type u) [Ring R] {M : ModuleCat R} : AddCommGroup ((CategoryTheory.forget (ModuleCat R)).toPrefunctor.obj M)

Equations

• ModuleCat.instAddCommGroupObjModuleCatToQuiverToCategoryStructModuleCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetModuleConcreteCategory R = inferInstance

instance ModuleCat.instModuleObjModuleCatToQuiverToCategoryStructModuleCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetModuleConcreteCategoryToSemiringToAddCommMonoidInstAddCommGroupObjModuleCatToQuiverToCategoryStructModuleCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetModuleConcreteCategory (R : Type u) [Ring R] {M : ModuleCat R} : Module R ((CategoryTheory.forget (ModuleCat R)).toPrefunctor.obj M)

Equations

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

theorem ModuleCat.ext (R : Type u) [Ring R] {M : ModuleCat R} {N : ModuleCat R} {f₁ : M ⟶ N} {f₂ : M ⟶ N} (h : ∀ (x : ↑M), f₁ x = f₂ x) : f₁ = f₂

instance ModuleCat.hasForgetToAddCommGroup (R : Type u) [Ring R] : CategoryTheory.HasForget₂ (ModuleCat R) AddCommGroupCat

Equations

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

def ModuleCat.of (R : Type u) [Ring R] (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat R

The object in the category of R-modules associated to an R-module

Equations

• ModuleCat.of R X = ModuleCat.mk X

@[simp]

theorem ModuleCat.forget₂_obj (R : Type u) [Ring R] (X : ModuleCat R) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj X = AddCommGroupCat.of ↑X

theorem ModuleCat.forget₂_obj_moduleCat_of (R : Type u) [Ring R] (X : Type v) [AddCommGroup X] [Module R X] : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj (ModuleCat.of R X) = AddCommGroupCat.of X

@[simp]

theorem ModuleCat.forget₂_map (R : Type u) [Ring R] (X : ModuleCat R) (Y : ModuleCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.map f = LinearMap.toAddMonoidHom f

def ModuleCat.ofHom {R : Type u} [Ring R] {X : Type v} {Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) : ModuleCat.of R X ⟶ ModuleCat.of R Y

Typecheck a LinearMap as a morphism in Module R.

Equations

• ModuleCat.ofHom f = f

@[simp]

theorem ModuleCat.ofHom_apply {R : Type u} [Ring R] {X : Type v} {Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) (x : X) : (ModuleCat.ofHom f) x = f x

instance ModuleCat.instInhabitedModuleCat (R : Type u) [Ring R] : Inhabited (ModuleCat R)

Equations

• ModuleCat.instInhabitedModuleCat R = { default := ModuleCat.of R PUnit.{u_1 + 1} }

instance ModuleCat.ofUnique (R : Type u) [Ring R] {X : Type v} [AddCommGroup X] [Module R X] [i : Unique X] : Unique ↑(ModuleCat.of R X)

Equations

• ModuleCat.ofUnique R = i

theorem ModuleCat.coe_of (R : Type u) [Ring R] (X : Type v) [AddCommGroup X] [Module R X] : ↑(ModuleCat.of R X) = X

@[simp]

theorem ModuleCat.ofSelfIso_inv {R : Type u} [Ring R] (M : ModuleCat R) : (ModuleCat.ofSelfIso M).inv = CategoryTheory.CategoryStruct.id M

@[simp]

theorem ModuleCat.ofSelfIso_hom {R : Type u} [Ring R] (M : ModuleCat R) : (ModuleCat.ofSelfIso M).hom = CategoryTheory.CategoryStruct.id M

def ModuleCat.ofSelfIso {R : Type u} [Ring R] (M : ModuleCat R) : ModuleCat.of R ↑M ≅ M

Forgetting to the underlying type and then building the bundled object returns the original module.

Equations

• ModuleCat.ofSelfIso M = CategoryTheory.Iso.mk (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id M)

theorem ModuleCat.isZero_of_subsingleton {R : Type u} [Ring R] (M : ModuleCat R) [Subsingleton ↑M] : CategoryTheory.Limits.IsZero M

instance ModuleCat.instHasZeroObjectModuleCatModuleCategory {R : Type u} [Ring R] : CategoryTheory.Limits.HasZeroObject (ModuleCat R)

Equations

• (_ : CategoryTheory.Limits.HasZeroObject (ModuleCat R)) = (_ : CategoryTheory.Limits.HasZeroObject (ModuleCat R))

@[simp]

theorem ModuleCat.id_apply {R : Type u} [Ring R] {M : ModuleCat R} (m : ↑M) : (CategoryTheory.CategoryStruct.id M) m = m

@[simp]

theorem ModuleCat.coe_comp {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} {U : ModuleCat R} (f : M ⟶ N) (g : N ⟶ U) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

theorem ModuleCat.comp_def {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} {U : ModuleCat R} (f : M ⟶ N) (g : N ⟶ U) : CategoryTheory.CategoryStruct.comp f g = g ∘ₗ f

@[simp]

theorem ModuleCat.forget_map {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) : (CategoryTheory.forget (ModuleCat R)).toPrefunctor.map f = ⇑f

def ModuleCat.asHom {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] : (X₁ →ₗ[R] X₂) → (ModuleCat.of R X₁ ⟶ ModuleCat.of R X₂)

Reinterpreting a linear map in the category of R-modules.

Equations

• ModuleCat.asHom = id

def ModuleCat.«term↟_» : Lean.ParserDescr

Reinterpreting a linear map in the category of R-modules

Equations

• ModuleCat.«term↟_» = Lean.ParserDescr.node `ModuleCat.term↟_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↟") (Lean.ParserDescr.cat `term 1024))

def ModuleCat.asHomRight {R : Type u} [Ring R] {X₁ : Type v} [AddCommGroup X₁] [Module R X₁] {X₂ : ModuleCat R} : (X₁ →ₗ[R] ↑X₂) → (ModuleCat.of R X₁ ⟶ X₂)

Reinterpreting a linear map in the category of R-modules.

Equations

• ModuleCat.asHomRight = id

def ModuleCat.«term↾_» : Lean.ParserDescr

Reinterpreting a linear map in the category of R-modules.

Equations

• ModuleCat.«term↾_» = Lean.ParserDescr.node `ModuleCat.term↾_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 1024))

def ModuleCat.asHomLeft {R : Type u} [Ring R] {X₂ : Type v} {X₁ : ModuleCat R} [AddCommGroup X₂] [Module R X₂] : (↑X₁ →ₗ[R] X₂) → (X₁ ⟶ ModuleCat.of R X₂)

Reinterpreting a linear map in the category of R-modules.

Equations

• ModuleCat.asHomLeft = id

def ModuleCat.«term↿_» : Lean.ParserDescr

Reinterpreting a linear map in the category of R-modules.

Equations

• ModuleCat.«term↿_» = Lean.ParserDescr.node `ModuleCat.term↿_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem LinearEquiv.toModuleIso_inv {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : (LinearEquiv.toModuleIso e).inv = ↑(LinearEquiv.symm e)

@[simp]

theorem LinearEquiv.toModuleIso_hom {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : (LinearEquiv.toModuleIso e).hom = ↑e

def LinearEquiv.toModuleIso {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : ModuleCat.of R X₁ ≅ ModuleCat.of R X₂

Build an isomorphism in the category Module R from a LinearEquiv between Modules.

Equations

• LinearEquiv.toModuleIso e = CategoryTheory.Iso.mk ↑e ↑(LinearEquiv.symm e)

@[inline, reducible]

abbrev LinearEquiv.toModuleIso' {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (i : ↑M ≃ₗ[R] ↑N) : M ≅ N

Build an isomorphism in the category Module R from a LinearEquiv between Modules.

Equations

• LinearEquiv.toModuleIso' i = LinearEquiv.toModuleIso i

@[inline, reducible]

abbrev LinearEquiv.toModuleIso'Left {R : Type u} [Ring R] {X₂ : Type v} {X₁ : ModuleCat R} [AddCommGroup X₂] [Module R X₂] (e : ↑X₁ ≃ₗ[R] X₂) : X₁ ≅ ModuleCat.of R X₂

Build an isomorphism in the category Module R from a linear_equiv between modules.

Equations

• LinearEquiv.toModuleIso'Left e = LinearEquiv.toModuleIso e

@[inline, reducible]

abbrev LinearEquiv.toModuleIso'Right {R : Type u} [Ring R] {X₁ : Type v} [AddCommGroup X₁] [Module R X₁] {X₂ : ModuleCat R} (e : X₁ ≃ₗ[R] ↑X₂) : ModuleCat.of R X₁ ≅ X₂

Build an isomorphism in the category Module R from a linear_equiv between modules.

Equations

• LinearEquiv.toModuleIso'Right e = LinearEquiv.toModuleIso e

def CategoryTheory.Iso.toLinearEquiv {R : Type u} [Ring R] {X : ModuleCat R} {Y : ModuleCat R} (i : X ≅ Y) : ↑X ≃ₗ[R] ↑Y

Build a linear_equiv from an isomorphism in the category Module R.

Equations

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

@[simp]

theorem linearEquivIsoModuleIso_hom {R : Type u} [Ring R] {X : Type u} {Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] (e : X ≃ₗ[R] Y) : linearEquivIsoModuleIso.hom e = LinearEquiv.toModuleIso e

@[simp]

theorem linearEquivIsoModuleIso_inv {R : Type u} [Ring R] {X : Type u} {Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] (i : ModuleCat.of R X ≅ ModuleCat.of R Y) : linearEquivIsoModuleIso.inv i = CategoryTheory.Iso.toLinearEquiv i

def linearEquivIsoModuleIso {R : Type u} [Ring R] {X : Type u} {Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] : (X ≃ₗ[R] Y) ≅ ModuleCat.of R X ≅ ModuleCat.of R Y

linear equivalences between modules are the same as (isomorphic to) isomorphisms in Module

Equations

• linearEquivIsoModuleIso = CategoryTheory.Iso.mk (fun (e : X ≃ₗ[R] Y) => LinearEquiv.toModuleIso e) fun (i : ModuleCat.of R X ≅ ModuleCat.of R Y) => CategoryTheory.Iso.toLinearEquiv i

instance ModuleCat.instAddCommGroupHomModuleCatToQuiverToCategoryStructModuleCategory {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} : AddCommGroup (M ⟶ N)

Equations

• ModuleCat.instAddCommGroupHomModuleCatToQuiverToCategoryStructModuleCategory = LinearMap.addCommGroup

instance ModuleCat.instPreadditiveModuleCatModuleCategory {R : Type u} [Ring R] : CategoryTheory.Preadditive (ModuleCat R)

Equations

• ModuleCat.instPreadditiveModuleCatModuleCategory = CategoryTheory.Preadditive.mk

instance ModuleCat.forget₂_addCommGroupCat_additive {R : Type u} [Ring R] : CategoryTheory.Functor.Additive (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)

Equations

• (_ : CategoryTheory.Functor.Additive (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)) = (_ : CategoryTheory.Functor.Additive (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat))

instance ModuleCat.instLinearToSemiringToCommSemiringModuleCatToRingModuleCategoryInstPreadditiveModuleCatModuleCategory {S : Type u} [CommRing S] : CategoryTheory.Linear S (ModuleCat S)

Equations

• ModuleCat.instLinearToSemiringToCommSemiringModuleCatToRingModuleCategoryInstPreadditiveModuleCatModuleCategory = CategoryTheory.Linear.mk

theorem ModuleCat.Iso.homCongr_eq_arrowCongr {S : Type u} [CommRing S] {X : ModuleCat S} {Y : ModuleCat S} {X' : ModuleCat S} {Y' : ModuleCat S} (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) : (CategoryTheory.Iso.homCongr i j) f = (LinearEquiv.arrowCongr (CategoryTheory.Iso.toLinearEquiv i) (CategoryTheory.Iso.toLinearEquiv j)) f

theorem ModuleCat.Iso.conj_eq_conj {S : Type u} [CommRing S] {X : ModuleCat S} {X' : ModuleCat S} (i : X ≅ X') (f : CategoryTheory.End X) : (CategoryTheory.Iso.conj i) f = (LinearEquiv.conj (CategoryTheory.Iso.toLinearEquiv i)) f

def ModuleCat.smul {R : Type u} [Ring R] (M : ModuleCat R) : R →+* CategoryTheory.End ((CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj M)

The scalar multiplication on an object of ModuleCat R considered as a morphism of rings from R to the endomorphisms of the underlying abelian group.

Equations

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

theorem ModuleCat.smul_naturality {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (f : M ⟶ N) (r : R) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.map f) ((ModuleCat.smul N) r) = CategoryTheory.CategoryStruct.comp ((ModuleCat.smul M) r) ((CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.map f)

@[simp]

theorem ModuleCat.smulNatTrans_apply_app (R : Type u) [Ring R] (r : R) (M : ModuleCat R) : ((ModuleCat.smulNatTrans R) r).app M = (ModuleCat.smul M) r

def ModuleCat.smulNatTrans (R : Type u) [Ring R] : R →+* CategoryTheory.End (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat)

The scalar multiplication on ModuleCat R considered as a morphism of rings to the endomorphisms of the forgetful functor to AddCommGroupCat).

Equations

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

def ModuleCat.mkOfSMul' {R : Type u} [Ring R] {A : AddCommGroupCat} : (R →+* CategoryTheory.End A) → AddCommGroupCat

Given A : AddCommGroupCat and a ring morphism R →+* End A, this is a type synonym for A, on which we shall define a structure of R-module.

Equations

• ModuleCat.mkOfSMul' x = A

instance ModuleCat.instAddCommGroupαMkOfSMul' {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) : AddCommGroup ↑(ModuleCat.mkOfSMul' φ)

Equations

• ModuleCat.instAddCommGroupαMkOfSMul' φ = id inferInstance

instance ModuleCat.instSMulαAddCommGroupMkOfSMul' {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) : SMul R ↑(ModuleCat.mkOfSMul' φ)

Equations

• ModuleCat.instSMulαAddCommGroupMkOfSMul' φ = { smul := fun (r : R) (x : ↑A) => (let_fun this := φ r; this) x }

@[simp]

theorem ModuleCat.mkOfSMul'_smul {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) (r : R) (x : ↑(ModuleCat.mkOfSMul' φ)) : r • x = (let_fun this := φ r; this) x

instance ModuleCat.instModuleαAddCommGroupMkOfSMul'ToSemiringToAddCommMonoidInstAddCommGroupαMkOfSMul' {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) : Module R ↑(ModuleCat.mkOfSMul' φ)

Equations

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

@[inline, reducible]

abbrev ModuleCat.mkOfSMul {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) : ModuleCat R

Given A : AddCommGroupCat and a ring morphism R →+* End A, this is an object in ModuleCat R, whose underlying abelian group is A and whose scalar multiplication is given by R.

Equations

• ModuleCat.mkOfSMul φ = ModuleCat.of R ↑(ModuleCat.mkOfSMul' φ)

@[simp]

theorem ModuleCat.mkOfSMul_smul {R : Type u} [Ring R] {A : AddCommGroupCat} (φ : R →+* CategoryTheory.End A) (r : R) : (ModuleCat.smul (ModuleCat.mkOfSMul φ)) r = φ r

@[simp]

theorem ModuleCat.homMk_apply {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ ((ModuleCat.smul N) r) = CategoryTheory.CategoryStruct.comp ((ModuleCat.smul M) r) φ) (a : ↑((CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj M)) : (ModuleCat.homMk φ hφ) a = φ a

def ModuleCat.homMk {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ ((ModuleCat.smul N) r) = CategoryTheory.CategoryStruct.comp ((ModuleCat.smul M) r) φ) : M ⟶ N

Constructor for morphisms in ModuleCat R which takes as inputs a morphism between the underlying objects in AddCommGroupCat and the compatibility with the scalar multiplication.

Equations

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

theorem ModuleCat.forget₂_map_homMk {R : Type u} [Ring R] {M : ModuleCat R} {N : ModuleCat R} (φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.obj N) (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ ((ModuleCat.smul N) r) = CategoryTheory.CategoryStruct.comp ((ModuleCat.smul M) r) φ) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGroupCat).toPrefunctor.map (ModuleCat.homMk φ hφ) = φ