Tools for the maximal-contact step of CP1

Elementary bookkeeping for the step of the proof of CP1 (the statement of Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) that descends to the hypersurface of maximal contact (Step 2.2 of the proof of [Kol07, Theorem 103], the proof of [Kol07, Lemma 102]): snc with a closed subscheme restricts along an injection of families with equal members (HasSncWith.of_embeds) and depends on the subscheme only through its stalks at its points (HasSncWith.of_stalkIdeal_eq); generic points and the reducedness of I at them descend along a closed immersion (mem_genericPoints_comap_of_isClosedImmersion, stalkIdeal_comap_eq_vanishingIdeal_closure_of_eq); removing a member keeps a family snc (isSnc_erase); in E + J with J appended last, every index other than J's is an original index (exists_eq_inl_of_erase_append_last); and along a smooth order-1 sequence without empty blow-ups from a triple with max-ord I ≤ 1, a point on the marked transform's support forces max-ord I = 1 (maxOrd_eq_one_of_mem_support_markedTransformSeq; below the mark the sequence is empty, [Kol07, Theorem 68]). The coordinates are those of [Kol07, Definition 24]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22Core and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step22.

theorem Hironaka.Resolution.HasSncWith.of_embeds {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (e : E₁.ι → E₂.ι) (he : Function.Injective e) (hcomp : ∀ (a : E₁.ι), E₂.component (e a) = E₁.component a) {Z : X.IdealSheafData} (h : E₂.HasSncWith Z) : E₁.HasSncWith Z

Snc with Z restricts along an injection of families with equal members — the coordinates are the same, the members of E₁ through x corresponding to members of E₂ through x.

theorem Hironaka.Resolution.HasSncWith.of_stalkIdeal_eq {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {Z Z' : X.IdealSheafData} (h : E.HasSncWith Z) (hsupp : Z'.support ≤ Z.support) (hst : ∀ x ∈ Z'.support, Z'.stalkIdeal x = Z.stalkIdeal x) : E.HasSncWith Z'

Snc with Z depends on Z only through its stalks at its points — a closed subscheme Z' inside Z with the same stalks at its points has snc with E when Z does.

theorem Hironaka.Resolution.mem_genericPoints_comap_of_isClosedImmersion {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (I : X.IdealSheafData) {η' : ↥Y} (hη : g η' ∈ I.support.genericPoints) : η' ∈ (I.comap g).support.genericPoints

Generic points descend along a closed immersion — a point over a generic point of V(I) is a generic point of V(I|_Y) (the closed immersion is injective, so a generization in V(I|_Y) maps to a generization in V(I)).

theorem Hironaka.Resolution.stalkIdeal_comap_eq_vanishingIdeal_closure_of_eq {X Y : AlgebraicGeometry.Scheme} (g : Y ⟶ X) [AlgebraicGeometry.IsClosedImmersion g] (I : X.IdealSheafData) (η' : ↥Y) (hIc : I.stalkIdeal (g η') = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {g η'})).stalkIdeal (g η')) : (I.comap g).stalkIdeal η' = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η'})).stalkIdeal η'

The reducedness of I at a point descends along a closed immersion — if I_{g η'} is the reduced ideal of the closure of g η', then (I|_Y)_{η'} is the reduced ideal of the closure of η'.

theorem Hironaka.Resolution.isSnc_erase {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (j : E.ι) (hE : E.IsSnc) : (E.erase j).IsSnc

Removing a member keeps a family snc — the regularity of the members and the coordinates at every point are inherited.

theorem Hironaka.Resolution.exists_eq_inl_of_erase_append_last {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (J : X.IdealSheafData) (h : Fintype.card E.ι < Fintype.card (E.append J).ι) (b : ((E.append J).erase ((monoEquivOfFin (E.append J).ι ⋯) ⟨Fintype.card E.ι, h⟩)).ι) : ∃ (a : E.ι), ↑b = toLex (Sum.inl a)

In E + J with J appended last (position card E.ι, nth_append_last), every index other than J's is an original index.

theorem Hironaka.Resolution.maxOrd_eq_one_of_mem_support_markedTransformSeq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (_n : ℕ) {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} (hS : S.IsOrderSeq f I E 1) (hne : S.NoEmptyCenters) (hmax : I.maxOrd ≤ 1) {i : Fin (S.length + 1)} {η : ↥(S.stage i)} (hη : η ∈ (S.markedTransformSeq I 1 i).support) : I.maxOrd = ↑1

Along a smooth order-1 sequence without empty blow-ups from a triple with max-ord I ≤ 1, a point on the marked transform's support forces max-ord I = 1 — below the mark the sequence is empty (the remark after [Kol07, Theorem 68]: the case max-ord I < m is trivial) and the marked transform is I itself, which then has no point of order ≥ 1.