Documentation

Mathlib.Algebra.Module.LocalizedModule

Localized Module #

Given a commutative semiring R, a multiplicative subset S ⊆ R and an R-module M, we can localize M by S. This gives us a Localization S-module.

Main definitions #

Future work #

def LocalizedModule.r {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] (a : M × S) (b : M × S) :

The equivalence relation on M × S where (m1, s1) ≈ (m2, s2) if and only if for some (u : S), u * (s2 • m1 - s1 • m2) = 0

Equations
theorem LocalizedModule.r.isEquiv {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] :
instance LocalizedModule.r.setoid {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] :
Setoid (M × S)
Equations
def LocalizedModule {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] :
Type (max u v)

If S is a multiplicative subset of a ring R and M an R-module, then we can localize M by S.

Equations
def LocalizedModule.mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (m : M) (s : S) :

The canonical map sending (m, s) ↦ m/s

Equations
theorem LocalizedModule.mk_eq {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m : M} {m' : M} {s : S} {s' : S} :
LocalizedModule.mk m s = LocalizedModule.mk m' s' ∃ (u : S), u s' m = u s m'
theorem LocalizedModule.induction_on {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {β : LocalizedModule S MProp} (h : ∀ (m : M) (s : S), β (LocalizedModule.mk m s)) (x : LocalizedModule S M) :
β x
theorem LocalizedModule.induction_on₂ {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {β : LocalizedModule S MLocalizedModule S MProp} (h : ∀ (m m' : M) (s s' : S), β (LocalizedModule.mk m s) (LocalizedModule.mk m' s')) (x : LocalizedModule S M) (y : LocalizedModule S M) :
β x y
def LocalizedModule.liftOn {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (x : LocalizedModule S M) (f : M × Sα) (wd : ∀ (p p' : M × S), p p'f p = f p') :
α

If f : M × S → α respects the equivalence relation LocalizedModule.r, then f descents to a map LocalizedModule M S → α.

Equations
theorem LocalizedModule.liftOn_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} {f : M × Sα} (wd : ∀ (p p' : M × S), p p'f p = f p') (m : M) (s : S) :
(LocalizedModule.mk m s).liftOn f wd = f (m, s)
def LocalizedModule.liftOn₂ {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (x : LocalizedModule S M) (y : LocalizedModule S M) (f : M × SM × Sα) (wd : ∀ (p q p' q' : M × S), p p'q q'f p q = f p' q') :
α

If f : M × S → M × S → α respects the equivalence relation LocalizedModule.r, then f descents to a map LocalizedModule M S → LocalizedModule M S → α.

Equations
theorem LocalizedModule.liftOn₂_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (f : M × SM × Sα) (wd : ∀ (p q p' q' : M × S), p p'q q'f p q = f p' q') (m : M) (m' : M) (s : S) (s' : S) :
(LocalizedModule.mk m s).liftOn₂ (LocalizedModule.mk m' s') f wd = f (m, s) (m', s')
instance LocalizedModule.instZero {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] :
Equations
theorem LocalizedModule.subsingleton {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (h : 0 S) :

If S contains 0 then the localization at S is trivial.

@[simp]
theorem LocalizedModule.zero_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) :
instance LocalizedModule.instAdd {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] :
Equations
theorem LocalizedModule.mk_add_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m1 : M} {m2 : M} {s1 : S} {s2 : S} :
Equations
  • LocalizedModule.hasNatSMul = { smul := fun (n : ) => nsmulRec n }
Equations
instance LocalizedModule.instNeg {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommGroup M] [Module R M] :
Equations
Equations
theorem LocalizedModule.mk_neg {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommGroup M] [Module R M] {m : M} {s : S} :
instance LocalizedModule.instMonoid {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {S : Submonoid R} :
Equations
  • LocalizedModule.instMonoid = Monoid.mk npowRecAuto
instance LocalizedModule.instSemiring {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {S : Submonoid R} :
Equations
  • LocalizedModule.instSemiring = Semiring.mk Monoid.npow
Equations
instance LocalizedModule.instRing {R : Type u} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] {S : Submonoid R} :
Equations
  • LocalizedModule.instRing = Ring.mk SubNegMonoid.zsmul
instance LocalizedModule.instCommRing {R : Type u} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] {S : Submonoid R} :
Equations
theorem LocalizedModule.mk_mul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] {a₁ : A} {a₂ : A} {s₁ : S} {s₂ : S} :
LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.mk (a₁ * a₂) (s₁ * s₂)
noncomputable instance LocalizedModule.instSMul {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] :
Equations
  • One or more equations did not get rendered due to their size.
theorem LocalizedModule.smul_def {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] (x : T) (m : M) (s : S) :
theorem LocalizedModule.mk'_smul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] (r : R) (m : M) (s : S) (s' : S) :
theorem LocalizedModule.mk_smul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (m : M) (s : S) (t : S) :
noncomputable instance LocalizedModule.isModule {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] :
Equations
@[simp]
theorem LocalizedModule.mk_cancel_common_left {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s' : S) (s : S) (m : M) :
@[simp]
theorem LocalizedModule.mk_cancel {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) (m : M) :
@[simp]
theorem LocalizedModule.mk_cancel_common_right {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) (s' : S) (m : M) :
noncomputable instance LocalizedModule.isModule' {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] :
Equations
theorem LocalizedModule.smul'_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (s : S) (m : M) :
theorem LocalizedModule.smul_eq_iff_of_mem {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (hr : r S) (x : LocalizedModule S M) (y : LocalizedModule S M) :
r x = y x = Localization.mk 1 r, hr y
theorem LocalizedModule.eq_zero_of_smul_eq_zero {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (hr : r S) (x : LocalizedModule S M) (hx : r x = 0) :
x = 0
theorem LocalizedModule.smul'_mul {R : Type u} [CommSemiring R] {S : Submonoid R} {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (x : T) (p₁ : LocalizedModule S A) (p₂ : LocalizedModule S A) :
x p₁ * p₂ = x (p₁ * p₂)
theorem LocalizedModule.mul_smul' {R : Type u} [CommSemiring R] {S : Submonoid R} {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (x : T) (p₁ : LocalizedModule S A) (p₂ : LocalizedModule S A) :
p₁ * x p₂ = x (p₁ * p₂)
noncomputable instance LocalizedModule.instAlgebra {R : Type u} [CommSemiring R] {S : Submonoid R} (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] :
Equations
theorem LocalizedModule.algebraMap_mk' {R : Type u} [CommSemiring R] {S : Submonoid R} (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (a : R) (s : S) :
theorem LocalizedModule.algebraMap_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] (a : R) (s : S) :
Equations
  • =
noncomputable instance LocalizedModule.algebra' {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] :
Equations

The function m ↦ m / 1 as an R-linear map.

Equations
@[simp]
theorem LocalizedModule.divBy_apply {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) (p : LocalizedModule S M) :
(LocalizedModule.divBy s) p = p.liftOn (fun (p : M × S) => LocalizedModule.mk p.1 (p.2 * s))
def LocalizedModule.divBy {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) :

For any s : S, there is an R-linear map given by a/b ↦ a/(b*s).

Equations
theorem LocalizedModule.divBy_mul_by {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) (p : LocalizedModule S M) :
theorem LocalizedModule.mul_by_divBy {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : S) (p : LocalizedModule S M) :
theorem isLocalizedModule_iff {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') :
IsLocalizedModule S f (∀ (x : S), IsUnit ((algebraMap R (Module.End R M')) x)) (∀ (y : M'), ∃ (x : M × S), x.2 y = f x.1) ∀ {x₁ x₂ : M}, f x₁ = f x₂∃ (c : S), c x₁ = c x₂
class IsLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') :

The characteristic predicate for localized module. IsLocalizedModule S f describes that f : M ⟶ M' is the localization map identifying M' as LocalizedModule S M.

  • map_units : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M')) x)
  • surj' : ∀ (y : M'), ∃ (x : M × S), x.2 y = f x.1
  • exists_of_eq : ∀ {x₁ x₂ : M}, f x₁ = f x₂∃ (c : S), c x₁ = c x₂
Instances
    theorem IsLocalizedModule.map_units {R : Type u_1} :
    ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} (f : M →ₗ[R] M') [self : IsLocalizedModule S f] (x : S), IsUnit ((algebraMap R (Module.End R M')) x)
    theorem IsLocalizedModule.surj' {R : Type u_1} :
    ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} {f : M →ₗ[R] M'} [self : IsLocalizedModule S f] (y : M'), ∃ (x : M × S), x.2 y = f x.1
    theorem IsLocalizedModule.exists_of_eq {R : Type u_1} :
    ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} {f : M →ₗ[R] M'} [self : IsLocalizedModule S f] {x₁ x₂ : M}, f x₁ = f x₂∃ (c : S), c x₁ = c x₂
    theorem IsLocalizedModule.surj {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (y : M') :
    ∃ (x : M × S), x.2 y = f x.1
    theorem IsLocalizedModule.eq_iff_exists {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {x₁ : M} {x₂ : M} :
    f x₁ = f x₂ ∃ (c : S), c x₁ = c x₂
    theorem IsLocalizedModule.of_linearEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (e : M' ≃ₗ[R] M'') [hf : IsLocalizedModule S f] :
    IsLocalizedModule S (e ∘ₗ f)
    theorem isLocalizedModule_id {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) [AddCommMonoid M] [Module R M] (R' : Type u_6) [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] [Module R' M] [IsScalarTower R R' M] :
    IsLocalizedModule S LinearMap.id
    theorem isLocalizedModule_iff_isLocalization {R : Type u_1} [CommSemiring R] {S : Submonoid R} {A : Type u_6} {Aₛ : Type u_7} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] :
    Equations
    • =
    noncomputable def LocalizedModule.lift' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
    LocalizedModule S MM''

    If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map LocalizedModule S M → M''.

    Equations
    theorem LocalizedModule.lift'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (m : M) (s : S) :
    LocalizedModule.lift' S g h (LocalizedModule.mk m s) = .unit⁻¹ (g m)
    theorem LocalizedModule.lift'_add {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (x : LocalizedModule S M) (y : LocalizedModule S M) :
    theorem LocalizedModule.lift'_smul {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (r : R) (m : LocalizedModule S M) :
    noncomputable def LocalizedModule.lift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :

    If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map LocalizedModule S M → M''.

    Equations
    theorem LocalizedModule.lift_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (m : M) (s : S) :
    (LocalizedModule.lift S g h) (LocalizedModule.mk m s) = .unit⁻¹ (g m)

    If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then lift g m s = s⁻¹ • g m.

    theorem LocalizedModule.lift_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :

    If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map lift g ∘ mkLinearMap = g.

    theorem LocalizedModule.lift_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (l : LocalizedModule S M →ₗ[R] M'') (hl : l ∘ₗ LocalizedModule.mkLinearMap S M = g) :

    If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible and l is another linear map LocalizedModule S M ⟶ M'' such that l ∘ mkLinearMap = g then l = lift g

    noncomputable def IsLocalizedModule.fromLocalizedModule' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :
    LocalizedModule S MM'

    If (M', f : M ⟶ M') satisfies universal property of localized module, there is a canonical map LocalizedModule S M ⟶ M'.

    Equations
    @[simp]
    theorem IsLocalizedModule.fromLocalizedModule'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    noncomputable def IsLocalizedModule.fromLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :

    If (M', f : M ⟶ M') satisfies universal property of localized module, there is a canonical map LocalizedModule S M ⟶ M'.

    Equations
    theorem IsLocalizedModule.fromLocalizedModule_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    @[simp]
    theorem IsLocalizedModule.iso_symm_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :
    ∀ (a : M'), (IsLocalizedModule.iso S f).symm a = (Equiv.ofBijective (IsLocalizedModule.fromLocalizedModule S f) ).symm a
    @[simp]
    theorem IsLocalizedModule.iso_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :
    noncomputable def IsLocalizedModule.iso {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :

    If (M', f : M ⟶ M') satisfies universal property of localized module, then M' is isomorphic to LocalizedModule S M as an R-module.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem IsLocalizedModule.iso_apply_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    (IsLocalizedModule.iso S f) (LocalizedModule.mk m s) = .unit⁻¹ (f m)
    theorem IsLocalizedModule.iso_symm_apply_aux {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M') :
    (IsLocalizedModule.iso S f).symm m = LocalizedModule.mk .choose.1 .choose.2
    theorem IsLocalizedModule.iso_symm_apply' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M') (a : M) (b : S) (eq1 : b m = f a) :
    theorem IsLocalizedModule.iso_symm_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :
    noncomputable def IsLocalizedModule.lift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
    M' →ₗ[R] M''

    If M' is a localized module and g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map M' → M''.

    Equations
    theorem IsLocalizedModule.lift_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
    IsLocalizedModule.lift S f g h ∘ₗ f = g
    @[simp]
    theorem IsLocalizedModule.lift_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (x : M) :
    (IsLocalizedModule.lift S f g h) (f x) = g x
    theorem IsLocalizedModule.lift_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (l : M' →ₗ[R] M'') (hl : l ∘ₗ f = g) :
    theorem IsLocalizedModule.is_universal {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') :
    (∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x))∃! l : M' →ₗ[R] M'', l ∘ₗ f = g

    Universal property from localized module: If (M', f : M ⟶ M') is a localized module then it satisfies the following universal property: For every R-module M'' which every s : S-scalar multiplication is invertible and for every R-linear map g : M ⟶ M'', there is a unique R-linear map l : M' ⟶ M'' such that l ∘ f = g.

    M -----f----> M'
    |           /
    |g       /
    |     /   l
    v   /
    M''
    
    theorem IsLocalizedModule.ringHom_ext {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (map_unit : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) ⦃j : M' →ₗ[R] M'' ⦃k : M' →ₗ[R] M'' (h : j ∘ₗ f = k ∘ₗ f) :
    j = k
    noncomputable def IsLocalizedModule.linearEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [IsLocalizedModule S f] [IsLocalizedModule S g] :
    M' ≃ₗ[R] M''

    If (M', f) and (M'', g) both satisfy universal property of localized module, then M', M'' are isomorphic as R-module

    Equations
    theorem IsLocalizedModule.smul_injective {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : S) :
    Function.Injective fun (m : M') => s m
    theorem IsLocalizedModule.smul_inj {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : S) (m₁ : M') (m₂ : M') :
    s m₁ = s m₂ m₁ = m₂
    noncomputable def IsLocalizedModule.mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    M'

    mk' f m s is the fraction m/s with respect to the localization map f.

    Equations
    theorem IsLocalizedModule.mk'_smul {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (r : R) (m : M) (s : S) :
    theorem IsLocalizedModule.mk'_add_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f m₁ s₁ + IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ m₁ + s₁ m₂) (s₁ * s₂)
    @[simp]
    theorem IsLocalizedModule.mk'_zero {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : S) :
    @[simp]
    theorem IsLocalizedModule.mk'_one {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) :
    @[simp]
    theorem IsLocalizedModule.mk'_cancel {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    @[simp]
    theorem IsLocalizedModule.mk'_cancel' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    @[simp]
    theorem IsLocalizedModule.mk'_cancel_left {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f (s₁ m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₂
    @[simp]
    theorem IsLocalizedModule.mk'_cancel_right {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f (s₂ m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₁
    theorem IsLocalizedModule.mk'_add {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s : S) :
    theorem IsLocalizedModule.mk'_eq_mk'_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f m₁ s₁ = IsLocalizedModule.mk' f m₂ s₂ ∃ (s : S), s s₁ m₂ = s s₂ m₁
    theorem IsLocalizedModule.mk'_neg {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) :
    theorem IsLocalizedModule.mk'_sub {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s : S) :
    theorem IsLocalizedModule.mk'_sub_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f m₁ s₁ - IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ m₁ - s₁ m₂) (s₁ * s₂)
    theorem IsLocalizedModule.mk'_mul_mk'_of_map_mul {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [Semiring M] [Semiring M'] [Module R M] [Algebra R M'] (f : M →ₗ[R] M') (hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂) [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f m₁ s₁ * IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (m₁ * m₂) (s₁ * s₂)
    theorem IsLocalizedModule.mk'_mul_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [Semiring M] [Semiring M'] [Algebra R M] [Algebra R M'] (f : M →ₐ[R] M') [IsLocalizedModule S f.toLinearMap] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
    IsLocalizedModule.mk' f.toLinearMap m₁ s₁ * IsLocalizedModule.mk' f.toLinearMap m₂ s₂ = IsLocalizedModule.mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)
    theorem IsLocalizedModule.mk'_eq_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [IsLocalizedModule S f] {m : M} {s : S} {m' : M'} :
    IsLocalizedModule.mk' f m s = m' f m = s m'
    @[simp]
    theorem IsLocalizedModule.mk'_eq_zero {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [IsLocalizedModule S f] {m : M} (s : S) :
    theorem IsLocalizedModule.mk'_eq_zero' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {m : M} (s : S) :
    IsLocalizedModule.mk' f m s = 0 ∃ (s' : S), s' m = 0
    theorem IsLocalizedModule.mk'_smul_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] (A : Type u_5) [CommSemiring A] [Algebra R A] [Module A M'] [IsLocalization S A] [Module R M] [Module R M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (x : R) (m : M) (s : S) (t : S) :
    theorem IsLocalizedModule.eq_zero_iff {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {m : M} :
    f m = 0 ∃ (s' : S), s' m = 0
    noncomputable def IsLocalizedModule.map {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] :
    (M →ₗ[R] N) →ₗ[R] M' →ₗ[R] N'

    A linear map M →ₗ[R] N gives a map between localized modules Mₛ →ₗ[R] Nₛ.

    Equations
    theorem IsLocalizedModule.map_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) :
    (IsLocalizedModule.map S f g) h ∘ₗ f = g ∘ₗ h
    @[simp]
    theorem IsLocalizedModule.map_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) :
    ((IsLocalizedModule.map S f g) h) (f x) = g (h x)
    @[simp]
    theorem IsLocalizedModule.map_mk' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) (s : S) :
    @[simp]
    theorem IsLocalizedModule.map_id {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] :
    (IsLocalizedModule.map S f f) LinearMap.id = LinearMap.id
    @[simp]
    theorem IsLocalizedModule.map_injective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (h_inj : Function.Injective h) :
    @[simp]
    theorem IsLocalizedModule.map_surjective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (h_surj : Function.Surjective h) :

    The linear map (LocalizedModule S M) → (LocalizedModule S M) from iso is the identity.

    theorem IsLocalizedModule.map_LocalizedModules {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} [AddCommMonoid M₀] [Module R M₀] {M₁ : Type u_7} [AddCommMonoid M₁] [Module R M₁] (g : M₀ →ₗ[R] M₁) (m : M₀) (s : S) :

    Formula for IsLocalizedModule.map when each localized module is a LocalizedModule.

    theorem IsLocalizedModule.map_iso_commute {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_8} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] (g : M₀ →ₗ[R] M₁) :
    theorem LocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} [AddCommMonoid M₀] [Module R M₀] {M₁ : Type u_7} [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_8} [AddCommMonoid M₂] [Module R M₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact g h) :

    Localization of modules is an exact functor, proven here for LocalizedModule. See IsLocalizedModule.map_exact for the more general version.

    theorem IsLocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_10} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] {M₂ : Type u_8} {M₂' : Type u_11} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂'] (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact g h) :
    Function.Exact ((IsLocalizedModule.map S f₀ f₁) g) ((IsLocalizedModule.map S f₁ f₂) h)

    Localization of modules is an exact functor.

    theorem IsLocalizedModule.map_comp' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_11} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] {M₂ : Type u_8} {M₂' : Type u_10} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂'] (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) :
    (IsLocalizedModule.map S f₀ f₂) (h ∘ₗ g) = (IsLocalizedModule.map S f₁ f₂) h ∘ₗ (IsLocalizedModule.map S f₀ f₁) g

    Localization of composition is the composition of localization

    theorem IsLocalizedModule.mkOfAlgebra {R : Type u_6} {S : Type u_7} {S' : Type u_8} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] (M : Submonoid R) (f : S →ₐ[R] S') (h₁ : xM, IsUnit ((algebraMap R S') x)) (h₂ : ∀ (y : S'), ∃ (x : S × M), x.2 y = f x.1) (h₃ : ∀ (x : S), f x = 0∃ (m : M), m x = 0) :
    IsLocalizedModule M f.toLinearMap
    theorem LocalizedModule.mem_ker_mkLinearMap_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {S : Submonoid R} {m : M} :
    theorem LocalizedModule.subsingleton_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {S : Submonoid R} :
    Subsingleton (LocalizedModule S M) ∀ (m : M), rS, r m = 0