English
Under IsLocalization, the comap of the image of p under one map equals the pullback of pS under another map; i.e., comap(algebraMap S S_p) (p.map(algebraMap R S_p)) = pS.
Русский
При условии IsLocalization выполняется совместимость обратного образа: comap(algebraMap S S_p)(p.map(algebraMap R S_p)) = pS.
LaTeX
$$$(p.map (\\alpha)) .\\!\\! .comap (\\beta) = pS$$$
Lean4
theorem comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
(Ideal.map (algebraMap R Sₚ) p).comap (algebraMap S Sₚ) = pS :=
by
rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]
apply Ideal.le_comap_map.antisymm
intro x hx
obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS :=
by
have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
rw [← map_mul, IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
obtain ⟨c, hc⟩ := hy
obtain ⟨α, hα, e⟩ := (c * s).prop
refine ⟨α, hα, ?_⟩
rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
exact Ideal.mul_mem_left _ _ y.prop
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ :=
by
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
refine ⟨β, β * α - 1, ?_, ?_⟩
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, map_mul, hβ, inv_mul_cancel₀, sub_self]
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
· rw [add_sub_cancel]
have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this
refine (Submodule.add_mem_iff_left _ ?_).mp this
rw [Algebra.smul_def]
apply Ideal.mul_mem_right
exact Ideal.mem_map_of_mem _ hγ
