Theorems · Definition · commutative algebra
LocalizedModule.equivTensorProduct
{R : Type u_1} →
[inst : CommSemiring R] →
(S : Submonoid R) →
(M : Type u_3) →
[inst_1 : AddCommMonoid M] →
[inst_2 : Module R M] → LocalizedModule S M ≃ₗ[Localization S] TensorProduct R (Localization S) MThe localization of an R-module M at a submonoid S is isomorphic to S⁻¹R ⊗[R] M as
an S⁻¹R-module.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- LinearEquivstatement · cited by 3,317
- Submonoidstatement and proof · cited by 3,086
- TensorProductstatement · cited by 2,545
- LinearEquiv.symmproof · cited by 1,461
- Localizationstatement · cited by 270
- LocalizedModulestatement · cited by 154
- IsBaseChange.equivproof · cited by 27
- LocalizedModule.isBaseChangeproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- Module.rankAtStalk_baseChangeproof · cited by 4
- Module.rankAtStalk_eq_finrank_tensorProductproof · cited by 3
- LocalizedModule.equivTensorProduct_symm_apply_tmulstatement · cited by 2
- Ideal.finrank_fiber_eq_finrankproof · cited by 1
- LocalizedModule.equivTensorProduct_apply_mkstatement and proof · cited by 0
- LocalizedModule.equivTensorProduct_symm_apply_tmul_onestatement and proof · cited by 0
- Module.mem_support_iff_nontrivial_residueField_tensorProductproof · cited by 0