The data of Lemma 102 are indifferent to empty boundary members

Kollár's convention ignores empty blow-ups ([Kol07, 32]) and reindexes after deleting them (the second bullet of [Kol07, 34.1]); for the functor data of this library the corresponding property is BDFamily.IndifferentToEmptyMembers (Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferent.lean): deleting empty (unit-ideal) members of the boundary, with the distinguished position carried along, does not change the value. This module proves it for the data bdData n m j Dom B (hDom m) hB hsm hbc of AssemblyTuned.lean, at every mark, GIVEN the same indifference of the inductive input B (the marked form OrderGeSeqAssignment.IndifferentToEmptyMembers). The statement is a bookkeeping property of the construction, not in the sources.

• At the mark 0 (bdDataZero, zeroFunctor) the value is π_{-1} at the distinguished member E^j, which the position clause identifies with E'^{j'} (handled inline in bdData_indifferentToEmptyMembers).
• At m + 1 (dataFunctor, Lemma 102 through the re-tuning) the value is, on the tuned triple, the erased raw sequence of Output.lean: π_{-1} on S = E^j followed by B on the restricted marked triple (X_S, I_0|_S, m, E_S), pushed forward along S ↪ X (rawSeq). The restricted triple depends on the boundary through the distinguished member E^j (the scheme S, the centre, the push-forward) and through the erased family E − E^j (its boundary only). We separate the two: restrictedTripleD T m D F and rawSeqD T m D F of Restriction.lean take the member D and the family F as parameters (restrictedTriple T m j is restrictedTripleD T m (E^j) (E − E^j)). The position clause gives E'^{j'} = E^j, so the two members agree and the dependence on D is a substitution (rawSeqD_congr_D); the embedding e restricts to E' − E'^{j'} ↪o E − E^j with ⊤ complement (eraseEmb, isTopErasure_erase), preserved by the inverse image along S ↪ X and the total transform along Z_{-1}|_S (the transport lemmas of IsTopErasure), so B's indifference identifies the two values on the restricted triples (rawSeqD_congr_F); the first blow-up, the push-forward and the deletion of empty blow-ups are then the same (functor_seq_indifferent, dataFunctor_seq_indifferent).

Used by Hironaka/Resolution/Algebraic/OrderReduction/Step3Data.lean.

theorem Hironaka.BD.RestrictedHyps.congr {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (I : X.IdealSheafData) (m : ℕ) (F : X.DivisorFamily) {D₁ D₂ : X.IdealSheafData} (hD : D₂ = D₁) (h : RestrictedHyps f I m D₂ F) : RestrictedHyps f I m D₁ F

Transport of the facts along an equality of members.

theorem Hironaka.BD.rawSeqD_congr_D {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsSeparated f] (I : X.IdealSheafData) (m : ℕ) (F : X.DivisorFamily) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) {D₁ D₂ : X.IdealSheafData} (hD : D₂ = D₁) (h₂ : RestrictedHyps f I m D₂ F) (h₁ : RestrictedHyps f I m D₁ F) (hdom₂ : Dom (restrictedTripleD f I m D₂ F h₂)) (hdom₁ : Dom (restrictedTripleD f I m D₁ F h₁)) : rawSeqD f I m D₂ F B h₂ hdom₂ = rawSeqD f I m D₁ F B h₁ hdom₁

The raw output depends on the member only through its value (a substitution).

theorem Hironaka.BD.rawSeqD_congr_F {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsSeparated f] (I : X.IdealSheafData) (m : ℕ) (D : X.IdealSheafData) {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) {F₁ F₂ : X.DivisorFamily} (e : F₂.ι ↪o F₁.ι) (he : Sequence.IsTopErasure F₂ F₁ e) (hBind : B.IndifferentToEmptyMembers) (h₁ : RestrictedHyps f I m D F₁) (h₂ : RestrictedHyps f I m D F₂) (hdom₁ : Dom (restrictedTripleD f I m D F₁ h₁)) (hdom₂ : Dom (restrictedTripleD f I m D F₂ h₂)) : rawSeqD f I m D F₂ B h₂ hdom₂ = rawSeqD f I m D F₁ B h₁ hdom₁

The raw output is indifferent to ⊤ members of the erased family: the boundaries of the two restricted triples differ by a deletion of ⊤ members (the inverse image along D ↪ X and the total transform along Z_{-1}|_D of the deletion), so B's indifference identifies B's values; the first blow-up and the push-forward are the same.

noncomputable def Hironaka.BD.eraseEmb {X : AlgebraicGeometry.Scheme} {E E' : X.DivisorFamily} (e : E'.ι ↪o E.ι) {j : E.ι} {j' : E'.ι} (hj : e j' = j) : (E'.erase j').ι ↪o (E.erase j).ι

The restriction of a ⊤-deletion embedding to the erased families: E' − E'^{j'} ↪o E − E^j when e j' = j.

Equations

• Hironaka.BD.eraseEmb e hj = OrderEmbedding.ofMapLEIff (fun (i : (E'.erase j').ι) => ⟨e ↑i, ⋯⟩) ⋯

theorem Hironaka.BD.isTopErasure_erase {X : AlgebraicGeometry.Scheme} {E E' : X.DivisorFamily} {e : E'.ι ↪o E.ι} (he : Sequence.IsTopErasure E' E e) {j : E.ι} {j' : E'.ι} (hj : e j' = j) : Sequence.IsTopErasure (E'.erase j') (E.erase j) (eraseEmb e hj)

A deletion of ⊤ members restricts to a deletion of ⊤ members of the erased families.

theorem Hironaka.BD.functor_seq_indifferent {k : Type u} [Field k] [CharZero k] {n m : ℕ} {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = m → Dom T') (hBind : B.IndifferentToEmptyMembers) (T : AlgebraicGeometry.Triple k) (E' : T.X.left.DivisorFamily) (hsnc' : E'.IsSnc) (e : E'.ι ↪o T.E.ι) (hc : ∀ (i : E'.ι), T.E.component (e i) = E'.component i) (ht : ∀ b ∉ Set.range ⇑e, T.E.component b = ⊤) {j j' : ℕ} (hj : j < Fintype.card T.E.ι) (hj' : j' < Fintype.card E'.ι) (hpos : e (E'.nthIdx ⟨j', hj'⟩) = T.E.nthIdx ⟨j, hj⟩) (hT : Domain n m j T) (hT' : Domain n m j' { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hsnc' }) : (functor n m j B hDom).seq T hT = (functor n m j' B hDom).seq { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hsnc' } hT'

The functor of Output.lean at position j is indifferent to ⊤ members of the boundary ([Kol07, 32]): for a deletion e of ⊤ members carrying the position j' of E' to the position j of E, the values at (X, I, E) and (X, I, E') agree: the distinguished members agree, so the first blow-up and the push-forward are the same (rawSeqD_congr_D), and B's indifference handles the erased families (rawSeqD_congr_F).

theorem Hironaka.BD.dataFunctor_seq_indifferent {k : Type u} [Field k] [CharZero k] {n m : ℕ} {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (hm : 1 ≤ m) (hDom : ∀ (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom T') (hBind : B.IndifferentToEmptyMembers) (T : AlgebraicGeometry.Triple k) (E' : T.X.left.DivisorFamily) (hsnc' : E'.IsSnc) (e : E'.ι ↪o T.E.ι) (hc : ∀ (i : E'.ι), T.E.component (e i) = E'.component i) (ht : ∀ b ∉ Set.range ⇑e, T.E.component b = ⊤) {j j' : ℕ} (hj : j < Fintype.card T.E.ι) (hj' : j' < Fintype.card E'.ι) (hpos : e (E'.nthIdx ⟨j', hj'⟩) = T.E.nthIdx ⟨j, hj⟩) (hT : AlgebraicGeometry.Triple.BDClass n m j T) (hT' : AlgebraicGeometry.Triple.BDClass n m j' { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hsnc' }) : (dataFunctor n m j hm B hDom).seq T hT = (dataFunctor n m j' hm B hDom).seq { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hsnc' } hT'

The data of [Kol07, Lemma 102] at the mark m ≥ 1 through the re-tuning (dataFunctor) are indifferent to ⊤ members: both sides tune the same ideal, so both are the functor of Output.lean on the tuned triple, or both are empty below the mark.

theorem Hironaka.BD.bdData_indifferentToEmptyMembers {n : ℕ} (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (hBind : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).IndifferentToEmptyMembers) (m : ℕ) : BDFamily.IndifferentToEmptyMembers fun (j : ℕ) => bdData n m j Dom B ⋯ hB hsm hbc

The data bdData of [Kol07, Lemma 102] are indifferent to empty boundary members at every mark ([Kol07, 32]; the second bullet of [Kol07, 34.1]), given that the inductive data B are.