Functors and local analytic isomorphisms: general tools

Tools for the passage from local to global in the proof of [Kol07, Theorem 103], placed here, downstream of the pull-back, deletion-of-empty-members and order-along-a-centre modules, because they need all of them:

• the two-summand disjoint union N ⊔ M (sumFamily, sumDesc, sumInl and their lemmas), the device by which an arbitrary local analytic isomorphism h : N → M becomes the composite of an open embedding with a surjective local isomorphism, and the two-piece union f ⊔ g of two maps (sumDesc₂), the cover used for the functoriality clauses of the descended functor;
• [Kol07, 34.1] for an arbitrary local analytic isomorphism, up to the deletion of empty blow-ups (CommutesWithLocalIsos.seq_pullback_eq_eraseEmpty), the analytic counterpart of etaleEquivSeq_of_functor for schemes (Hironaka.Resolution.Algebraic.MaximalContact.EtaleEquivSeqFunctor);
• the lifts of a local isomorphism along a centre list (BlowUpSequence.mem_range_pullbackLift_of_stageMap_mem, BlowUpSequence.noEmptyCenters_pullback_of_subset_range, the counterpart of noEmptyCenters_pullback_of_centersInRange for schemes, and BlowUpSequence.centers_subset_range_pullbackLiftAux);
• along a sequence of order ≥ m: points of order ≥ m lie over points of order ≥ m (IsOfOrderGe.le_ord_stageMap, the counterpart of le_ord_stageMap_of_mem_center for schemes) and the sequence is of order ≥ 1 for the marked maximal-contact ideal (IsOfOrderGe.isMarkedOne).

The two-summand disjoint union N ⊔ M

@[reducible, inline]

abbrev Hironaka.Manifold.sumFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (N M : AnalyticManifold 𝕜 E) : ULift.{u, 0} Bool → AnalyticManifold 𝕜 E

The two-summand family N ⊔ M, indexed by the lifted booleans (true ↦ N, false ↦ M).

Equations

• Hironaka.Manifold.sumFamily N M b = bif b.down then N else M

The two-piece union f ⊔ g (general tools)

def Hironaka.Manifold.sumDesc₂ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ M : AnalyticManifold 𝕜 E} (f : AnalyticMap N₁ M) (g : AnalyticMap N₂ M) (b : ULift.{u, 0} Bool) : AnalyticMap (sumFamily N₁ N₂ b) M

The map f ⊔ g : N₁ ⊔ N₂ → M on the summands of sumFamily N₁ N₂ (true ↦ N₁, false ↦ N₂; sumDesc with two maps).

Equations

• Hironaka.Manifold.sumDesc₂ f g b = Bool.rec g f b.down

theorem Hironaka.Manifold.sumDesc₂_true {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ M : AnalyticManifold 𝕜 E} (f : AnalyticMap N₁ M) (g : AnalyticMap N₂ M) : sumDesc₂ f g { down := true } = f

The first piece of the two-piece coproduct map is f.

theorem Hironaka.Manifold.isLocalDiffeomorph_sumDesc₂ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ M : AnalyticManifold 𝕜 E} {f : AnalyticMap N₁ M} {g : AnalyticMap N₂ M} (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (b : ULift.{u, 0} Bool) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(sumDesc₂ f g b)

The two-piece coproduct map of two local analytic isomorphisms is a family of local analytic isomorphisms (the hypothesis of isSigmaOf_pullback_sigmaDescMap).

theorem Hironaka.Manifold.iUnion_range_sumDesc₂ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N₁ N₂ M : AnalyticManifold 𝕜 E} (f : AnalyticMap N₁ M) {g : AnalyticMap N₂ M} (hgs : Function.Surjective ⇑g) : ⋃ (b : ULift.{u, 0} Bool), Set.range ⇑(sumDesc₂ f g b) = Set.univ

The two pieces cover M as soon as the second does (the cover g of the triple is surjective).

def Hironaka.Manifold.sumDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (b : ULift.{u, 0} Bool) : AnalyticMap (sumFamily N M b) M

The map h ⊔ id_M : N ⊔ M → M on the summands. The body is the instance sumDesc₂ h ContMDiffMap.id of the two-map form, definitionally Bool.rec (motive := fun c => AnalyticMap (cond c N M) M) ContMDiffMap.id h b.down.

Equations

• Hironaka.Manifold.sumDesc h = Hironaka.Manifold.sumDesc₂ h ContMDiffMap.id

theorem Hironaka.Manifold.isLocalDiffeomorph_sumDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} {h : AnalyticMap N M} (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (b : ULift.{u, 0} Bool) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(sumDesc h b)

theorem Hironaka.Manifold.iUnion_range_sumDesc {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) : ⋃ (b : ULift.{u, 0} Bool), Set.range ⇑(sumDesc h b) = Set.univ

theorem Hironaka.Manifold.sumDesc_true {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) : sumDesc h { down := true } = h

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.sumInl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} : AnalyticMap N (Manifold.sigmaManifold (sumFamily N M))

