Theorems · Theorem · commutative algebra
IsLocalizedModule.map_linearMap_of_isLocalization
∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (Rₚ : Type u_5)
(Sₚ : Type u_6) [inst_3 : CommSemiring Rₚ] [inst_4 : Algebra R Rₚ] [inst_5 : CommSemiring Sₚ] [inst_6 : Algebra S Sₚ]
[inst_7 : Algebra R Sₚ] [inst_8 : IsScalarTower R S Sₚ] [inst_9 : Algebra Rₚ Sₚ] [inst_10 : IsScalarTower R Rₚ Sₚ]
(p : Ideal R) [inst_11 : p.IsPrime] [inst_12 : IsLocalization.AtPrime Rₚ p]
[inst_13 : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)],
(IsLocalizedModule.map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ))
(Algebra.linearMap R S) =
↑R (Algebra.linearMap Rₚ Sₚ)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHom.idstatement · cited by 18,349
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement · cited by 10,215
- Idealstatement and proof · cited by 4,748
- Algebra.algebraMapproof · cited by 4,706
- IsScalarTowerstatement and proof · cited by 3,896
- AlgHomstatement · cited by 3,236
- map_oneproof · cited by 861
- Ideal.IsPrimestatement and proof · cited by 827
- Ideal.primeComplstatement and proof · cited by 462
Cited by2
Results whose statement or proof uses this declaration.
- injective_of_isLocalization_isMaximalproof · cited by 2
- surjective_of_isLocalization_isMaximalproof · cited by 2