The trivial blow-up sequence functors

The structures OrderSeqFunctor and OrderGeSeqFunctor are inhabited: the trivial functor (X, I, E) ↦ nil X, assigning the empty blow-up sequence to every input, is a smooth blow-up sequence functor of every order m on every class of triples, and the trivial marked functor is a marked one on every class of marked triples. Both commute with every morphism in the sense of [Kol07, 34.1] (CommutesWith, CommutesWithSmooth), since the pullback of the empty sequence is the empty sequence; the examples record this.

The functoriality clause of [Kol07, 34.1] itself, and its locality, are proved in Hironaka/Scheme/BlowUpSequence/Functoriality.lean.

Pullback data and commuting with a morphism

Smooth surjections

Smooth morphisms, with deletion of the empty blow-ups

Locality of the functoriality clause

The order predicates along pullback data

The structures are inhabited: the trivial functor (X, I, E) ↦ nil X is a smooth blow-up

sequence functor of every order on every class, and it commutes with every morphism.

noncomputable def Hironaka.Sequence.trivialFunctor {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} : OrderSeqAssignment k m Dom

The trivial functor of order m: every input gets the empty sequence.

Equations

• Hironaka.Sequence.trivialFunctor = { seq := fun (T : AlgebraicGeometry.Triple k) (x : Dom T) => AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left, isOrderSeq := ⋯, noEmptyCenters := ⋯ }

noncomputable def Hironaka.Sequence.trivialGeFunctor {k : Type u} [Field k] {Dom' : MarkedTriple k → Prop} : OrderGeSeqAssignment k Dom'

The trivial marked functor.

Equations

• Hironaka.Sequence.trivialGeFunctor = { seq := fun (T : Hironaka.MarkedTriple k) (x : Dom' T) => AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left, isOrderGeSeq := ⋯, noEmptyCenters := ⋯ }