English
Equivalence between a localized spanSingleton product and a product of spans of x and y with ideals.
Русский
Эквиваленция между локализованным произведением spanSingleton и произведением spanSingleton по x и y с идеалами.
LaTeX
$$spanSingleton R₁⁰ (IsLocalization.mk' K x ⟨y, hy⟩) * I = (J : FractionalIdeal R₁⁰ K) ↔ Ideal.span { x } * I = Ideal.span { y } * J$$
Lean4
theorem mk'_mul_coeIdeal_eq_coeIdeal {I J : Ideal R₁} {x y : R₁} (hy : y ∈ R₁⁰) :
spanSingleton R₁⁰ (IsLocalization.mk' K x ⟨y, hy⟩) * I = (J : FractionalIdeal R₁⁰ K) ↔
Ideal.span { x } * I = Ideal.span { y } * J :=
by
have : spanSingleton R₁⁰ (IsLocalization.mk' _ (1 : R₁) ⟨y, hy⟩) * spanSingleton R₁⁰ (algebraMap R₁ K y) = 1 := by
rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_self,
spanSingleton_one]
let y' : (FractionalIdeal R₁⁰ K)ˣ := Units.mkOfMulEqOne _ _ this
have coe_y' : ↑y' = spanSingleton R₁⁰ (IsLocalization.mk' K (1 : R₁) ⟨y, hy⟩) := rfl
refine Iff.trans ?_ (y'.mul_right_inj.trans coeIdeal_inj)
rw [coe_y', coeIdeal_mul, coeIdeal_span_singleton, coeIdeal_mul, coeIdeal_span_singleton, ← mul_assoc,
spanSingleton_mul_spanSingleton, ← mul_assoc, spanSingleton_mul_spanSingleton, mul_comm (mk' _ _ _), ←
IsLocalization.mk'_eq_mul_mk'_one, mul_comm (mk' _ _ _), ← IsLocalization.mk'_eq_mul_mk'_one,
IsLocalization.mk'_self, spanSingleton_one, one_mul]
