The category of R-modules

If R is a semiring, SemimoduleCat.{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 and monomorphism are equivalent to being a linear equivalence and an injective 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 : SemimoduleCat 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 (SemimoduleCat.Hom.hom). To go from linear maps to morphisms in Module R, use SemimoduleCat.ofHom.

Similarly, given an isomorphism f : M ≅ N use f.toLinearEquiv and given a linear equiv f : M ≃ₗ[R] N, use f.toModuleIso.

structure SemimoduleCat (R : Type u) [Semiring 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 isAddCommMonoid 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 SemimoduleCat R

• isAddCommMonoid : AddCommMonoid ↑self
• isModule : Module R ↑self

instance SemimoduleCat.instCoeSortType (R : Type u) [Semiring R] : CoeSort (SemimoduleCat R) (Type v)

Equations

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

@[reducible, inline]

abbrev SemimoduleCat.of (R : Type u) [Semiring R] (X : Type v) [AddCommMonoid X] [Module R X] : SemimoduleCat 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 SemimoduleCat R.

Equations

• SemimoduleCat.of R X = { carrier := X, isAddCommMonoid := inst✝¹, isModule := inst✝ }

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

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

The type of morphisms in SemimoduleCat R.

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

  The underlying linear map.

theorem SemimoduleCat.Hom.ext_iff {R : Type u} {inst✝ : Semiring R} {M N : SemimoduleCat R} {x y : M.Hom N} : x = y ↔ x.hom' = y.hom'

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

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

Equations

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

instance SemimoduleCat.instConcreteCategoryLinearMapIdCarrier (R : Type u) [Semiring R] : CategoryTheory.ConcreteCategory (SemimoduleCat R) fun (x1 x2 : SemimoduleCat R) => ↑x1 →ₗ[R] ↑x2

Equations

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

@[reducible, inline]

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

Turn a morphism in SemimoduleCat back into a LinearMap.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev SemimoduleCat.ofHom {R : Type u} [Semiring R] {X Y : Type v} [AddCommMonoid X] [Module R X] [AddCommMonoid Y] [Module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y

Typecheck a LinearMap as a morphism in SemimoduleCat.

Equations

• SemimoduleCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

Equations

• SemimoduleCat.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 SemimoduleCat.hom_id {R : Type u} [Semiring R] {M : SemimoduleCat R} : Hom.hom (CategoryTheory.CategoryStruct.id M) = LinearMap.id

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

@[simp]

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

theorem SemimoduleCat.comp_apply {R : Type u} [Semiring R] {M N O : SemimoduleCat 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 SemimoduleCat.hom_ext {R : Type u} [Semiring R] {M N : SemimoduleCat R} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

theorem SemimoduleCat.hom_ext_iff {R : Type u} [Semiring R] {M N : SemimoduleCat R} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom g

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

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

Convenience shortcut for SemimoduleCat.hom_bijective.injective.

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

Convenience shortcut for SemimoduleCat.hom_bijective.surjective.

@[simp]

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

@[simp]

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

@[simp]

theorem SemimoduleCat.ofHom_id {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] : ofHom LinearMap.id = CategoryTheory.CategoryStruct.id (of R M)

@[simp]

theorem SemimoduleCat.ofHom_comp {R : Type u} [Semiring R] {M N O : Type v} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid 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 SemimoduleCat.ofHom_apply {R : Type u} [Semiring R] {M N : Type v} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (x : M) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

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

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

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

SemimoduleCat.Hom.hom bundled as an Equiv.

Equations

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

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

@[simp]

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

instance SemimoduleCat.hasForgetToAddCommMonoid (R : Type u) [Semiring R] : CategoryTheory.HasForget₂ (SemimoduleCat R) AddCommMonCat

Equations

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

@[simp]

theorem SemimoduleCat.forget₂_obj (R : Type u) [Semiring R] (X : SemimoduleCat R) : (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).obj X = AddCommMonCat.of ↑X

theorem SemimoduleCat.forget₂_obj_moduleCat_of (R : Type u) [Semiring R] (X : Type v) [AddCommMonoid X] [Module R X] : (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).obj (of R X) = AddCommMonCat.of X

@[simp]

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

instance SemimoduleCat.instInhabited (R : Type u) [Semiring R] : Inhabited (SemimoduleCat R)

Equations

• SemimoduleCat.instInhabited R = { default := SemimoduleCat.of R PUnit.{?u.10 + 1} }

@[simp]

theorem SemimoduleCat.of_coe (R : Type u) [Semiring R] (X : SemimoduleCat R) : of R ↑X = X

@[deprecated CategoryTheory.Iso.refl (since := "2025-05-15")]

def SemimoduleCat.ofSelfIso {R : Type u} [Semiring R] (M : SemimoduleCat 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 := ⋯ }

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

instance SemimoduleCat.instHasZeroObject {R : Type u} [Semiring R] : CategoryTheory.Limits.HasZeroObject (SemimoduleCat R)

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

Reinterpreting a linear map in the category of R-modules

Equations

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

def LinearEquiv.toModuleIsoₛ {R : Type u} [Semiring R] {X₁ X₂ : Type v} {g₁ : AddCommMonoid X₁} {g₂ : AddCommMonoid X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : SemimoduleCat.of R X₁ ≅ SemimoduleCat.of R X₂

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

Equations

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

@[simp]

theorem LinearEquiv.toModuleIsoₛ_inv {R : Type u} [Semiring R] {X₁ X₂ : Type v} {g₁ : AddCommMonoid X₁} {g₂ : AddCommMonoid X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : e.toModuleIsoₛ.inv = SemimoduleCat.ofHom ↑e.symm

@[simp]

theorem LinearEquiv.toModuleIsoₛ_hom {R : Type u} [Semiring R] {X₁ X₂ : Type v} {g₁ : AddCommMonoid X₁} {g₂ : AddCommMonoid X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) : e.toModuleIsoₛ.hom = SemimoduleCat.ofHom ↑e

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

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

Equations

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

def linearEquivIsoModuleIsoₛ {R : Type u} [Semiring R] {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] [Module R X] [Module R Y] : (X ≃ₗ[R] Y) ≅ SemimoduleCat.of R X ≅ SemimoduleCat.of R Y

linear equivalences between Modules are the same as (isomorphic to) isomorphisms in SemimoduleCat

Equations

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

@[simp]

theorem linearEquivIsoModuleIsoₛ_hom {R : Type u} [Semiring R] {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] [Module R X] [Module R Y] (e : X ≃ₗ[R] Y) : linearEquivIsoModuleIsoₛ.hom e = e.toModuleIsoₛ

@[simp]

theorem linearEquivIsoModuleIsoₛ_inv {R : Type u} [Semiring R] {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] [Module R X] [Module R Y] (i : SemimoduleCat.of R X ≅ SemimoduleCat.of R Y) : linearEquivIsoModuleIsoₛ.inv i = i.toLinearEquivₛ

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

instance SemimoduleCat.instSMulNatHom_1 {R : Type u} [Semiring R] {M N : SemimoduleCat R} : SMul ℕ (M ⟶ N)

Equations

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

@[simp]

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

instance SemimoduleCat.instAddCommMonoidHom {R : Type u} [Semiring R] {M N : SemimoduleCat R} : AddCommMonoid (M ⟶ N)

Equations

• SemimoduleCat.instAddCommMonoidHom = Function.Injective.addCommMonoid SemimoduleCat.Hom.hom ⋯ ⋯ ⋯ ⋯

@[simp]

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

instance SemimoduleCat.instHasZeroMorphisms {R : Type u} [Semiring R] : CategoryTheory.Limits.HasZeroMorphisms (SemimoduleCat R)

Equations

• SemimoduleCat.instHasZeroMorphisms = { zero := @SemimoduleCat.instZeroHom R inst✝, comp_zero := ⋯, zero_comp := ⋯ }

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

SemimoduleCat.Hom.hom bundled as an additive equivalence.

Equations

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

@[simp]

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

@[simp]

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

theorem SemimoduleCat.subsingleton_of_isZero {R : Type u} [Semiring R] {M : SemimoduleCat R} (h : CategoryTheory.Limits.IsZero M) : Subsingleton ↑M

theorem SemimoduleCat.isZero_iff_subsingleton {R : Type u} [Semiring R] {M : SemimoduleCat R} : CategoryTheory.Limits.IsZero M ↔ Subsingleton ↑M

@[simp]

theorem SemimoduleCat.isZero_of_iff_subsingleton {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] : CategoryTheory.Limits.IsZero (of R M) ↔ Subsingleton M

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

Equations

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

@[simp]

theorem SemimoduleCat.hom_smul {R : Type u} [Semiring R] {M N : SemimoduleCat 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 SemimoduleCat.Hom.instModule {R : Type u} [Semiring R] {M N : SemimoduleCat R} {S : Type u_1} [Semiring S] [Module S ↑N] [SMulCommClass R S ↑N] : Module S (M ⟶ N)

Equations

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

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

SemimoduleCat.Hom.hom bundled as a linear equivalence.

Equations

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

@[simp]

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

@[simp]

theorem SemimoduleCat.homLinearEquiv_symm_apply {R : Type u} [Semiring R] {M N : SemimoduleCat 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 SemimoduleCat.Algebra.instModuleCarrier {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Semiring S] [Algebra S₀ S] {M : SemimoduleCat S} : Module S₀ ↑M

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

Equations

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

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

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

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

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

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

instance SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂ {R : Type u} [Semiring R] : (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).ReflectsIsomorphisms

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

Turn a bilinear map into a homomorphism.

Equations

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

@[simp]

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

def SemimoduleCat.Hom.hom₂ {R : Type u_1} [CommSemiring R] {M N P : SemimoduleCat 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 (SemimoduleCat.ofHom ↑SemimoduleCat.homLinearEquiv))).hom

@[simp]

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

@[simp]

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

@[simp]

theorem SemimoduleCat.ofHom₂_hom₂ {R : Type u_1} [CommSemiring R] {M N P : SemimoduleCat 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_semiModuleCat {R : Type u_1} [Semiring R] {G : SemimoduleCat R} {H : Type u} [AddCommMonoid H] [Module R H] (f : ↑G →ₗ[R] H) : f ∘ₗ SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.id G) = f

@[simp]

theorem LinearMap.id_semiModuleCat_comp {R : Type u_1} [Semiring R] {G : Type u} [AddCommMonoid G] [Module R G] {H : SemimoduleCat R} (f : G →ₗ[R] ↑H) : SemimoduleCat.Hom.hom (CategoryTheory.CategoryStruct.id H) ∘ₗ f = f