theorem LocalizedModule.map'_mk {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_4} [AddCommGroup N] [Module R N] (S : Submonoid R) (f : N →ₗ[R] M) (n : N) (s : ↥S) : ((map' S) f) (LocalizedModule.mk n s) = LocalizedModule.mk (f n) s

noncomputable def tensor_eqv_local {R : Type u_1} (M : Type u_2) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] : TensorProduct R (Localization S) M ≃ₗ[Localization S] LocalizedModule S M

Equations

• tensor_eqv_local M S = ⋯.equiv

noncomputable def eqv1 {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct R (TensorProduct R (Localization S) M) N ≃ₗ[R] LocalizedModule S (TensorProduct R M N)

Equations

• eqv1 M N S = (TensorProduct.assoc R (Localization S) M N).trans (LinearEquiv.restrictScalars R (tensor_eqv_local (TensorProduct R M N) S))

noncomputable def eqv2 {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct R (TensorProduct (Localization S) (TensorProduct R (Localization S) M) (Localization S)) N ≃ₗ[R] TensorProduct R (TensorProduct R (Localization S) M) N

Equations

• eqv2 M N S = TensorProduct.congr (LinearEquiv.restrictScalars R (TensorProduct.rid (Localization S) (TensorProduct R (Localization S) M))) (LinearEquiv.refl R N)

noncomputable def eqv3 {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct (Localization S) (TensorProduct R (Localization S) M) (TensorProduct R (Localization S) N) ≃ₗ[Localization S] TensorProduct R (TensorProduct (Localization S) (TensorProduct R (Localization S) M) (Localization S)) N

Equations

• eqv3 M N S = (TensorProduct.AlgebraTensorModule.assoc R (Localization S) (Localization S) (TensorProduct R (Localization S) M) (Localization S) N).symm

noncomputable def eqv4 {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[Localization S] TensorProduct (Localization S) (TensorProduct R (Localization S) M) (TensorProduct R (Localization S) N)

Equations

• eqv4 M N S = TensorProduct.congr (tensor_eqv_local M S).symm (tensor_eqv_local N S).symm

noncomputable def eqv' {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[R] LocalizedModule S (TensorProduct R M N)

Equations

• eqv' M N S = (LinearEquiv.restrictScalars R (eqv4 M N S)).trans ((LinearEquiv.restrictScalars R (eqv3 M N S)).trans ((eqv2 M N S).trans (eqv1 M N S)))

noncomputable def lmap {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) →ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Equations

• lmap M N S = LinearMap.extendScalarsOfIsLocalization S (Localization S) ↑(eqv' M N S)

noncomputable def rmap {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : LocalizedModule S (TensorProduct R M N) →ₗ[Localization S] TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N)

Equations

• rmap M N S = LinearMap.extendScalarsOfIsLocalization S (Localization S) ↑(eqv' M N S).symm

noncomputable def eqv {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Equations

• eqv M N S = LinearEquiv.ofLinear (lmap M N S) (rmap M N S) ⋯ ⋯

theorem tensor_eqv_local_apply {R : Type u_1} (M : Type u_2) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] (m : M) (sm : ↥S) (r : R) : (tensor_eqv_local M S) (Localization.mk r sm ⊗ₜ[R] m) = LocalizedModule.mk (r • m) sm

theorem tensor_eqv_local_symm_apply {R : Type u_1} (M : Type u_2) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] (m : M) (sm : ↥S) : (tensor_eqv_local M S).symm (LocalizedModule.mk m sm) = Localization.mk 1 sm ⊗ₜ[R] m

theorem eqv'_mk_apply {R : Type u_1} (M : Type u_2) (N : Type u_3) [CommRing R] (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {sm : ↥S} {sn : ↥S} (m : M) (n : N) : (eqv' M N S) (LocalizedModule.mk m sm ⊗ₜ[Localization S] LocalizedModule.mk n sn) = LocalizedModule.mk (m ⊗ₜ[R] n) (sm * sn)

theorem Flat_of_localization {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Module.Flat (Localization.AtPrime J) (LocalizedModule.AtPrime J M)) : Module.Flat R M

theorem Flat_of_localization_finitespan {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (s : Finset R) (spn : Ideal.span ↑s = ⊤) (h : ∀ (r : { x : R // x ∈ s }), Module.Flat (Localization (Submonoid.powers ↑r)) (LocalizedModule (Submonoid.powers ↑r) M)) : Module.Flat R M

instance instFlatLocalization_moduleLocalProperties (R : Type u_1) [CommRing R] (S : Submonoid R) : Module.Flat R (Localization S)

Equations

• ⋯ = ⋯

theorem IsLocalization.Flat (R : Type u_1) (R' : Type u_2) [CommRing R] [CommRing R'] [Algebra R R'] (S : Submonoid R) [IsLocalization S R'] : Module.Flat R R'

theorem flat_iff_localization (R : Type u_1) (R' : Type u_2) [CommRing R] [CommRing R'] [Algebra R R'] (S : Submonoid R) [IsLocalization S R'] {M' : Type u_3} [AddCommGroup M'] [Module R M'] [Module R' M'] [IsScalarTower R R' M'] : Module.Flat R' M' ↔ Module.Flat R M'

noncomputable instance instModuleAtPrimeComapRingHomAlgebraMapAtPrime {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module A M] (J : Ideal A) [J.IsPrime] : Module (Localization.AtPrime (Ideal.comap (algebraMap R A) J)) (LocalizedModule.AtPrime J M)

Equations

• instModuleAtPrimeComapRingHomAlgebraMapAtPrime J = Module.compHom (LocalizedModule.AtPrime J M) (Localization.localRingHom (Ideal.comap (algebraMap R A) J) J (algebraMap R A) ⋯)

theorem flatiff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] : Module.Flat R M ↔ ∀ (J : Ideal A) (hJ : J.IsMaximal), Module.Flat (Localization.AtPrime (Ideal.comap (algebraMap R A) J)) (LocalizedModule.AtPrime J M)