@[instance]
Equations
- Module.has_coe_to_sort R = {S := Type u, coe := Module.carrier _inst_1}
@[instance]
@[instance]
@[instance]
Equations
- Module.has_forget_to_AddCommGroup R = {forget₂ := {obj := λ (M : Module R), AddCommGroup.of ↥M, map := λ (M₁ M₂ : Module R) (f : M₁ ⟶ M₂), linear_map.to_add_monoid_hom f, map_id' := _, map_comp' := _}, forget_comp := _}
The object in the category of R-modules associated to an R-module
@[instance]
Equations
- Module.inhabited R = {default := Module.of R punit (punit.semimodule R)}
@[simp]
@[simp]
Forgetting to the underlying type and then building the bundled object returns the original module.
Equations
- M.of_self_iso = {hom := 𝟙 M, inv := 𝟙 M, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
@[instance]
Equations
@[instance]
Equations
- Module.category_theory.limits.has_zero_object = {zero := Module.of R punit (punit.semimodule R), unique_to := λ (X : Module R), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : Module R), {to_inhabited := {default := 0}, uniq := _}}
def
Module.as_hom
{R : Type u}
[ring R]
{X₁ X₂ : Type u}
[add_comm_group X₁]
[module R X₁]
[add_comm_group X₂]
[module R X₂] :
Reinterpreting a linear map in the category of R-modules.
Equations
@[simp]
theorem
linear_equiv.to_Module_iso_hom
{R : Type u}
[ring R]
{X₁ X₂ : Type u}
{g₁ : add_comm_group X₁}
{g₂ : add_comm_group X₂}
{m₁ : module R X₁}
{m₂ : module R X₂}
(e : X₁ ≃ₗ[R] X₂) :
e.to_Module_iso.hom = ↑e
def
linear_equiv.to_Module_iso
{R : Type u}
[ring R]
{X₁ X₂ : Type u}
{g₁ : add_comm_group X₁}
{g₂ : add_comm_group X₂}
{m₁ : module R X₁}
{m₂ : module R X₂} :
Build an isomorphism in the category Module R from a linear_equiv between modules.
Equations
- e.to_Module_iso = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
linear_equiv.to_Module_iso_inv
{R : Type u}
[ring R]
{X₁ X₂ : Type u}
{g₁ : add_comm_group X₁}
{g₂ : add_comm_group X₂}
{m₁ : module R X₁}
{m₂ : module R X₂}
(e : X₁ ≃ₗ[R] X₂) :
e.to_Module_iso.inv = ↑(e.symm)
Build an isomorphism in the category Module R from a linear_equiv between modules.
This version is better than linear_equiv_to_Module_iso when applicable, because Lean can't see Module.of R M is defeq to M when M : Module R.
Equations
- i.to_Module_iso' = {hom := ↑i, inv := ↑(i.symm), hom_inv_id' := _, inv_hom_id' := _}
Build a linear_equiv from an isomorphism in the category Module R.
def
linear_equiv_iso_Module_iso
{R : Type u}
[ring R]
{X Y : Type u}
[add_comm_group X]
[add_comm_group Y]
[module R X]
[module R Y] :
linear equivalences between modules are the same as (isomorphic to) isomorphisms in Module
Equations
- linear_equiv_iso_Module_iso = {hom := λ (e : X ≃ₗ[R] Y), e.to_Module_iso, inv := λ (i : Module.of R X ≅ Module.of R Y), i.to_linear_equiv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
linear_equiv_iso_Module_iso_inv
{R : Type u}
[ring R]
{X Y : Type u}
[add_comm_group X]
[add_comm_group Y]
[module R X]
[module R Y]
(i : Module.of R X ≅ Module.of R Y) :
@[simp]
theorem
linear_equiv_iso_Module_iso_hom
{R : Type u}
[ring R]
{X Y : Type u}
[add_comm_group X]
[add_comm_group Y]
[module R X]
[module R Y]
(e : X ≃ₗ[R] Y) :
@[instance]
Equations
- Module.category_theory.preadditive = {hom_group := λ (P Q : Module R), linear_map.add_comm_group, add_comp' := _, comp_add' := _}
theorem
Module.ker_eq_bot_of_mono
{R : Type u}
[ring R]
{M N : Module R}
(f : M ⟶ N)
[category_theory.mono f] :
linear_map.ker f = ⊥
theorem
Module.range_eq_top_of_epi
{R : Type u}
[ring R]
{M N : Module R}
(f : M ⟶ N)
[category_theory.epi f] :
theorem
Module.mono_of_ker_eq_bot
{R : Type u}
[ring R]
{M N : Module R}
(f : M ⟶ N) :
linear_map.ker f = ⊥ → category_theory.mono f
@[instance]