The category of R-modules

ModuleCat.{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. The roundtrip ↑(of R M) is definitionally equal to M itself (when M is a type with Module instance), and so is of R ↑M (when M : ModuleCat R M).

The morphisms are given their own type, not identified with LinearMap. There is a cast from morphisms in Module R to linear maps, written f.hom (ModuleCat.Hom.hom). To go from linear maps to morphisms in Module R, use ModuleCat.ofHom.

Similarly, given an isomorphism f : M ≅ N use f.toLinearEquiv and given a linear equiv f : M ≃ₗ[R] N, use f.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

@[reducible, inline]

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.instCoeSortType (R : Type u) [Ring R] : CoeSort (ModuleCat R) (Type v)

Equations

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

@[reducible, inline]

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

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of ModuleCat R.

Equations

• ModuleCat.of R X = ModuleCat.mk✝ X

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

structure ModuleCat.Hom {R : Type u} [Ring R] (M N : ModuleCat R) : Type v

The type of morphisms in ModuleCat R.

• hom' : ↑M →ₗ[R] ↑N

  The underlying linear map.

theorem ModuleCat.Hom.ext {R : Type u} {inst✝ : Ring R} {M N : ModuleCat R} {x y : M.Hom N} (hom' : x.hom' = y.hom') : x = y

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.instConcreteCategoryLinearMapIdCarrier (R : Type u) [Ring R] : CategoryTheory.ConcreteCategory (ModuleCat R) fun (x1 x2 : ModuleCat R) => ↑x1 →ₗ[R] ↑x2

Equations

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

@[reducible, inline]

abbrev ModuleCat.Hom.hom {R : Type u} [Ring R] {A B : ModuleCat R} (f : A.Hom B) : ↑A →ₗ[R] ↑B

Turn a morphism in ModuleCat back into a LinearMap.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

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

Typecheck a LinearMap as a morphism in ModuleCat.

Equations

• ModuleCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def ModuleCat.Hom.Simps.hom {R : Type u} [Ring R] (A B : ModuleCat R) (f : A.Hom B) : ↑A →ₗ[R] ↑B

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• ModuleCat.Hom.Simps.hom A B f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

theorem ModuleCat.comp_apply {R : Type u} [Ring R] {M N O : ModuleCat R} (f : M ⟶ N) (g : N ⟶ O) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem ModuleCat.hom_ext {R : Type u} [Ring R] {M N : ModuleCat R} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem ModuleCat.hom_bijective {R : Type u} [Ring R] {M N : ModuleCat R} : Function.Bijective Hom.hom

theorem ModuleCat.hom_injective {R : Type u} [Ring R] {M N : ModuleCat R} : Function.Injective Hom.hom

Convenience shortcut for ModuleCat.hom_bijective.injective.

theorem ModuleCat.hom_surjective {R : Type u} [Ring R] {M N : ModuleCat R} : Function.Surjective Hom.hom

Convenience shortcut for ModuleCat.hom_bijective.surjective.

@[deprecated ModuleCat.ofHom (since := "2024-10-06")]

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

Alias of ModuleCat.ofHom.

---

Typecheck a LinearMap as a morphism in ModuleCat.

Equations

• @ModuleCat.asHom = @ModuleCat.ofHom

@[simp]

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

@[simp]

theorem ModuleCat.ofHom_hom {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem ModuleCat.ofHom_id {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] : ofHom LinearMap.id = CategoryTheory.CategoryStruct.id (of R M)

@[simp]

theorem ModuleCat.ofHom_comp {R : Type u} [Ring R] {M N O : Type v} [AddCommGroup M] [AddCommGroup N] [AddCommGroup O] [Module R M] [Module R N] [Module R O] (f : M →ₗ[R] N) (g : N →ₗ[R] O) : ofHom (g ∘ₗ f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem ModuleCat.ofHom_apply {R : Type u} [Ring R] {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (x : M) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem ModuleCat.inv_hom_apply {R : Type u} [Ring R] {M N : ModuleCat R} (e : M ≅ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem ModuleCat.hom_inv_apply {R : Type u} [Ring R] {M N : ModuleCat R} (e : M ≅ N) (x : ↑N) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x

def ModuleCat.homEquiv {R : Type u} [Ring R] {M N : ModuleCat R} : (M ⟶ N) ≃ (↑M →ₗ[R] ↑N)

ModuleCat.Hom.hom bundled as an Equiv.

Equations

• ModuleCat.homEquiv = { toFun := ModuleCat.Hom.hom, invFun := ModuleCat.ofHom, left_inv := ⋯, right_inv := ⋯ }

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

Equations

• ModuleCat.instInhabited R = { default := ModuleCat.of R R }

theorem ModuleCat.forget_obj (R : Type u) [Ring R] {M : ModuleCat R} : (CategoryTheory.forget (ModuleCat R)).obj M = ↑M

@[simp]

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

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

Equations

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

@[simp]

theorem ModuleCat.forget₂_obj (R : Type u) [Ring R] (X : ModuleCat R) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj X = AddCommGrp.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) AddCommGrp).obj (of R X) = AddCommGrp.of X

@[simp]

theorem ModuleCat.forget₂_map (R : Type u) [Ring R] (X Y : ModuleCat R) (f : X ⟶ Y) : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).map f = AddCommGrp.ofHom ↑(Hom.hom f)

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

Equations

• ModuleCat.instInhabited_1 R = { default := ModuleCat.of R PUnit.{?u.17 + 1} }

@[simp]

theorem ModuleCat.of_coe (R : Type u) [Ring R] (X : ModuleCat R) : of R ↑X = X

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

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

Equations

• M.ofSelfIso = { hom := CategoryTheory.CategoryStruct.id M, inv := CategoryTheory.CategoryStruct.id M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

theorem ModuleCat.ofSelfIso_inv {R : Type u} [Ring R] (M : ModuleCat R) : M.ofSelfIso.inv = 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.instHasZeroObject {R : Type u} [Ring R] : CategoryTheory.Limits.HasZeroObject (ModuleCat R)

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))

@[deprecated ModuleCat.ofHom_apply (since := "2024-10-06")]

theorem ModuleCat.asHom_apply {R : Type u} [Ring R] {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (x : M) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

Alias of ModuleCat.ofHom_apply.

@[deprecated ModuleCat.ofHom (since := "2024-11-29")]

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

Alias of ModuleCat.ofHom.

---

Typecheck a LinearMap as a morphism in ModuleCat.

Equations

• @ModuleCat.asHomRight = @ModuleCat.ofHom

@[deprecated ModuleCat.ofHom (since := "2024-11-29")]

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

Alias of ModuleCat.ofHom.

---

Typecheck a LinearMap as a morphism in ModuleCat.

Equations

• @ModuleCat.asHomLeft = @ModuleCat.ofHom

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

Reinterpreting a linear map in the category of R-modules. This notation is deprecated: use ↟ instead.

Equations

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

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

Reinterpreting a linear map in the category of R-modules. This notation is deprecated: use ↟ instead.

Equations

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

def LinearEquiv.toModuleIso {R : Type u} [Ring R] {X₁ 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

• e.toModuleIso = { hom := ModuleCat.ofHom ↑e, inv := ModuleCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

@[reducible, inline, deprecated LinearEquiv.toModuleIso (since := "2024-11-29")]

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

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

Equations

• i.toModuleIso' = i.toModuleIso

@[reducible, inline, deprecated LinearEquiv.toModuleIso (since := "2024-11-29")]

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 ModuleCat R from a LinearEquiv between Modules.

Equations

• e.toModuleIso'Left = e.toModuleIso

@[reducible, inline, deprecated LinearEquiv.toModuleIso (since := "2024-11-29")]

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 ModuleCat R from a LinearEquiv between Modules.

Equations

• e.toModuleIso'Right = e.toModuleIso

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

Build a LinearEquiv from an isomorphism in the category ModuleCat R.

Equations

• i.toLinearEquiv = LinearEquiv.ofLinear (ModuleCat.Hom.hom i.hom) (ModuleCat.Hom.hom i.inv) ⋯ ⋯

def linearEquivIsoModuleIso {R : Type u} [Ring R] {X 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 ModuleCat

Equations

• linearEquivIsoModuleIso = { hom := fun (e : X ≃ₗ[R] Y) => e.toModuleIso, inv := fun (i : ModuleCat.of R X ≅ ModuleCat.of R Y) => i.toLinearEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem linearEquivIsoModuleIso_inv {R : Type u} [Ring R] {X 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 = i.toLinearEquiv

@[simp]

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

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

Equations

• ModuleCat.instAddHom = { add := fun (f g : M ⟶ N) => { hom' := ModuleCat.Hom.hom f + ModuleCat.Hom.hom g } }

@[simp]

theorem ModuleCat.hom_add {R : Type u} [Ring R] {M N : ModuleCat R} (f g : M ⟶ N) : Hom.hom (f + g) = Hom.hom f + Hom.hom g

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

Equations

• ModuleCat.instZeroHom = { zero := { hom' := 0 } }

@[simp]

theorem ModuleCat.hom_zero {R : Type u} [Ring R] {M N : ModuleCat R} : Hom.hom 0 = 0

instance ModuleCat.instSMulNatHom {R : Type u} [Ring R] {M N : ModuleCat R} : SMul ℕ (M ⟶ N)

Equations

• ModuleCat.instSMulNatHom = { smul := fun (n : ℕ) (f : M ⟶ N) => { hom' := n • ModuleCat.Hom.hom f } }

@[simp]

theorem ModuleCat.hom_nsmul {R : Type u} [Ring R] {M N : ModuleCat R} (n : ℕ) (f : M ⟶ N) : Hom.hom (n • f) = n • Hom.hom f

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

Equations

• ModuleCat.instNegHom = { neg := fun (f : M ⟶ N) => { hom' := -ModuleCat.Hom.hom f } }

@[simp]

theorem ModuleCat.hom_neg {R : Type u} [Ring R] {M N : ModuleCat R} (f : M ⟶ N) : Hom.hom (-f) = -Hom.hom f

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

Equations

• ModuleCat.instSubHom = { sub := fun (f g : M ⟶ N) => { hom' := ModuleCat.Hom.hom f - ModuleCat.Hom.hom g } }

@[simp]

theorem ModuleCat.hom_sub {R : Type u} [Ring R] {M N : ModuleCat R} (f g : M ⟶ N) : Hom.hom (f - g) = Hom.hom f - Hom.hom g

instance ModuleCat.instSMulIntHom {R : Type u} [Ring R] {M N : ModuleCat R} : SMul ℤ (M ⟶ N)

Equations

• ModuleCat.instSMulIntHom = { smul := fun (n : ℤ) (f : M ⟶ N) => { hom' := n • ModuleCat.Hom.hom f } }

@[simp]

theorem ModuleCat.hom_zsmul {R : Type u} [Ring R] {M N : ModuleCat R} (n : ℕ) (f : M ⟶ N) : Hom.hom (n • f) = n • Hom.hom f

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

Equations

• ModuleCat.instAddCommGroupHom = Function.Injective.addCommGroup ModuleCat.Hom.hom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ModuleCat.hom_sum {R : Type u} [Ring R] {M N : ModuleCat R} {ι : Type u_1} (f : ι → (M ⟶ N)) (s : Finset ι) : Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)

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

Equations

• ModuleCat.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

instance ModuleCat.forget₂_addCommGrp_additive {R : Type u} [Ring R] : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).Additive

def ModuleCat.homAddEquiv {R : Type u} [Ring R] {M N : ModuleCat R} : (M ⟶ N) ≃+ (↑M →ₗ[R] ↑N)

ModuleCat.Hom.hom bundled as an additive equivalence.

Equations

• ModuleCat.homAddEquiv = { toEquiv := ModuleCat.homEquiv, map_add' := ⋯ }

@[simp]

theorem ModuleCat.homAddEquiv_symm_apply_hom {R : Type u} [Ring R] {M N : ModuleCat R} (f : ↑M →ₗ[R] ↑N) : Hom.hom (homAddEquiv.symm f) = f

@[simp]

theorem ModuleCat.homAddEquiv_apply {R : Type u} [Ring R] {M N : ModuleCat R} (f : M.Hom N) : homAddEquiv f = f.hom

instance ModuleCat.instSMulHom {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Monoid S] [DistribMulAction S ↑N] [SMulCommClass R S ↑N] : SMul S (M ⟶ N)

Equations

• ModuleCat.instSMulHom = { smul := fun (c : S) (f : M ⟶ N) => { hom' := c • ModuleCat.Hom.hom f } }

@[simp]

theorem ModuleCat.hom_smul {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Monoid S] [DistribMulAction S ↑N] [SMulCommClass R S ↑N] (s : S) (f : M ⟶ N) : Hom.hom (s • f) = s • Hom.hom f

instance ModuleCat.Hom.instModule {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Semiring S] [Module S ↑N] [SMulCommClass R S ↑N] : Module S (M ⟶ N)

Equations

• ModuleCat.Hom.instModule = Function.Injective.module S { toFun := ModuleCat.Hom.hom, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

def ModuleCat.homLinearEquiv {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Semiring S] [Module S ↑N] [SMulCommClass R S ↑N] : (M ⟶ N) ≃ₗ[S] ↑M →ₗ[R] ↑N

ModuleCat.Hom.hom bundled as a linear equivalence.

Equations

• ModuleCat.homLinearEquiv = { toFun := ModuleCat.homAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := ModuleCat.homAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ModuleCat.homLinearEquiv_apply {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Semiring S] [Module S ↑N] [SMulCommClass R S ↑N] (a✝ : M ⟶ N) : homLinearEquiv a✝ = homAddEquiv.toFun a✝

@[simp]

theorem ModuleCat.homLinearEquiv_symm_apply {R : Type u} [Ring R] {M N : ModuleCat R} {S : Type u_1} [Semiring S] [Module S ↑N] [SMulCommClass R S ↑N] (a✝ : ↑M →ₗ[R] ↑N) : homLinearEquiv.symm a✝ = homAddEquiv.invFun a✝

def ModuleCat.Algebra.instModuleCarrier {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S] {M : ModuleCat S} : Module S₀ ↑M

Let S be an S₀-algebra. Then S-modules are modules over S₀.

Equations

• ModuleCat.Algebra.instModuleCarrier = Module.compHom (↑M) (algebraMap S₀ S)

theorem ModuleCat.Algebra.instIsScalarTowerCarrier {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S] {M : ModuleCat S} : IsScalarTower S₀ S ↑M

theorem ModuleCat.Algebra.instSMulCommClassCarrier {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S] {M : ModuleCat S} : SMulCommClass S S₀ ↑M

def ModuleCat.Algebra.instLinear {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S] : CategoryTheory.Linear S₀ (ModuleCat S)

Let S be an S₀-algebra. Then the category of S-modules is S₀-linear.

Equations

• ModuleCat.Algebra.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

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

Equations

• ModuleCat.instLinear = ModuleCat.Algebra.instLinear

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

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

def ModuleCat.endRingEquiv {R : Type u} [Ring R] (M : ModuleCat R) : CategoryTheory.End M ≃+* (↑M →ₗ[R] ↑M)

ModuleCat.Hom.hom as an isomorphism of rings.

Equations

• M.endRingEquiv = { toFun := ModuleCat.Hom.hom, invFun := ModuleCat.ofHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem ModuleCat.endRingEquiv_symm_apply_hom {R : Type u} [Ring R] (M : ModuleCat R) (f : ↑M →ₗ[R] ↑M) : Hom.hom (M.endRingEquiv.symm f) = f

@[simp]

theorem ModuleCat.endRingEquiv_apply {R : Type u} [Ring R] (M : ModuleCat R) (f : M.Hom M) : M.endRingEquiv f = f.hom

@[deprecated ModuleCat.endRingEquiv (since := "2025-01-23")]

def ModuleCat.endMulEquiv {R : Type u} [Ring R] (M : ModuleCat R) : CategoryTheory.End M ≃+* (↑M →ₗ[R] ↑M)

ModuleCat.Hom.hom as an isomorphism of monoids.

Equations

• @ModuleCat.endMulEquiv = @ModuleCat.endRingEquiv

def ModuleCat.smul {R : Type u} [Ring R] (M : ModuleCat R) : R →+* CategoryTheory.End ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).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

• M.smul = { toFun := fun (r : R) => AddCommGrp.ofHom { toFun := fun (m : ↑M) => r • m, map_zero' := ⋯, map_add' := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

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

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

Equations

• ModuleCat.smulNatTrans R = { toFun := fun (r : R) => { app := fun (M : ModuleCat R) => M.smul r, naturality := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

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

Given A : AddCommGrp 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.instAddCommGroupCarrierMkOfSMul' {R : Type u} [Ring R] {A : AddCommGrp} (φ : R →+* CategoryTheory.End A) : AddCommGroup ↑(mkOfSMul' φ)

Equations

• ModuleCat.instAddCommGroupCarrierMkOfSMul' φ = id inferInstance

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

Equations

• ModuleCat.instSMulCarrierMkOfSMul' φ = { smul := fun (r : R) (x : ↑A) => (CategoryTheory.ConcreteCategory.hom (let_fun this := φ r; this)) x }

@[simp]

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

instance ModuleCat.instModuleCarrierMkOfSMul' {R : Type u} [Ring R] {A : AddCommGrp} (φ : R →+* CategoryTheory.End A) : Module R ↑(mkOfSMul' φ)

Equations

• ModuleCat.instModuleCarrierMkOfSMul' φ = Module.mk ⋯ ⋯

@[reducible, inline]

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

Given A : AddCommGrp 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 : AddCommGrp} (φ : R →+* CategoryTheory.End A) (r : R) : (mkOfSMul φ).smul r = φ r

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

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

Equations

• ModuleCat.homMk φ hφ = { hom' := { toFun := ⇑(CategoryTheory.ConcreteCategory.hom φ), map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

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

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

instance ModuleCat.instReflectsIsomorphismsForget {R : Type u} [Ring R] : (CategoryTheory.forget (ModuleCat R)).ReflectsIsomorphisms

instance ModuleCat.instReflectsIsomorphismsAddCommGrpForget₂ {R : Type u} [Ring R] : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).ReflectsIsomorphisms

def ModuleCat.ofHom₂ {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) : M ⟶ of R (N ⟶ P)

Turn a bilinear map into a homomorphism.

Equations

• ModuleCat.ofHom₂ f = ModuleCat.ofHom (↑ModuleCat.homLinearEquiv.symm ∘ₗ f)

@[simp]

theorem ModuleCat.ofHom₂_hom_apply_hom {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (a✝ : ↑M) : Hom.hom ((Hom.hom (ofHom₂ f)) a✝) = f a✝

def ModuleCat.Hom.hom₂ {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : M.Hom (of R (N ⟶ P))) : ↑M →ₗ[R] ↑N →ₗ[R] ↑P

Turn a homomorphism into a bilinear map.

Equations

• f.hom₂ = (⋯.mpr (CategoryTheory.CategoryStruct.comp f (ModuleCat.ofHom ↑ModuleCat.homLinearEquiv))).hom

@[simp]

theorem ModuleCat.Hom.hom₂_apply {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : M.Hom (of R (N ⟶ P))) (a✝ : ↑M) : f.hom₂ a✝ = (ofHom ↑homLinearEquiv).hom' (f.hom' a✝)

@[simp]

theorem ModuleCat.Hom.hom₂_ofHom₂ {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) : hom₂ (ofHom₂ f) = f

@[simp]

theorem ModuleCat.ofHom₂_hom₂ {R : Type u_1} [CommRing R] {M N P : ModuleCat R} (f : M ⟶ of R (N ⟶ P)) : ofHom₂ (Hom.hom₂ f) = f

@[simp] lemmas for LinearMap.comp and categorical identities.

@[simp]

theorem LinearMap.comp_id_moduleCat {R : Type u_1} [Ring R] {G : ModuleCat R} {H : Type u} [AddCommGroup H] [Module R H] (f : ↑G →ₗ[R] H) : f ∘ₗ ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem LinearMap.id_moduleCat_comp {R : Type u_1} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : ModuleCat R} (f : G →ₗ[R] ↑H) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id H) ∘ₗ f = f