Analytic blow-up sequences: recursions, constructors, trivial and empty blow-ups

Basic lemmas on a finite sequence of monoidal transformations FiniteSuccession and on the constructors FiniteSuccession.nil and FiniteSuccession.cons:

• the accessors satisfy the clauses of [Kol07, Definition 29] definitionally (X_0 = M, Π_0 = id, Π_{i+1} = Π_i ∘ π_i, Π = Π_r), and the constructor lemmas are rfl because cons puts the head in front of the fields of rest by Fin.cases over finStages;
• the centre C_i is the ideal sheaf of its cosupport Z_i (idealSheaf_center), so the witnesses chosen from isMonoidal do not enter it;
• equality of sequences built by cons is equality of centres (the sense in which a sequence is identified with its centres, [Kol07, Warning 20]): the first centre of a cons is the ideal sheaf of its submanifold, whose cosupport is that submanifold, and the tail is recovered field by field from the structure equality (FiniteSuccession.mk.injEq, Fin.cases_succ);
• trivial and empty blow-ups [Kol07, Warning 20]: an empty centre has empty cosupport, so its blowing-up is an isomorphism (IsBlowUp.exists_diffeomorph_of_empty at the witnesses of isMonoidal), as is the blowing-up along a centre of codimension one (exists_diffeomorph_of_codim_one); the exceptional divisor of an empty blow-up is empty;
• the recursions of the weak and marked transforms [Kol07, Definition 66 (1), (1′)] are definitional, and the constructor form of the weak-transform recursion follows by induction on the stage.

theorem AnalyticManifold.FiniteSuccession.stage_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : S.stage 0 = M

theorem AnalyticManifold.FiniteSuccession.stage_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : S.stage i.succ = S.later i

theorem AnalyticManifold.FiniteSuccession.stageMap_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : S.stageMap 0 = ContMDiffMap.id

theorem AnalyticManifold.FiniteSuccession.stageMap_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : S.stageMap i.succ = ContMDiffMap.comp (S.stageMap i.castSucc) (S.map i)

theorem AnalyticManifold.FiniteSuccession.composite_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) : S.composite = S.stageMap (Fin.last S.length)

@[simp]

theorem AnalyticManifold.FiniteSuccession.idealSheaf_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : ⋯.idealSheaf = S.center i

The centre C_i is the ideal sheaf idealSheaf of the closed submanifold Z_i = cosupp C_i (by the uniqueness of the ideal sheaf of a closed submanifold): the witnesses chosen from isMonoidal i do not enter the value.

The cosupport of the unit ideal sheaf and the empty centre

@[simp]

theorem Manifold.IdealSheaf.support_top {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} : ⊤.support = ∅

The unit ideal sheaf has empty cosupport.

theorem Manifold.IdealSheaf.eq_top_of_support_eq_empty {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {J : IdealSheaf 𝒪} (h : J.support = ∅) : J = ⊤

An ideal sheaf with empty cosupport is the unit ideal sheaf.

theorem Manifold.isIdealSheafOf_empty_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (ψ : E ≃L[𝕜] Fin n → 𝕜) (c : ℕ) : IsIdealSheafOf ψ ∅ c ⊤

The unit ideal sheaf is the ideal sheaf of the empty submanifold of any codimension.

theorem AnalyticManifold.FiniteSuccession.isEmptyAt_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : S.IsEmptyAt i ↔ Manifold.IdealSheaf.support (S.center i) = ∅

theorem AnalyticManifold.FiniteSuccession.IsEmptyAt.isTrivialAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {i : Fin S.length} (h : S.IsEmptyAt i) : S.IsTrivialAt i

theorem AnalyticManifold.FiniteSuccession.IsEmptyAt.exists_diffeomorph_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {i : Fin S.length} (h : S.IsEmptyAt i) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (S.stage i.succ).carrier (S.stage i.castSucc).carrier ⊤), ∀ (p : (S.stage i.succ).carrier), g p = (S.map i) p

theorem AnalyticManifold.FiniteSuccession.cons_codimOne_exists_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y 1) : ∃ (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (Manifold.blowUp ψ hY).carrier M.carrier ⊤), ∀ (p : (Manifold.blowUp ψ hY).carrier), g p = (Manifold.blowUpπ ψ hY) p

theorem AnalyticManifold.FiniteSuccession.mem_exceptionalAt_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) (p : (S.stage i.succ).carrier) : p ∈ S.exceptionalAt i ↔ (S.map i) p ∈ Manifold.IdealSheaf.support (S.center i)

theorem AnalyticManifold.FiniteSuccession.IsEmptyAt.exceptionalAt_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {i : Fin S.length} (h : S.IsEmptyAt i) : S.exceptionalAt i = ∅

Equality of sequences is equality of centres

def AnalyticManifold.FiniteSuccession.firstCenterSupport {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} : M.FiniteSuccession → Set M.carrier

The support of the first centre, as a function of the sequence (empty for the empty sequence), so that it can be applied to both sides of an equality of sequences.

Equations

• { length := 0, later := later, center := center, map := map, isMonoidal := isMonoidal }.firstCenterSupport = ∅
• { length := n.succ, later := later, center := center, map := map, isMonoidal := isMonoidal }.firstCenterSupport = Manifold.IdealSheaf.support (center 0)

theorem AnalyticManifold.FiniteSuccession.firstCenterSupport_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) : (cons ψ hY rest).firstCenterSupport = Y

theorem AnalyticManifold.FiniteSuccession.center_zero_eq_of_cons_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c n' : ℕ} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {Y' : Set M.carrier} {c' : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hY' : Manifold.IsClosedSubmanifold ψ' Y' c') (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (rest' : (Manifold.blowUp ψ' hY').FiniteSuccession) (h : cons ψ hY rest = cons ψ' hY' rest') : Y = Y'

theorem AnalyticManifold.FiniteSuccession.cons_inj {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest rest' : (Manifold.blowUp ψ hY).FiniteSuccession) (h : cons ψ hY rest = cons ψ hY rest') : rest = rest'

The recursions of the weak and marked transforms

theorem AnalyticManifold.FiniteSuccession.weakTransformSeq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) : S.weakTransformSeq J 0 = J

theorem AnalyticManifold.FiniteSuccession.weakTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (i : Fin S.length) : S.weakTransformSeq J i.succ = IdealSheaf.weakTransform (S.map i) (S.weakTransformSeq J i.castSucc) (S.center i)

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (m : ℕ) : S.markedTransformSeq J m 0 = J

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (m : ℕ) (i : Fin S.length) : S.markedTransformSeq J m i.succ = (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := S.markedTransformSeq J m i.castSucc, m := m }).I

theorem AnalyticManifold.FiniteSuccession.cons_weakTransformSeq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) : (cons ψ hY rest).weakTransformSeq J 0 = J

theorem AnalyticManifold.FiniteSuccession.cons_weakTransformSeqAux_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) (k : ℕ) (h : k + 1 < (cons ψ hY rest).length + 1) : (cons ψ hY rest).weakTransformSeqAux J (k + 1) h = rest.weakTransformSeqAux (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) J hY.idealSheaf) k ⋯

The recursion of the weak transforms on the constructor form, at the level of the ℕ-indexed auxiliary recursion.

theorem AnalyticManifold.FiniteSuccession.cons_weakTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) (j : Fin (rest.length + 1)) : (cons ψ hY rest).weakTransformSeq J j.succ = rest.weakTransformSeq (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) J hY.idealSheaf) j