Kollár's constructors of analytic blow-up sequences

Kollár's view of a blow-up sequence as its list of centres [Kol07, Definition 29], as constructors of AnalyticManifold.FiniteSuccession M:

• blowUp ψ hY, blowUpπ ψ hY: the blowing-up of M along the closed submanifold Y (BlowUpSpace, the blowing-up of [BM88, Definition 4.1]) as a bundled analytic manifold with its blow-down, a blowing-up with centre Y (isBlowUp_blowUpπ) and a monoidal transformation with centre the ideal sheaf hY.idealSheaf of Y (isMonoidalTransformation_blowUpπ);
• FiniteSuccession.nil M (the empty sequence) and FiniteSuccession.cons ψ hY rest, the sequence whose first blow-up is blowUpπ ψ hY followed by rest; the later stages are finStages (blowUp ψ hY) rest.later, so that the dependent fields center, map, isMonoidal are Fin.cases of the head and of the fields of rest, definitionally (cons_length, cons_center_zero, cons_map_zero, cons_center_succ, cons_map_succ, cons_stage_zero, cons_stage_succ).

The constructors are the form in which the order-reduction and resolution algorithms build their sequences.

The blowing-up along a closed submanifold as a bundled analytic manifold

noncomputable def Manifold.blowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : AnalyticManifold 𝕜 E

The blowing-up of M along the closed submanifold Y (BlowUpSpace, the blowing-up of [BM88, Definition 4.1]) as a bundled analytic manifold.

Equations

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

noncomputable def Manifold.blowUpπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : AnalyticMap (blowUp ψ hY) M

The blow-down π : Bl_Y M → M (blowUpMap) as a bundled analytic map.

Equations

• Manifold.blowUpπ ψ hY = ⟨Manifold.blowUpMap ψ hY, ⋯⟩

theorem Manifold.blowUpπ_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (p : (blowUp ψ hY).carrier) : (blowUpπ ψ hY) p = blowUpMap ψ hY p

theorem Manifold.isBlowUp_blowUpπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : IsBlowUp ψ Y c ⇑(blowUpπ ψ hY)

The blow-down blowUpπ ψ hY is a blowing-up with centre Y [BM88, Definition 4.1].

theorem Manifold.isMonoidalTransformation_blowUpπ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : (blowUpπ ψ hY).IsMonoidalTransformation hY.idealSheaf

The blow-down blowUpπ ψ hY is a monoidal transformation of M with centre the ideal sheaf I_Y of Y, in the sense in which the main theorems use the phrase (IsMonoidalTransformation). The witnesses are the chart ψ, the codimension c, the facts that Y is the cosupport of I_Y and that I_Y is the ideal sheaf of Y, and isBlowUp_blowUpπ.

Kollár's constructors: the empty sequence and cons

def AnalyticManifold.FiniteSuccession.nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : M.FiniteSuccession

The empty blow-up sequence X_0 = M, of length 0 [Kol07, Definition 29].

Equations

• AnalyticManifold.FiniteSuccession.nil M = { length := 0, later := Fin.elim0, center := fun (i : Fin 0) => i.elim0, map := fun (i : Fin 0) => i.elim0, isMonoidal := ⋯ }

noncomputable def AnalyticManifold.FiniteSuccession.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) : M.FiniteSuccession

The blow-up sequence whose first blow-up is the blowing-up of M along the closed submanifold Y (centre the ideal sheaf hY.idealSheaf of Y), followed by the sequence rest starting with Bl_Y M [Kol07, Definition 29]. The later stages are finStages (blowUp ψ hY) rest.later, so that center, map and isMonoidal are Fin.cases of the head and of the fields of rest.

Equations

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

theorem AnalyticManifold.FiniteSuccession.nil_length {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} : (nil M).length = 0

theorem AnalyticManifold.FiniteSuccession.cons_length {𝕜 : 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).length = rest.length + 1

theorem AnalyticManifold.FiniteSuccession.cons_center_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) : (cons ψ hY rest).center 0 = hY.idealSheaf

theorem AnalyticManifold.FiniteSuccession.cons_map_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) : (cons ψ hY rest).map 0 = Manifold.blowUpπ ψ hY

theorem AnalyticManifold.FiniteSuccession.cons_center_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 : Fin rest.length) : (cons ψ hY rest).center j.succ = rest.center j

theorem AnalyticManifold.FiniteSuccession.cons_map_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 : Fin rest.length) : (cons ψ hY rest).map j.succ = rest.map j

theorem AnalyticManifold.FiniteSuccession.cons_stage_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) : (cons ψ hY rest).stage 0 = M

theorem AnalyticManifold.FiniteSuccession.cons_stage_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 : Fin (rest.length + 1)) : (cons ψ hY rest).stage j.succ = rest.stage j