English
If M ≤ N are submonoids of R, then the localization of N in T along the map R → S yields IsLocalization (Submonoid.map(algebraMap R S) N) T, i.e., localization respects submonoid inclusions.
Русский
Если M ≤ N — подмонойды R, локализация N в T остается локализацией по отображению R → S.
LaTeX
$$IsLocalization (Submonoid.map (algebraMap R S) N) T$$
Lean4
/-- If `M ≤ N` are submonoids of `R`, then `N⁻¹S` is also the localization of `M⁻¹S` at `N`. -/
theorem isLocalization_of_submonoid_le (M N : Submonoid R) (h : M ≤ N) [IsLocalization M S] [IsLocalization N T]
[Algebra S T] [IsScalarTower R S T] : IsLocalization (N.map (algebraMap R S)) T
where
map_units := by
rintro ⟨_, ⟨y, hy, rfl⟩⟩
convert IsLocalization.map_units T ⟨y, hy⟩
exact (IsScalarTower.algebraMap_apply _ _ _ _).symm
surj
y := by
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y
refine ⟨⟨algebraMap R S x, _, _, s.prop, rfl⟩, ?_⟩
simpa [← IsScalarTower.algebraMap_apply] using e
exists_of_eq
{x₁ x₂} := by
obtain ⟨⟨y₁, s₁⟩, e₁⟩ := IsLocalization.surj M x₁
obtain ⟨⟨y₂, s₂⟩, e₂⟩ := IsLocalization.surj M x₂
refine (Set.exists_image_iff (algebraMap R S) N fun c => c * x₁ = c * x₂).mpr.comp ?_
dsimp only at e₁ e₂ ⊢
suffices
algebraMap R T (y₁ * s₂) = algebraMap R T (y₂ * s₁) →
∃ a : N, algebraMap R S (a * (y₁ * s₂)) = algebraMap R S (a * (y₂ * s₁))
by
have h₁ :=
@IsUnit.mul_left_inj T _ _ (algebraMap S T x₁) (algebraMap S T x₂)
(IsLocalization.map_units T ⟨(s₁ : R), h s₁.prop⟩)
have h₂ :=
@IsUnit.mul_left_inj T _ _ ((algebraMap S T x₁) * (algebraMap R T s₁))
((algebraMap S T x₂) * (algebraMap R T s₁)) (IsLocalization.map_units T ⟨(s₂ : R), h s₂.prop⟩)
simp only [IsScalarTower.algebraMap_apply R S T] at h₁ h₂
simp only [IsScalarTower.algebraMap_apply R S T, map_mul, ← e₁, ← e₂, ← mul_assoc,
mul_right_comm _ (algebraMap R S s₂), (IsLocalization.map_units S s₁).mul_left_inj,
(IsLocalization.map_units S s₂).mul_left_inj] at this
rw [h₂, h₁] at this
simpa only [mul_comm] using this
simp_rw [IsLocalization.eq_iff_exists N T, IsLocalization.eq_iff_exists M S]
intro ⟨a, e⟩
exact ⟨a, 1, by convert e using 1 <;> simp⟩
