English
There is an algebra isomorphism between Localization.AtPrime p for a prime p of Localization M and Localization.AtPrime p in the composite setting, showing a canonical equivalence of prime localizations.
Русский
Существуют канонические алгебраические изоморфизмы между AtPrime p локализации M и соответствующей локализацией двойной структуры.
LaTeX
$$LocalizationAtPrime p ≃ₐ[R] Localization.AtPrime p$$
Lean4
theorem isFractionRing_of_isLocalization (S T : Type*) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
[Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T] (hM : M ≤ nonZeroDivisors R) :
IsFractionRing S T := by
have := isLocalization_of_submonoid_le S T M (nonZeroDivisors R) hM
refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_
· exact map_nonZeroDivisors_le M S
· rintro ⟨x, -, hx⟩
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x
use algebraMap R S s
rw [mul_comm, Subtype.coe_mk, e]
refine Set.mem_image_of_mem (algebraMap R S) (mem_nonZeroDivisors_iff_right.mpr ?_)
intro z hz
apply IsLocalization.injective S hM
rw [map_zero]
apply hx
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero, zero_mul]
