Restriction of a blow-up sequence functor to a smaller class

Kollár's functors are defined on classes of triples (the class of [Kol07, Theorem 103] is the triples with dim X = n and max-ord I ≤ m); OrderSeqFunctor k m Dom carries its class Dom in its type, so the same assignment of sequences on a smaller class is a different term. The restriction of a functor along an inclusion of classes Dom' ⊆ Dom is the functor on Dom' with the same values; it inherits the order condition and the absence of empty blow-ups (the functor's fields) and the commutation with the surjections of a class of morphisms (hypothesis (3) of [Kol07, Theorem 105]). The tower of order reduction functors indexed by the dimension is compared stage against stage through such restrictions, using the uniqueness of the globalization of [Kol07, Theorem 105].

def Hironaka.OrderSeqAssignment.restrict {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (Dom' : AlgebraicGeometry.Triple k → Prop) (h : ∀ (T : AlgebraicGeometry.Triple k), Dom' T → Dom T) : OrderSeqAssignment k m Dom'

The restriction of a blow-up sequence functor of order m to a smaller class Dom' along the inclusion h : ∀ T, Dom' T → Dom T: the same sequences, the same fields.

Equations

• B.restrict Dom' h = { seq := fun (T : AlgebraicGeometry.Triple k) (hT : Dom' T) => B.seq T ⋯, isOrderSeq := ⋯, noEmptyCenters := ⋯ }

theorem Hironaka.OrderSeqAssignment.restrict_seq {k : Type u} [Field k] {m : ℕ} {Dom Dom' : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (h : ∀ (T : AlgebraicGeometry.Triple k), Dom' T → Dom T) (T : AlgebraicGeometry.Triple k) (hT : Dom' T) : (B.restrict Dom' h).seq T hT = B.seq T ⋯

The restricted functor has the same values.

theorem Hironaka.OrderSeqAssignment.restrict_commutesWithSurjectionsIn {k : Type u} [Field k] {m : ℕ} {Dom Dom' : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (h : ∀ (T : AlgebraicGeometry.Triple k), Dom' T → Dom T) (M : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hB : B.CommutesWithSurjectionsIn M) : (B.restrict Dom' h).CommutesWithSurjectionsIn M

A functor commuting with the surjections of a class of morphisms (hypothesis (3) of [Kol07, Theorem 105]) restricts to one: the same pairs, the class proofs carried along the inclusion.