English
Let R, S, T be commutative rings with S and T algebras over R, and g ∈ S. Suppose T is the localization of S away from g, and P represents a presentation of S by generators. If f ∈ P.Ring satisfies algebraMap P.Ring S f = g, then the kernel of the composed map ((Generators.localizationAway T g).comp P) equals the sum of the image of the kernel of P under the induced map and the principal ideal generated by rename f in the localization relation: rename Sum.inr f · X(Sum.inl()) − 1.
Русский
Пусть R, S, T — коммутативные кольца, S и T — алгебры над R, g ∈ S. Пусть T является локализацией S away от g, и P представляет презентацию S по генераторам. Пусть f ∈ P.Ring удовлетворяет algebraMap P.Ring S f = g. Тогда ядро композиции ((Generators.localizationAway T g).comp P) равно образу ядра P под соответствующим отображением плюс идеал, порожденный элементом rename f умноженным на X(Sum.inl()) минус единица: rename Sum.inr f · X(Sum.inl()) − 1.
LaTeX
$$$((Generators.localizationAway T g).comp P).ker = \\operatorname{map}(((Generators.localizationAway T g).toComp P).toAlgHom)\\,P.ker \\;\\sqcup\\; \\operatorname{span}\\{ \\operatorname{rename} (Sum.inr f) \\cdot X (Sum.inl()) - 1\\}$$$
Lean4
theorem comp_localizationAway_ker (P : Generators R S ι) (f : P.Ring) (h : algebraMap P.Ring S f = g) :
((Generators.localizationAway T g).comp P).ker =
Ideal.map ((Generators.localizationAway T g).toComp P).toAlgHom P.ker ⊔
Ideal.span {rename Sum.inr f * X (Sum.inl ()) - 1} :=
by
have :
(localizationAway T g).ker =
Ideal.map ((localizationAway T g).ofComp P).toAlgHom
(Ideal.span {MvPolynomial.rename Sum.inr f * MvPolynomial.X (Sum.inl ()) - 1}) :=
by
rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway, Hom.toAlgHom_X,
toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]
rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot, ← sup_assoc]
simp
