Completed ideals of principal stalks under automorphisms of the completion

In the proof of Theorem 92 ([Kol07, 95]) Kollár notes: "By construction φ(Ĥ) = Ĥ', φ(Êⁱ) = Êⁱ". With H_p = (x₁), H'_p = (x₁') and φ^*(x₁') = x₁, the completed ideal Ĥ' = (ι x₁') is carried to (ι x₁) = Ĥ (map_completionIdeal_eq_of_stalkIdeal_eq_span); with Eⁱ_p = (y_{c(i)}) and φ^*(y_{c(i)}) = y_{c(i)} the completed ideal of a component through p is fixed (the same lemma with a = b); and for a component not through p the stalk, hence the completed ideal, is the unit ideal (completionIdeal_eq_top_of_notMem_support), fixed by every ring map. Everything is the behaviour of Ideal.map on a principal ideal: (a).map φ = (φ a).

theorem AlgebraicGeometry.Scheme.IdealSheafData.completionIdeal_eq_top_of_notMem_support {X : Scheme} (J : X.IdealSheafData) {p : ↥X} (hp : p ∉ J.support) : J.completionIdeal p = ⊤

For a component not through p the completed ideal is the unit ideal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.completionIdeal_eq_span_of_stalkIdeal_eq_span {X : Scheme} {J : X.IdealSheafData} {p : ↥X} {a : ↑(X.presheaf.stalk p)} (h : J.stalkIdeal p = Ideal.span {a}) : J.completionIdeal p = Ideal.span {(algebraMap (↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))) a}

The completion of an ideal sheaf whose stalk is principal is principal, generated by the image of the generator.

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_completionIdeal_eq_of_stalkIdeal_eq_span {X : Scheme} {p : ↥X} (J J' : X.IdealSheafData) {a b : ↑(X.presheaf.stalk p)} (hJ : J.stalkIdeal p = Ideal.span {a}) (hJ' : J'.stalkIdeal p = Ideal.span {b}) {F : Type u_1} [FunLike F (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))] [RingHomClass F (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))] (φ : F) (hφ : φ ((algebraMap (↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))) a) = (algebraMap (↑(X.presheaf.stalk p)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk p)) ↑(X.presheaf.stalk p))) b) : Ideal.map φ (J.completionIdeal p) = J'.completionIdeal p

Kollár's "By construction φ(Ĥ) = Ĥ', φ(Êⁱ) = Êⁱ" ([Kol07, 95]): if J_p = (a), J'_p = (b) and a ring map φ of the completion sends ι a to ι b, then φ(Ĵ) = Ĵ'.