English
The square of the kernel of the composed localization map is contained in the kernel of the localization AlgHom, i.e., ker(comp)^2 ⊆ ker(compLocalizationAwayAlgHom).
Русский
Квадрат ядра композиции локализации содержится в ядре соответствующего алгебра-хома локализации.
LaTeX
$$((localizationAway T g).comp P).ker^2 \\leq RingHom.ker (compLocalizationAwayAlgHom T g P)$$
Lean4
theorem sq_ker_comp_le_ker_compLocalizationAwayAlgHom :
((localizationAway T g).comp P).ker ^ 2 ≤ RingHom.ker (compLocalizationAwayAlgHom T g P) :=
by
have hsple {x} (hx : x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1}) :
(compLocalizationAwayAlgHom T g P) x = 0 :=
by
obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton.mp hx
rw [map_mul, compLocalizationAwayAlgHom_relation_eq_zero, zero_mul]
rw [comp_localizationAway_ker _ _ (P.σ g) (by simp), sq, Ideal.sup_mul, Ideal.mul_sup, Ideal.mul_sup]
apply sup_le
· apply sup_le
· rw [← Ideal.map_mul, Ideal.map_le_iff_le_comap, ← sq]
intro x hx
simp only [Ideal.mem_comap, RingHom.mem_ker, compLocalizationAwayAlgHom_toAlgHom_toComp (T := T) g P x]
rw [IsScalarTower.algebraMap_apply P.Ring (P.Ring ⧸ P.ker ^ 2) (Localization.Away _),
Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem.mpr hx, map_zero]
· rw [Ideal.mul_le]
intro x hx y hy
simp [hsple hy]
·
apply sup_le <;>
· rw [Ideal.mul_le]
intro x hx y hy
simp [hsple hx]
