Two general lemmas for Definition 66

Two facts used to check the clauses of [Kol07, Definition 66] for a blow-up sequence, first on the model of Kollár's Warning 63 (HironakaExamples/Sequence/Remark33Warning63.lean) and later in the library:

• hasSncWith_empty_of_smooth: the empty family has simple normal crossings with every smooth center (adapted parameters, exists_adaptedParameters_of_smooth; [Kol07, Definition 24] for E = ∅);
• leOrdAlong_one_of_le: ord_Z I ≥ 1 whenever I ≤ Z (the order along Z of [Kol07, Definition 47] is the order at its generic points).

Two general lemmas for Definition 66

theorem Hironaka.Sequence.hasSncWith_empty_of_smooth {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] : (AlgebraicGeometry.Scheme.DivisorFamily.empty X).HasSncWith Z

The empty family has simple normal crossings with every smooth center: at a point of the center, adapted parameters (exists_adaptedParameters_of_smooth) are a regular system of parameters an initial segment of which generates the center ([Kol07, Definition 24] for E = ∅).

theorem Hironaka.Sequence.leOrdAlong_one_of_le {X : AlgebraicGeometry.Scheme} {I Z : X.IdealSheafData} (h : I ≤ Z) : I.LeOrdAlong Z.support ↑1

ord_Z I ≥ 1 when I ≤ Z (the order along Z of [Kol07, Definition 47] is the order at its generic points): every generic point of Z lies in the support of I.