Pull-back of a marked triple up to unit boundary members

The second clause of [Kol07, 34.1] and the convention [Kol07, 32]: along an arbitrary smooth h : Y → X the rounds of Steps 1 and 2 of the proof of [Kol07, Theorem 107] whose parameters exceed those of Y pull back to empty blow-ups, which are deleted; their exceptional divisors survive as unit members of the boundary of the pulled-back data. The invariant of the loops is therefore not the exact pull-back relation T'.IsPullbackOf T h but its version up to unit members: T' has the structure morphism, the ideal and the mark of the pull-back of T, and its boundary is the pull-back boundary with unit-ideal members deleted (IsTopErasure; the fourth conjunct of the skipped-round lemma pullback_eraseEmpty_eq_nil_of_maxOrd_lt of Hironaka/Resolution/Algebraic/MarkedOrderReduction/SkippedRound.lean produces exactly this). This module collects the bookkeeping of that relation.

• The split of [Kol07, Definition–Lemma 110] ignores unit members (DivisorFamily.monomial_of_extendsByEmpty in Hironaka/Resolution/Algebraic/MarkedOrderReduction/MonomialExtendsByEmpty.lean: a unit member has no irreducible components, so its factor in the monomial ideal is 1), hence so do M(I), N(I) and the round parameters (nonmonomialPart_of_extendsByEmpty, roundOrder_fullPullback, sepOrder_fullPullback).
• The full pull-back fullPullback T' T h, the boundary restored to h^{-1} E, is an exact pull-back (fullPullback_isPullbackOf), and its round triple is the round triple of T' with unit members appended (nonmonomialTriple_fullPullback), the shape in which the indifference of the input functors and the second clause of [Kol07, 34.1] for [Kol07, Theorem 103] apply.
• The relation passes to the marked triples induced at the end of the erased pull-back of a sequence of order ≥ m, along eraseEmptyLastHom ≫ pullbackLastHom (IsPullbackOfUpToUnits.induced_eraseEmpty): the ideal by the transport of the induced triple along the last-stage lift and the erasure identity markedTransformSeq_eraseEmpty_last (Hironaka/Resolution/Algebraic/Kol07/EraseEmptyInduced.lean), the boundary by eraseEmbeds_eraseEmpty composed with exists_isTopErasure_totalTransformSeq.

These facts drive the functoriality of the loops for an arbitrary smooth morphism (Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothLoop.lean).

