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

• LocalizedModule.r : the equivalence relation defining this localization, namely (m, s) ≈ (m', s') if and only if there is some u : S such that u • s' • m = u • s • m'.
• LocalizedModule M S : the localized module by S.
• LocalizedModule.mk : the canonical map sending (m, s) : M × S ↦ m/s : LocalizedModule M S
• LocalizedModule.liftOn : any well defined function f : M × S → α respecting r descents to a function LocalizedModule M S → α
• LocalizedModule.liftOn₂ : any well defined function f : M × S → M × S → α respecting r descents to a function LocalizedModule M S → LocalizedModule M S
• LocalizedModule.mk_add_mk : in the localized module mk m s + mk m' s' = mk (s' • m + s • m') (s * s')
• LocalizedModule.mk_smul_mk : in the localized module, for any r : R, s t : S, m : M, we have mk r s • mk m t = mk (r • m) (s * t) where mk r s : Localization S is localized ring by S.
• LocalizedModule.isModule : LocalizedModule M S is a Localization S-module.

## Future work #

• Redefine Localization for monoids and rings to coincide with LocalizedModule.
def LocalizedModule.r {R : Type u} [] (S : ) (M : Type v) [] [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
Instances For
theorem LocalizedModule.r.isEquiv {R : Type u} [] (S : ) (M : Type v) [] [Module R M] :
IsEquiv (M × S) ()
instance LocalizedModule.r.setoid {R : Type u} [] (S : ) (M : Type v) [] [Module R M] :
Setoid (M × S)
Equations
• = { r := , iseqv := }
def LocalizedModule {R : Type u} [] (S : ) (M : Type v) [] [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
Instances For
def LocalizedModule.mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] (m : M) (s : S) :

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

Equations
Instances For
theorem LocalizedModule.mk_eq {R : Type u} [] {S : } {M : Type v} [] [Module R M] {m : M} {m' : M} {s : S} {s' : S} :
= ∃ (u : S), u s' m = u s m'
theorem LocalizedModule.induction_on {R : Type u} [] {S : } {M : Type v} [] [Module R M] {β : Prop} (h : ∀ (m : M) (s : S), β ()) (x : ) :
β x
theorem LocalizedModule.induction_on₂ {R : Type u} [] {S : } {M : Type v} [] [Module R M] {β : Prop} (h : ∀ (m m' : M) (s s' : S), β () ()) (x : ) (y : ) :
β x y
def LocalizedModule.liftOn {R : Type u} [] {S : } {M : Type v} [] [Module R M] {α : Type u_2} (x : ) (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
Instances For
theorem LocalizedModule.liftOn_mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] {α : Type u_2} {f : M × Sα} (wd : ∀ (p p' : M × S), p p'f p = f p') (m : M) (s : S) :
().liftOn f wd = f (m, s)
def LocalizedModule.liftOn₂ {R : Type u} [] {S : } {M : Type v} [] [Module R M] {α : Type u_2} (x : ) (y : ) (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
Instances For
theorem LocalizedModule.liftOn₂_mk {R : Type u} [] {S : } {M : Type v} [] [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) :
().liftOn₂ () f wd = f (m, s) (m', s')
instance LocalizedModule.instZero {R : Type u} [] {S : } {M : Type v} [] [Module R M] :
Zero ()
Equations
• LocalizedModule.instZero = { zero := }
theorem LocalizedModule.subsingleton {R : Type u} [] {S : } {M : Type v} [] [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} [] {S : } {M : Type v} [] [Module R M] (s : S) :
= 0
instance LocalizedModule.instAdd {R : Type u} [] {S : } {M : Type v} [] [Module R M] :
Equations
• LocalizedModule.instAdd = { add := fun (p1 p2 : ) => p1.liftOn₂ p2 (fun (x y : M × S) => LocalizedModule.mk (y.2 x.1 + x.2 y.1) (x.2 * y.2)) }
theorem LocalizedModule.mk_add_mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] {m1 : M} {m2 : M} {s1 : S} {s2 : S} :
+ = LocalizedModule.mk (s2 m1 + s1 m2) (s1 * s2)
instance LocalizedModule.hasNatSMul {R : Type u} [] {S : } {M : Type v} [] [Module R M] :
Equations
• LocalizedModule.hasNatSMul = { smul := fun (n : ) => }
instance LocalizedModule.instAddCommMonoid {R : Type u} [] {S : } {M : Type v} [] [Module R M] :
Equations
instance LocalizedModule.instNeg {R : Type u} [] {S : } {M : Type u_2} [] [Module R M] :
Neg ()
Equations
• LocalizedModule.instNeg = { neg := fun (p : ) => p.liftOn (fun (x : M × S) => LocalizedModule.mk (-x.1) x.2) }
instance LocalizedModule.instAddCommGroup {R : Type u} [] {S : } {M : Type u_2} [] [Module R M] :
Equations
• LocalizedModule.instAddCommGroup = let __src := let_fun this := inferInstance; this;
theorem LocalizedModule.mk_neg {R : Type u} [] {S : } {M : Type u_2} [] [Module R M] {m : M} {s : S} :
=
instance LocalizedModule.instMonoid {R : Type u} [] {A : Type u_2} [] [Algebra R A] {S : } :
Equations
• LocalizedModule.instMonoid = Monoid.mk npowRec
instance LocalizedModule.instSemiring {R : Type u} [] {A : Type u_2} [] [Algebra R A] {S : } :
Equations
• LocalizedModule.instSemiring = let __src := let_fun this := inferInstance; this; let __src_1 := let_fun this := inferInstance; this; Semiring.mk Monoid.npow
instance LocalizedModule.instCommSemiring {R : Type u} [] {A : Type u_2} [] [Algebra R A] {S : } :
Equations
• LocalizedModule.instCommSemiring = let __src := let_fun this := inferInstance; this;
instance LocalizedModule.instRing {R : Type u} [] {A : Type u_2} [Ring A] [Algebra R A] {S : } :
Ring ()
Equations
• One or more equations did not get rendered due to their size.
instance LocalizedModule.instCommRing {R : Type u} [] {A : Type u_2} [] [Algebra R A] {S : } :
Equations
• LocalizedModule.instCommRing = let __src := let_fun this := inferInstance; this;
theorem LocalizedModule.mk_mul_mk {R : Type u} [] {S : } {A : Type u_2} [] [Algebra R A] {a₁ : A} {a₂ : A} {s₁ : S} {s₂ : S} :
* = LocalizedModule.mk (a₁ * a₂) (s₁ * s₂)
noncomputable instance LocalizedModule.instSMul {R : Type u} [] {S : } {M : Type v} [] [Module R M] (T : Type u_1) [] [Algebra R T] [] :
SMul T ()
Equations
• One or more equations did not get rendered due to their size.
theorem LocalizedModule.smul_def {R : Type u} [] {S : } {M : Type v} [] [Module R M] (T : Type u_1) [] [Algebra R T] [] (x : T) (m : M) (s : S) :
x = LocalizedModule.mk (().1 m) (().2 * s)
theorem LocalizedModule.mk'_smul_mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] (T : Type u_1) [] [Algebra R T] [] (r : R) (m : M) (s : S) (s' : S) :
= LocalizedModule.mk (r m) (s * s')
theorem LocalizedModule.mk_smul_mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] (r : R) (m : M) (s : S) (t : S) :
= LocalizedModule.mk (r m) (s * t)
noncomputable instance LocalizedModule.isModule {R : Type u} [] {S : } {M : Type v} [] [Module R M] {T : Type u_1} [] [Algebra R T] [] :
Module T ()
Equations
• LocalizedModule.isModule =
@[simp]
theorem LocalizedModule.mk_cancel_common_left {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s' : S) (s : S) (m : M) :
LocalizedModule.mk (s' m) (s' * s) =
@[simp]
theorem LocalizedModule.mk_cancel {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) (m : M) :
@[simp]
theorem LocalizedModule.mk_cancel_common_right {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) (s' : S) (m : M) :
LocalizedModule.mk (s' m) (s * s') =
noncomputable instance LocalizedModule.isModule' {R : Type u} [] {S : } {M : Type v} [] [Module R M] :
Module R ()
Equations
theorem LocalizedModule.smul'_mk {R : Type u} [] {S : } {M : Type v} [] [Module R M] (r : R) (s : S) (m : M) :
theorem LocalizedModule.smul'_mul {R : Type u} [] {S : } {T : Type u_1} [] [Algebra R T] [] {A : Type u_2} [] [Algebra R A] (x : T) (p₁ : ) (p₂ : ) :
x p₁ * p₂ = x (p₁ * p₂)
theorem LocalizedModule.mul_smul' {R : Type u} [] {S : } {T : Type u_1} [] [Algebra R T] [] {A : Type u_2} [] [Algebra R A] (x : T) (p₁ : ) (p₂ : ) :
p₁ * x p₂ = x (p₁ * p₂)
noncomputable instance LocalizedModule.instAlgebra {R : Type u} [] {S : } (T : Type u_1) [] [Algebra R T] [] {A : Type u_2} [] [Algebra R A] :
Algebra T ()
Equations
theorem LocalizedModule.algebraMap_mk' {R : Type u} [] {S : } (T : Type u_1) [] [Algebra R T] [] {A : Type u_2} [] [Algebra R A] (a : R) (s : S) :
(algebraMap T ()) () = LocalizedModule.mk (() a) s
theorem LocalizedModule.algebraMap_mk {R : Type u} [] {S : } {A : Type u_2} [] [Algebra R A] (a : R) (s : S) :
(algebraMap () ()) () = LocalizedModule.mk (() a) s
instance LocalizedModule.instIsScalarTower {R : Type u} [] {S : } {M : Type v} [] [Module R M] (T : Type u_1) [] [Algebra R T] [] :
Equations
• =
noncomputable instance LocalizedModule.algebra' {R : Type u} [] {S : } {A : Type u_2} [] [Algebra R A] :
Algebra R ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LocalizedModule.mkLinearMap_apply {R : Type u} [] (S : ) (M : Type v) [] [Module R M] (m : M) :
m =
def LocalizedModule.mkLinearMap {R : Type u} [] (S : ) (M : Type v) [] [Module R M] :

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

Equations
• = { toFun := fun (m : M) => , map_add' := , map_smul' := }
Instances For
@[simp]
theorem LocalizedModule.divBy_apply {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) (p : ) :
= p.liftOn (fun (p : M × S) => LocalizedModule.mk p.1 (p.2 * s))
def LocalizedModule.divBy {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) :

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

Equations
• = { toFun := fun (p : ) => p.liftOn (fun (p : M × S) => LocalizedModule.mk p.1 (p.2 * s)) , map_add' := , map_smul' := }
Instances For
theorem LocalizedModule.divBy_mul_by {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) (p : ) :
(((algebraMap R (Module.End R ())) s) p) = p
theorem LocalizedModule.mul_by_divBy {R : Type u} [] {S : } {M : Type v} [] [Module R M] (s : S) (p : ) :
((algebraMap R (Module.End R ())) s) () = p
theorem isLocalizedModule_iff {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') :
(∀ (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} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [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} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [self : ] (x : S) :
IsUnit ((algebraMap R (Module.End R M')) x)
theorem IsLocalizedModule.surj' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [self : ] (y : M') :
∃ (x : M × S), x.2 y = f x.1
theorem IsLocalizedModule.exists_of_eq {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [self : ] {x₁ : M} {x₂ : M} :
f x₁ = f x₂∃ (c : S), c x₁ = c x₂
theorem IsLocalizedModule.surj {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (y : M') :
∃ (x : M × S), x.2 y = f x.1
theorem IsLocalizedModule.eq_iff_exists {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {x₁ : M} {x₂ : M} :
f x₁ = f x₂ ∃ (c : S), c x₁ = c x₂
theorem IsLocalizedModule.of_linearEquiv {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (e : M' ≃ₗ[R] M'') [hf : ] :
IsLocalizedModule S (e ∘ₗ f)
theorem isLocalizedModule_id {R : Type u_1} [] (S : ) (M : Type u_2) [] [Module R M] (R' : Type u_6) [] [Algebra R R'] [] [Module R' M] [IsScalarTower R R' M] :
IsLocalizedModule S LinearMap.id
theorem isLocalizedModule_iff_isLocalization {R : Type u_1} [] {S : } {A : Type u_6} {Aₛ : Type u_7} [] [Algebra R A] [] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] :
IsLocalizedModule S ().toLinearMap
instance instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid {R : Type u_1} [] (S : ) {A : Type u_6} {Aₛ : Type u_7} [] [Algebra R A] [] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] [h : ] :
IsLocalizedModule S ().toLinearMap
Equations
• =
theorem isLocalizedModule_iff_isLocalization' {R : Type u_1} [] (S : ) (R' : Type u_6) [] [Algebra R R'] :
IsLocalizedModule S (Algebra.ofId R R').toLinearMap
noncomputable def LocalizedModule.lift' {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
M''

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
• = m.liftOn (fun (p : M × S) => .unit⁻¹ (g p.1))
Instances For
theorem LocalizedModule.lift'_mk {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [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) :
= .unit⁻¹ (g m)
theorem LocalizedModule.lift'_add {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (x : ) (y : ) :
LocalizedModule.lift' S g h (x + y) = +
theorem LocalizedModule.lift'_smul {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (r : R) (m : ) :
noncomputable def LocalizedModule.lift {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
→ₗ[R] M''

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
• = { toFun := , map_add' := , map_smul' := }
Instances For
theorem LocalizedModule.lift_mk {R : Type u_1} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [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) :
() () = .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} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
∘ₗ = g

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} [] (S : ) {M : Type u_2} {M'' : Type u_4} [] [] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (l : →ₗ[R] M'') (hl : l ∘ₗ = g) :
= l

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

instance localizedModuleIsLocalizedModule {R : Type u_1} [] (S : ) {M : Type u_2} [] [Module R M] :
Equations
• =
noncomputable def IsLocalizedModule.fromLocalizedModule' {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
M'

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

Equations
• = p.liftOn (fun (x : M × S) => .unit⁻¹ (f x.1))
Instances For
@[simp]
theorem IsLocalizedModule.fromLocalizedModule'_mk {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
= .unit⁻¹ (f m)
theorem IsLocalizedModule.fromLocalizedModule'_add {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (x : ) (y : ) :
theorem IsLocalizedModule.fromLocalizedModule'_smul {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (r : R) (x : ) :
=
noncomputable def IsLocalizedModule.fromLocalizedModule {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :

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

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
theorem IsLocalizedModule.fromLocalizedModule_mk {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
= .unit⁻¹ (f m)
theorem IsLocalizedModule.fromLocalizedModule.inj {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
theorem IsLocalizedModule.fromLocalizedModule.surj {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
theorem IsLocalizedModule.fromLocalizedModule.bij {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
@[simp]
theorem IsLocalizedModule.iso_apply {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
∀ (a : ),
@[simp]
theorem IsLocalizedModule.iso_symm_apply {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
∀ (a : M'), ().symm a = .symm a
noncomputable def IsLocalizedModule.iso {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :

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.
Instances For
theorem IsLocalizedModule.iso_apply_mk {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
() () = .unit⁻¹ (f m)
theorem IsLocalizedModule.iso_symm_apply_aux {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M') :
().symm m = LocalizedModule.mk .choose.1 .choose.2
theorem IsLocalizedModule.iso_symm_apply' {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M') (a : M) (b : S) (eq1 : b m = f a) :
().symm m =
theorem IsLocalizedModule.iso_symm_comp {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
().symm ∘ₗ f =
noncomputable def IsLocalizedModule.lift {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (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
• = ∘ₗ ().symm
Instances For
theorem IsLocalizedModule.lift_comp {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
∘ₗ f = g
@[simp]
theorem IsLocalizedModule.lift_apply {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (x : M) :
() (f x) = g x
theorem IsLocalizedModule.lift_unique {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (g : M →ₗ[R] M'') (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) (l : M' →ₗ[R] M'') (hl : l ∘ₗ f = g) :
= l
theorem IsLocalizedModule.is_universal {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (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} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [] (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} [] (S : ) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [] [] [] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [] [] :
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
• = ().symm.trans ()
Instances For
theorem IsLocalizedModule.smul_injective {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (s : S) :
Function.Injective fun (m : M') => s m
theorem IsLocalizedModule.smul_inj {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (s : S) (m₁ : M') (m₂ : M') :
s m₁ = s m₂ m₁ = m₂
noncomputable def IsLocalizedModule.mk' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
M'

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

Equations
Instances For
theorem IsLocalizedModule.mk'_smul {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (r : R) (m : M) (s : S) :
theorem IsLocalizedModule.mk'_add_mk' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
+ = IsLocalizedModule.mk' f (s₂ m₁ + s₁ m₂) (s₁ * s₂)
@[simp]
theorem IsLocalizedModule.mk'_zero {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (s : S) :
= 0
@[simp]
theorem IsLocalizedModule.mk'_one {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) :
= f m
@[simp]
theorem IsLocalizedModule.mk'_cancel {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
@[simp]
theorem IsLocalizedModule.mk'_cancel' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
s = f m
@[simp]
theorem IsLocalizedModule.mk'_cancel_left {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s₁ : S) (s₂ : S) :
IsLocalizedModule.mk' f (s₁ m) (s₁ * s₂) =
@[simp]
theorem IsLocalizedModule.mk'_cancel_right {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s₁ : S) (s₂ : S) :
IsLocalizedModule.mk' f (s₂ m) (s₁ * s₂) =
theorem IsLocalizedModule.mk'_add {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m₁ : M) (m₂ : M) (s : S) :
IsLocalizedModule.mk' f (m₁ + m₂) s = +
theorem IsLocalizedModule.mk'_eq_mk'_iff {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
= ∃ (s : S), s s₁ m₂ = s s₂ m₁
theorem IsLocalizedModule.mk'_neg {R : Type u_1} [] {S : } {M : Type u_6} {M' : Type u_7} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m : M) (s : S) :
= -
theorem IsLocalizedModule.mk'_sub {R : Type u_1} [] {S : } {M : Type u_6} {M' : Type u_7} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m₁ : M) (m₂ : M) (s : S) :
IsLocalizedModule.mk' f (m₁ - m₂) s = -
theorem IsLocalizedModule.mk'_sub_mk' {R : Type u_1} [] {S : } {M : Type u_6} {M' : Type u_7} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
- = IsLocalizedModule.mk' f (s₂ m₁ - s₁ m₂) (s₁ * s₂)
theorem IsLocalizedModule.mk'_mul_mk'_of_map_mul {R : Type u_1} [] {S : } {M : Type u_6} {M' : Type u_7} [] [Semiring M'] [Module R M] [Algebra R M'] (f : M →ₗ[R] M') (hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂) [] (m₁ : M) (m₂ : M) (s₁ : S) (s₂ : S) :
* = IsLocalizedModule.mk' f (m₁ * m₂) (s₁ * s₂)
theorem IsLocalizedModule.mk'_mul_mk' {R : Type u_1} [] {S : } {M : Type u_6} {M' : Type u_7} [] [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} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [] {m : M} {s : S} {m' : M'} :
= m' f m = s m'

Porting note (#10618): simp can prove this @[simp]

@[simp]
theorem IsLocalizedModule.mk'_eq_zero {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [] {m : M} (s : S) :
= 0 f m = 0
theorem IsLocalizedModule.mk'_eq_zero' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {m : M} (s : S) :
= 0 ∃ (s' : S), s' m = 0
theorem IsLocalizedModule.mk_eq_mk' {R : Type u_1} [] {S : } {M : Type u_2} [] [Module R M] (s : S) (m : M) :
theorem IsLocalizedModule.mk'_smul_mk' {R : Type u_1} [] {S : } {M : Type u_2} {M' : Type u_3} [] [] (A : Type u_5) [] [Algebra R A] [Module A M'] [] [Module R M] [Module R M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [] (x : R) (m : M) (s : S) (t : S) :
theorem IsLocalizedModule.eq_zero_iff {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {m : M} :
f m = 0 ∃ (s' : S), s' m = 0
theorem IsLocalizedModule.mk'_surjective {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] :
noncomputable def IsLocalizedModule.map {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {N : Type u_6} {N' : Type u_7} [] [] [Module R N] [Module R N'] (g : N →ₗ[R] N') [] :
(M →ₗ[R] N) →ₗ[R] M' →ₗ[R] N'

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

Equations
Instances For
theorem IsLocalizedModule.map_comp {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {N : Type u_6} {N' : Type u_7} [] [] [Module R N] [Module R N'] (g : N →ₗ[R] N') [] (h : M →ₗ[R] N) :
() h ∘ₗ f = g ∘ₗ h
@[simp]
theorem IsLocalizedModule.map_apply {R : Type u_1} [] (S : ) {M : Type u_2} {M' : Type u_3} [] [] [Module R M] [Module R M'] (f : M →ₗ[R] M') [] {N : Type u_6} {N' : Type u_7} [] [] [Module R N] [Module R N'] (g : N →ₗ[R] N') [] (h : M →ₗ[R] N) (x : M) :
(() h) (f x) = g (h x)
theorem IsLocalizedModule.mkOfAlgebra {R : Type u_6} {S : Type u_7} {S' : Type u_8} [] [] [CommRing S'] [Algebra R S] [Algebra R S'] (M : ) (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