Theorem 88: the chart missing the strict transform of the hypersurface

In the proof of [Kol07, Theorem 88], only r − 1 of the charts of the blow-up have the displayed form, but "these r − 1 charts, however, completely cover S_1": the chart whose distinguished coordinate is the equation y_ρ of S misses the strict transform S_1. In the chart description of the stalk of the blow-up at a point q ∈ B_Z X over z ∈ Z with S_z = (y_ρ), the stalk of S_1 at q is the saturation ⋃ᵢ (π^* S_z : F_qⁱ) of the total transform by the exceptional ideal (stalkIdeal_saturate_of_isInvertible), where π^* S_z = (π^♯ y_ρ) = F_q (stalkIdeal_comap_eq_span_of_chart); so 1 ∈ (F_q : F_q) and (S_1)_q = 𝒪_{B,q}. This is the observation in the proof of [Kol07, Lemma 62] that the remaining chart "does not contain any point of the birational transform".

theorem Hironaka.Sequence.stalkIdeal_strictTransform_eq_top_of_pivot {X : AlgebraicGeometry.Scheme} (Z S : X.IdealSheafData) (q : ↥Z.blowUp) {n' : ℕ} (y : Fin n' → ↑(X.presheaf.stalk (Z.blowUpπ q))) (ρ : Fin n') (hZ' : Z.stalkIdeal (Z.blowUpπ q) = IsLocalRing.chartCenter y ρ) (hSz : S.stalkIdeal (Z.blowUpπ q) = Ideal.span {y ρ}) (𝔮 : Ideal ↥(IsLocalRing.chartRing y ρ)) [𝔮.IsPrime] (e : ↑(Z.blowUp.presheaf.stalk q) ≃+* Localization.AtPrime 𝔮) (he : ∀ (a : ↑(X.presheaf.stalk (Z.blowUpπ q))), e ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) a) = (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk (Z.blowUpπ q)) ↥(IsLocalRing.chartRing y ρ)) a)) : (S.strictTransform Z).stalkIdeal q = ⊤

In the chart description of the stalk at q ∈ B_Z X over z ∈ Z, when the distinguished coordinate y_ρ is the local equation of S (S_z = (y_ρ)), the strict transform of S misses q: (S_1)_q = 𝒪_{B,q} (the proofs of [Kol07, Lemma 62 and Theorem 88]).