theorem Hironaka.BMO.monomialPart_of_extendsByEmpty {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {E' E : X.DivisorFamily} (hext : AlgebraicGeometry.ExtendsByEmpty E' E) : monomialPart I E = monomialPart I E'

The monomial part ignores unit members ([Kol07, Definition–Lemma 110] with the convention [Kol07, 32]).

theorem Hironaka.BMO.nonmonomialPart_of_extendsByEmpty {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {E' E : X.DivisorFamily} (hext : AlgebraicGeometry.ExtendsByEmpty E' E) : nonmonomialPart I E = nonmonomialPart I E'

The nonmonomial part ignores unit members.

def Hironaka.MarkedTriple.IsPullbackOfUpToUnits {k : Type u} [Field k] (T' T : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) : Prop

T' is the pull-back of T along h up to unit boundary members (the second clause of [Kol07, 34.1] with the convention [Kol07, 32]): the structure morphism, the ideal and the mark of T' are those of the pull-back, and its boundary is the pull-back boundary h^{-1} E with unit-ideal members deleted (IsTopErasure). The exact pull-back is the case of no deletion; the data after a skipped round are the case of the deleted exceptional divisors.

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.MarkedTriple.IsPullbackOf.upToUnits {k : Type u} [Field k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} (hp : T'.IsPullbackOf T h) : T'.IsPullbackOfUpToUnits T h

An exact pull-back is a pull-back up to unit members (no deletion).

theorem Hironaka.MarkedTriple.isPullbackOfUpToUnits_id {k : Type u} [Field k] (T : MarkedTriple k) (E' : T.X.left.DivisorFamily) (hsnc' : E'.IsSnc) (e : E'.ι ↪o T.E.ι) (hmem : ∀ (i : E'.ι), T.E.component (e i) = E'.component i) (htop : ∀ b ∉ Set.range ⇑e, T.E.component b = ⊤) : { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hsnc', m := T.m }.IsPullbackOfUpToUnits T (CategoryTheory.CategoryStruct.id T.X.left)

Deleting unit members of the boundary is a pull-back up to unit members along the identity (the shape of IndifferentToEmptyMembers).

theorem Hironaka.MarkedTriple.Triple_mk_I_congr {k : Type u} [Field k] (T₀ : AlgebraicGeometry.Triple k) {J₁ J₂ : T₀.X.left.IdealSheafData} (e : J₁ = J₂) (h₁ : J₁.IsNonzeroEverywhere) (h₂ : J₂.IsNonzeroEverywhere) : { X := T₀.X, smoothOfRelativeDimension := ⋯, I := J₁, isNonzeroEverywhere := h₁, E := T₀.E, isSnc := ⋯ } = { X := T₀.X, smoothOfRelativeDimension := ⋯, I := J₂, isNonzeroEverywhere := h₂, E := T₀.E, isSnc := ⋯ }

Two triples differing only in the ideal are equal when the ideals are.

noncomputable def Hironaka.MarkedTriple.fullPullback {k : Type u} [Field k] [CharZero k] (T' T : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] : MarkedTriple k

The full pull-back: T' with its boundary restored to the whole pull-back boundary h^{-1} E, which has normal crossings by isSnc_comap_of_smooth.

Equations

• T'.fullPullback T h = { X := T'.X, smoothOfRelativeDimension := ⋯, I := T'.I, isNonzeroEverywhere := ⋯, E := T.E.comap h, isSnc := ⋯, m := T'.m }

theorem Hironaka.MarkedTriple.fullPullback_isPullbackOf {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : (T'.fullPullback T h).IsPullbackOf T h

The full pull-back of a pull-back up to unit members is an exact pull-back.

theorem Hironaka.MarkedTriple.fullPullback_bmoClass {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] {n m : ℕ} (hT' : BMOClass n m T') : BMOClass n m (T'.fullPullback T h)

The full pull-back is in the class when T' is (the class does not see the boundary).

theorem Hironaka.MarkedTriple.isTopErasure_fullPullback {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : ∃ (e : T'.E.ι ↪o (T'.fullPullback T h).E.ι), Sequence.IsTopErasure T'.E (T'.fullPullback T h).E e

The boundary of T' is the boundary of its full pull-back with unit members deleted.

theorem Hironaka.MarkedTriple.nonmonomialPart_fullPullback {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.nonmonomialPart (T'.fullPullback T h).I (T'.fullPullback T h).E = BMO.nonmonomialPart T'.I T'.E

The nonmonomial part of the full pull-back is that of T': unit members are ignored.

theorem Hironaka.MarkedTriple.nonmonomialPart_eq_comap_of_upToUnits {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.nonmonomialPart T'.I T'.E = (BMO.nonmonomialPart T.I T.E).comap h

The nonmonomial part of T' is the inverse image of that of T, through the full pull-back and nonmonomialPart_comap.

theorem Hironaka.MarkedTriple.roundOrder_fullPullback {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.roundOrder (T'.fullPullback T h) = BMO.roundOrder T'

The round parameter of Step 1 for the full pull-back is that of T'.

theorem Hironaka.MarkedTriple.sepOrder_fullPullback {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.sepOrder (T'.fullPullback T h) = BMO.sepOrder T'

The separation parameter of Step 2 for the full pull-back is that of T'.

theorem Hironaka.MarkedTriple.nonmonomialTriple_fullPullback {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.nonmonomialTriple T' = let __src := T'.toTriple; { X := __src.X, smoothOfRelativeDimension := ⋯, I := BMO.nonmonomialPart (T'.fullPullback T h).I (T'.fullPullback T h).E, isNonzeroEverywhere := ⋯, E := __src.E, isSnc := ⋯ }

The round triple (Y, N(I'), E') of T' is the round triple of its full pull-back with the unit members deleted (the ideal N(I', h^{-1} E) = N(I', E')): the shape in which IndifferentToEmptyMembers applies to the input functor.

theorem Hironaka.MarkedTriple.IsPullbackOfUpToUnits.roundOrder_le {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.roundOrder T' ≤ BMO.roundOrder T

The round parameter of Step 1 does not grow under a smooth pull-back (the second clause of [Kol07, 34.1]): the order at a point is the order at its image.

theorem Hironaka.MarkedTriple.IsPullbackOfUpToUnits.sepOrder_le {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : BMO.sepOrder T' ≤ BMO.sepOrder T

The separation parameter of Step 2 does not grow under a smooth pull-back (the second clause of [Kol07, 34.1]).

theorem Hironaka.MarkedTriple.IsPullbackOfUpToUnits.induced_eraseEmpty {k : Type u} [Field k] [CharZero k] {T T' : MarkedTriple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) {S : T.X.left.BlowUpSequence} (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) (hP' : (S.pullback h).eraseEmpty.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E) : (T'.induced (S.pullback h).eraseEmpty hP' (Fin.last (S.pullback h).eraseEmpty.length)).IsPullbackOfUpToUnits (T.induced S hS (Fin.last S.length)) (CategoryTheory.CategoryStruct.comp (S.pullback h).eraseEmptyLastHom (S.pullbackLastHom h))

The relation up to unit members passes to the induced marked triples at the end of the erased pull-back of a smooth blow-up sequence of order ≥ m (the second clause of [Kol07, 34.1] with [Kol07, Definition 66]), along the last-stage isomorphism followed by the last-stage lift: the ideal by the transport of the induced triple along the last-stage lift (isPullbackOf_induced_last on the full pull-back) and the erasure identity (markedTransformSeq_eraseEmpty_last), the boundary by eraseEmbeds_eraseEmpty composed with the transport of the deletion along the sequence (exists_isTopErasure_totalTransformSeq).

theorem Hironaka.MarkedTriple.isPullbackOfUpToUnits_induced_of_eq_seq {k : Type u} [Field k] [CharZero k] {T' : MarkedTriple k} {S S' : T'.X.left.BlowUpSequence} (e : S = S') {hS : S.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E} {hS' : S'.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E} {R : MarkedTriple k} {q : S'.last ⟶ R.X.left} (hq : (T'.induced S' hS' (Fin.last S'.length)).IsPullbackOfUpToUnits R q) : (T'.induced S hS (Fin.last S.length)).IsPullbackOfUpToUnits R (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) q)

Transport of the relation up to unit members of the last induced marked triple along an equality of sequences: the eqToHom of the last-stage identification is absorbed.