The marked transform of the centre and of the unit ideal

Two values of the marked transform π_*^{-1}(J, m) = (π^* J : F^m) of [Kol07, Definition 60]: the transform of the centre itself with mark 1 is the unit ideal, (F : F) = 𝒪 (markedTransform_self), and the transform of the unit ideal is the unit ideal, (𝒪 : F^m) = 𝒪 (markedTransform_top). They give the values along Σ in Kollár's Warning 63 on the model of Remark 33 (HironakaExamples/Sequence/Warning63.lean).

theorem Hironaka.Sequence.markedTransform_self {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) : Z.markedTransform Z 1 = ⊤

The marked transform of the center itself with mark 1 is the unit ideal: (F : F) = 𝒪.

theorem Hironaka.Sequence.markedTransform_top {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) (m : ℕ) : ⊤.markedTransform Z m = ⊤

The marked transform of the unit ideal is the unit ideal: (𝒪 : F^m) = 𝒪.