The weak transform of the bundled vocabulary

The vocabulary in which the main theorems are stated has its own weak transform AnalyticManifold.IdealSheaf.weakTransform f J D: the colon-stalk definition applied to a bundled analytic map f and an ideal sheaf D of the centre. For a blowing-up f with centre the closed submanifold Y and D the ideal sheaf of Y it is the unbundled IdealSheaf.weakTransformOf (an abbreviation of it) once D is identified with hY.idealSheaf (weakTransform_eq, the rewrite lemma used for the iterated transforms along a sequence of blowings-up), and it has the colon stalks whenever f is the monoidal transformation with centre D (isDivExceptional_weakTransform).

theorem Manifold.weakTransform_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {c : ℕ} {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) {Y : Set N.carrier} (hY : IsClosedSubmanifold ψ Y c) {D : N.IdealSheaf} (hD : IsIdealSheafOf ψ Y c D) (h : IsBlowUp ψ Y c ⇑f) (J : N.IdealSheaf) : AnalyticManifold.IdealSheaf.weakTransform f J D = IdealSheaf.weakTransformOf hY h J

For a blowing-up f with centre Y and D the ideal sheaf of Y, the bundled AnalyticManifold.IdealSheaf.weakTransform f J D is the unbundled weak transform.

theorem Manifold.isDivExceptional_weakTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N N' : AnalyticManifold 𝕜 E} (f : AnalyticMap N' N) (D J : N.IdealSheaf) (hf : f.IsMonoidalTransformation D) : (IdealSheaf.pullback ⇑f ⋯ J).IsDivExceptional (IdealSheaf.pullback ⇑f ⋯ D) (fun (a' : ↑↧N'.carrier) => (IdealSheaf.genericOrdAlong D J (f a')).toNat) (AnalyticManifold.IdealSheaf.weakTransform f J D)

When f is the monoidal transformation with centre D, the bundled weak transform has the colon stalks (f⁻¹(J)_{a'} : f⁻¹(D)_{a'}^{ν}), ν the generic order of J along the component of the centre through f a'.