Documentation

Hironaka.Resolution.Analytic.GoingUp.StageIso

The stage identifications T_i ≃ S_i between a sequence and the restriction of its push-forward #

For a smooth blow-up sequence T of a closed submanifold S ⊆ X, the push-forward Π = j_* T [Kol07, 30.3] carries at every stage the strict transform S_i ⊆ X_i and an identification e_i : T_i ≃ S_i, and the restriction Π|_S [Kol07, 30.2] is the sequence whose stages are these S_i. This module makes e_i a diffeomorphism onto the stages of Π|_S (pushforwardStageIso: the identification iso of the push-forward's stage data, carried across the identity of the underlying sets, strictTransformSeqAux_pushforward_succ) and records the two squares it satisfies (the inclusions j_i, the blow-downs) and the two identities that compare T with Π|_S: the centre Z_i^X pulls back along j_i to Z_i (center_pullback_pushforwardIncl) and along e_i from the centre of Π|_S (center_pushforwardStageIso), and the boundary of Π|_S started with any ideal sheaf E₀ pulls back along e_i to the boundary of T started with E₀ (boundarySeq_pushforwardStageIso; the boundary is Hironaka's reduced total transform [Hir64, Main Theorem II′(N), p. 156]), by induction with the naturality of the reduced transform (reducedTransform_pullback_of_comp_eq).

Kollár writes that "for all practical purposes, Z_i^X = Z_i^S" [Kol07, 30.3]; these identifications make the phrase precise, and they carry the normal-crossings clause of T to the push-forward in GoingUp/Theorem84.lean.

source
noncomputable def Manifold.IsClosedSubmanifold.diffeomorphOfEq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y Y' : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ Y' c) (h : Y = Y') :
Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - c) → 𝕜)) hY.toAnalyticManifold.carrier hY'.toAnalyticManifold.carrier ⊤

Two closed submanifolds with the same underlying set, as bundled analytic manifolds: the identity (IsClosedSubmanifold is a proposition, so the two bundles coincide).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Manifold.IsClosedSubmanifold.diffeomorphOfEq_apply_val {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y Y' : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ Y' c) (h : Y = Y') (p : hY.toAnalyticManifold.carrier) :
    ↑((hY.diffeomorphOfEq hY' h) p) = ↑p
    source
    noncomputable def AnalyticManifold.FiniteSuccession.pushforwardStageIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin (T.length + 1)) :
    Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (T.stage i).carrier (((pushforward hS T).restrictSubmanifold hS ⋯).stage i).carrier ⊤

    The identification e_i : T_i ≃ S_i of the stages of T with the stages of the restriction Π|_S of its push-forward ([Kol07, 30.2–30.3]): the identification iso of the push-forward's stage data, carried across the identity of the underlying sets (S_i is the strict transform of S along j_* T).

    Equations
    Instances For
      source
      theorem AnalyticManifold.FiniteSuccession.restrictIncl_pushforwardStageIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin (T.length + 1)) (p : (T.stage i).carrier) :
      ((pushforward hS T).restrictIncl hS ⋯ i) ((pushforwardStageIso hS T i) p) = (pushforwardIncl hS T i) p

      The inclusion S_i ↪ X_i after e_i is the natural inclusion j_i : T_i → X_i (pushforwardIncl).

      source
      theorem AnalyticManifold.FiniteSuccession.map_pushforwardStageIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) (p : (T.stage i.succ).carrier) :
      (((pushforward hS T).restrictSubmanifold hS ⋯).map i) ((pushforwardStageIso hS T i.succ) p) = (pushforwardStageIso hS T i.castSucc) ((T.map i) p)

      The square: the blow-down of Π|_S after e_{i+1} is e_i after the blow-down of T (the squares of the restriction and of the push-forward, through the injective inclusions).

      source
      theorem AnalyticManifold.FiniteSuccession.center_pullback_pushforwardIncl_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (k : ℕ) (hk : k < T.length) :
      Manifold.IdealSheaf.pullback ⇑(pushforwardAux hS T k ⋯).incl ⋯ (pushforwardCenterOf hS T k hk) = T.center ⟨k, hk⟩

      The centre Z_i^X of the push-forward pulls back along j_i : T_i → X_i to the centre Z_i of T, at the recursion level: the ideal sheaf of j_i(Z_i) restricted to S_i is the ideal sheaf of e_i(Z_i) (idealSheaf_preimageVal_eq_pullback), which pulls back along e_i to the ideal sheaf of Z_i (idealSheaf_image_diffeomorph_pullback).

      source
      theorem AnalyticManifold.FiniteSuccession.center_pullback_pushforwardIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) :
      Manifold.IdealSheaf.pullback ⇑(pushforwardIncl hS T i.castSucc) ⋯ ((pushforward hS T).center i) = T.center i

      The centre of the push-forward pulls back along j_i to the centre of T (Kollár's centres Z_i^X = (j_i)_* Z_i, [Kol07, 30.3]).

      source
      theorem AnalyticManifold.FiniteSuccession.center_pushforwardStageIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : Fin T.length) :
      Manifold.IdealSheaf.pullback ⇑(pushforwardStageIso hS T i.castSucc) ⋯ (((pushforward hS T).restrictSubmanifold hS ⋯).center i) = T.center i

      The centre of Π|_S pulls back along e_i to the centre of T (center_restrictSubmanifold composed with restrictIncl_pushforwardStageIso).

      source
      theorem AnalyticManifold.FiniteSuccession.boundarySeq_pushforwardStageIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) {E₀ : hS.toAnalyticManifold.IdealSheaf} (i : Fin (T.length + 1)) :
      Manifold.IdealSheaf.pullback ⇑(pushforwardStageIso hS T i) ⋯ (((pushforward hS T).restrictSubmanifold hS ⋯).boundarySeq E₀ i) = T.boundarySeq E₀ i

      The boundary of Π|_S started with E₀ pulls back along e_i to the boundary of T started with E₀ ([Kol07, 30.2] with [Kol07, 30.3]): the two sequences on S differ by the stage identifications only (e_0 is the identity of S), and the reduced transform is natural along them (reducedTransform_pullback_of_comp_eq on the squares map_pushforwardStageIso).