The inclusion of the summand N into N ⊔ M.

Equations

• Hironaka.Manifold.sumInl = Manifold.sigmaMk (Hironaka.Manifold.sumFamily N M) { down := true }

[Kol07, 34.1] for a local isomorphism, from the two clauses of CommutesWithLocalIsos

theorem Manifold.AnalyticBlowUpSequenceAssignment.CommutesWithLocalIsos.seq_pullback_eq_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ M → Prop} {B : AnalyticBlowUpSequenceAssignment ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} {M N : AnalyticManifold 𝕜 E} (hB : B.CommutesWithLocalIsos) (T : AnalyticTriple ψ₀ M) (hT : Dom T) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hT' : Dom (T.pullback h hh)) (hTsum : Dom (T.pullback (sigmaDescMap (Hironaka.Manifold.sumDesc h)) ⋯)) : B.seq (T.pullback h hh) hT' = ((B.seq T hT).pullback h hh).eraseEmpty

A functor commuting with surjective local isomorphisms and with open embeddings commutes with h up to the deletion of empty blow-ups, whenever the pull-backs along h and along h ⊔ id_M : N ⊔ M → M lie in its class — h = (h ⊔ id_M) ∘ inl with inl an open embedding and h ⊔ id_M a surjective local isomorphism; the analytic counterpart of etaleEquivSeq_of_functor for schemes (Hironaka.Resolution.Algebraic.MaximalContact.EtaleEquivSeqFunctor).

Centres of a sequence of order ≥ m lie over the cosupport, and the lifts cover

theorem AnalyticManifold.BlowUpSequence.mem_range_pullbackLift_of_stageMap_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) (p : (L.toSuccession.stage ⟨i, hi⟩).carrier) : (L.toSuccession.stageMapAux i hi) p ∈ Set.range ⇑h → p ∈ Set.range ⇑(L.pullbackLiftAux h hh i hi hi')

A point of a stage of L whose composite blow-down lies in the image of the local isomorphism h lies in the image of the lift of h to that stage — exists_liftStep_eq at each step.

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_pullback_of_subset_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : L.NoEmptyCenters → (∀ (i : ℕ) (hi : i < L.length) (hi' : i < (L.pullback h hh).length + 1), Manifold.IdealSheaf.support (L.toSuccession.center ⟨i, hi⟩) ⊆ Set.range ⇑(L.pullbackLiftAux h hh i ⋯ hi')) → (L.pullback h hh).NoEmptyCenters

The pull-back of a list with no empty centre along a local analytic isomorphism whose lifts cover the centres has no empty centre — the counterpart of noEmptyCenters_pullback_of_centersInRange (Hironaka.Scheme.BlowUpSequence.CentersCosupport).

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.le_ord_stageMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (hge : S.IsOfOrderGe I m E₀) (i : Fin (S.length + 1)) (x : (S.stage i).carrier) (hx : ↑m ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq I m i) x) : ↑m ≤ Manifold.IdealSheaf.ord I ((S.stageMap i) x)

As in the proof of [Kol07, Theorem 97]: along a smooth blow-up sequence of order ≥ m for (𝓘, m), a point of order ≥ m for the marked transform at stage i lies over a point of order ≥ m for 𝓘 — over the centre the order along the centre is ≥ m, off the centre the marked transform is the pull-back of the previous one along a local isomorphism — the analytic counterpart of le_ord_stageMap_of_mem_center for schemes (Hironaka.Scheme.BlowUpSequence.CentersCosupport).

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.isMarkedOne {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (hm : 1 ≤ m) (hge : S.IsOfOrderGe I m E₀) : S.IsMarkedOne (Manifold.IdealSheaf.iteratedDeriv I (m - 1))

By the derivative inequality of [Kol07, Corollary 77] (markedTransformSeq_iteratedDeriv_le_of_forall_lt with j = m − 1): a smooth blow-up sequence of order ≥ m for (𝓘, m) is of order ≥ 1 for (MC(𝓘), 1) in the containment form — each centre lies in cosupp(𝓘_i, m) = supp D^{m-1}(𝓘_i), which lies in the support of the marked transform of (MC(𝓘), 1).

theorem AnalyticManifold.BlowUpSequence.centers_subset_range_pullbackLiftAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : L.toSuccession.IsOfOrderGe I m E₀) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hcov : {x : ↑↧M.carrier | ↑m ≤ Manifold.IdealSheaf.ord I x} ⊆ Set.range ⇑h) (i : ℕ) (hi : i < L.length) (hi' : i < (L.pullback h hh).length + 1) : Manifold.IdealSheaf.support (L.toSuccession.center ⟨i, hi⟩) ⊆ Set.range ⇑(L.pullbackLiftAux h hh i ⋯ hi')

The centres of a list of order ≥ m for (𝓘, m) lie in the images of the lifts of a local analytic isomorphism whose image contains cosupp(𝓘, m).