The trivial compatible-family functor

Kollár starts the induction with dim X = 0, where everything is resolved without blow-ups [Kol07, 70]. On the family layer the functor that resolves without blow-ups is the constant family functor whose value on every triple is the trivial compatible family (CompatibleFamily.nil: the empty list on every relatively compact open, compatibility by pullback_nil and eraseEmpty_nil), cut once for every class and model:

• AnalyticFamilyFunctor.nilFamilyFunctor ψ₀ Dom, the family functor T ↦ CompatibleFamily.nil T on the class Dom, with nilFamilyFunctor_fam and nilFamilyFunctor_seqOn (rfl);
• nilFamilyFunctor_isOfOrderGe: its value on every relatively compact open is (vacuously) a smooth blow-up sequence of order ≥ m at the restricted triple (isOfOrderGe_nil);
• nilFamilyFunctor_commutesWithLocalIsos, nilFamilyFunctor_indifferentToEmptyMembers: the two predicates of a family functor, by pullback_nil and eraseEmpty_nil (the pull-back of the empty list is the empty list, its eraseEmpty too) and by the value's independence of the triple.

The order clause "ord I_r < m at the end" is not general: it is the dimension-zero content of [Kol07, 70] (ord_lt_of_dim_zero) and lives with the base stage of the family tower (Hironaka.Resolution.Analytic.OrderReduction.Stage.Family).

noncomputable def Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) (Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom

The trivial family functor on a class Dom of triples at the model ψ₀ — every triple is sent to the trivial compatible family (CompatibleFamily.nil).

Equations

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

@[simp]

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_fam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom T) : (nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom).fam T hT = CompatibleFamily.nil T

@[simp]

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom).fam T hT).seqOn U hU = AnalyticManifold.BlowUpSequence.nil (M.restrict U)

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (m : ℕ) : (((nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom).fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I m (T.pullback (M.inclusion U) ⋯).F.idealSheaf

[Kol07, Definition 66] (2′)–(4′) for the trivial family functor, per relatively compact open: the empty sequence is (vacuously) a smooth blow-up sequence of order ≥ m starting with the restricted triple.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} : (nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom).CommutesWithLocalIsos

[Kol07, 34.1], both bullets, for the trivial family functor, per relatively compact open: the pull-back of the empty list is the empty list (pullback_nil), and so is its eraseEmpty (eraseEmpty_nil).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} : (nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom).IndifferentToEmptyMembers

Indifference to empty boundary members (not in the source) for the trivial family functor: its value does not depend on the boundary.