Step 3 of Theorem 103 in the compatible-family form: the descent along the cover

The descent of Step 3 of the proof of [Kol07, Theorem 103] follows [Kol07, Proposition 37], as axiomatized in [Kol07, Theorem 105]: on the fibre product X'' := X' ×_X X' of the cover g : X' → X with itself, τ₁^* B(X') = B(X'') = τ₂^* B(X') (the first centres in (37.1) and (105.4)), so B(X') descends to a unique blow-up sequence B̄(X) with g^* B̄(X) = B(X'). In the compatible-family form the cover is the finite cover k : ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U of a relatively compact open U by pieces with maximal contact (ShrunkMCCover, GlobalizeFamCover.lean), and B(X') is the value of the family functor on the open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) of the coproduct. The saturation is checked on the fibre product of the coproduct of the whole pieces with itself: the pulled-back triple there has a global hypersurface of maximal contact, the open q₁^{-1}(O) ∩ q₂^{-1}(O) is relatively compact, and the commutation of the family functor with the two projections identifies both pull-backs of the value with its value there (ShrunkMCCover.exists_unique_descent).

The same fibre-product argument, run for a triple of the local class over an arbitrary local analytic isomorphism e₁ against a cover (e₂, O₂, L₂), is the comparison lemma CommutesWithLocalIsos.seqOn_eq_eraseEmpty_pullback_of_descent: the family's value on O₁ is the pull-back of the descended sequence L₂ along e₁|_{O₁}, with empty blow-ups deleted. From it GlobalizeFam.lean derives the compatibility of the descended values under restriction, their independence of the cover, the agreement with the family on the local class and the commutation of the descended functor with local analytic isomorphisms.

• CommutesWithLocalIsos.seqOn_eq_eraseEmpty_pullback_of_descent — the comparison lemma;
• ShrunkMCCover.coverList — Kollár's B(X'), the value on the cover;
• ShrunkMCCover.exists_unique_descent, descent, pullback_descent, descent_unique, noEmptyCenters_descent — Kollár's B̄(X) over U, the unique sequence on U pulling back to the value on the cover.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.CommutesWithLocalIsos.seqOn_eq_eraseEmpty_pullback_of_descent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (hB : B.CommutesWithLocalIsos) (hpull : ∀ {M N : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g), Dom T' → Dom (T'.pullback g hg)) {M₀ N₁ N₂ : AnalyticManifold 𝕜 E} {T₀ : Manifold.AnalyticTriple ψ₀ M₀} {T₁ : Manifold.AnalyticTriple ψ₀ N₁} {e₁ : AnalyticMap N₁ M₀} (he₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e₁) (hT₁ : Dom T₁) (hT₁e : T₁.IsPullbackOf T₀ e₁) {T₂ : Manifold.AnalyticTriple ψ₀ N₂} {e₂ : AnalyticMap N₂ M₀} (he₂ : Manifold.IsCoprodOfOpenEmbeddings e₂) (hT₂ : Dom T₂) (hT₂e : T₂.IsPullbackOf T₀ e₂) {O₁ : TopologicalSpace.Opens N₁.carrier} (hO₁ : IsCompact (closure ↑O₁)) {O₂ : TopologicalSpace.Opens N₂.carrier} (hO₂ : IsCompact (closure ↑O₂)) {V : TopologicalSpace.Opens M₀.carrier} (himg₂ : ⇑e₂ '' ↑O₂ = ↑V) (himg₁ : ⇑e₁ '' ↑O₁ ⊆ ↑V) (L₂ : AnalyticManifold.BlowUpSequence ψ₀ (M₀.restrict V)) (hL₂ : L₂.pullback (AnalyticMap.restrictMap e₂ O₂ V ⋯) ⋯ = (B.fam T₂ hT₂).seqOn O₂ hO₂) : (B.fam T₁ hT₁).seqOn O₁ hO₁ = (L₂.pullback (AnalyticMap.restrictMap e₁ O₁ V himg₁) ⋯).eraseEmpty

The comparison lemma (the argument of [Kol07, Proposition 37] in the compatible-family form, with [Wlo09, Definition 3.2.6] for the deletion of empty blow-ups). Let T₁ on N₁ carry the pull-back of T₀ along a local analytic isomorphism e₁, and T₂ on N₂ the pull-back along a coproduct of open embeddings e₂; let O₁ ⊆ N₁, O₂ ⊆ N₂ be relatively compact opens with e₂(O₂) = V and e₁(O₁) ⊆ V; and let L₂ be a sequence on V which pulls back along e₂|_{O₂} to the family's value on O₂. Then the family's value on O₁ is the pull-back of L₂ along e₁|_{O₁} with the empty blow-ups deleted. On the fibre product of e₁ and e₂ over M₀, the open O := O₁ ×_V O₂ is relatively compact and maps onto O₁; the family's commutation with the first projection gives the value on O as the pull-back of the value on O₁, its commutation with the second projection and its compatibility on N₂ give it as the pull-back of L₂ along the composite through O₂; the two composites to V agree, and pull-back along the surjective first projection is injective.

noncomputable def Manifold.AnalyticTriple.ShrunkMCCover.coverList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) : AnalyticManifold.BlowUpSequence ψ₀ (C.sigma.restrict C.opens)

Kollár's B(X'): the family's value on the open ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) of the coproduct of the pieces.

Equations

• C.coverList B hT = (B.fam C.triple ⋯).seqOn C.opens ⋯

theorem Manifold.AnalyticTriple.ShrunkMCCover.noEmptyCenters_coverList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) : (C.coverList B hT).NoEmptyCenters

The value on the cover has no empty centres.

theorem Manifold.AnalyticTriple.ShrunkMCCover.exists_unique_descent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) (hB : B.CommutesWithLocalIsos) : ∃! L : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U), L.pullback C.coverMap ⋯ = C.coverList B hT

The descent of [Kol07, Proposition 37] and of the proof of [Kol07, Theorem 105], in the compatible-family form: the value on the cover descends uniquely along the cover map k : ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) → U. On the fibre product Q of the coproduct of the whole pieces with itself, the pulled-back triple has a global hypersurface of maximal contact, the open q₁^{-1}(O) ∩ q₂^{-1}(O) over O = ⊔ᵢ ιᵢ^{-1}(Wᵢ ∩ U) is relatively compact, and the family's commutation with the two projections gives q₁^* B(X') = q₂^* B(X') there, the condition under which a sequence descends uniquely along a surjective coproduct of open embeddings (BlowUpSequence.exists_unique_pullback_eq_of_isFibreProduct).

noncomputable def Manifold.AnalyticTriple.ShrunkMCCover.descent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) (hB : B.CommutesWithLocalIsos) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

Kollár's B̄(X) over U: the sequence on U pulling back to the value on the cover.

Equations

• C.descent B hT hB = ⋯.choose

theorem Manifold.AnalyticTriple.ShrunkMCCover.pullback_descent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) (hB : B.CommutesWithLocalIsos) : (C.descent B hT ⋯).pullback C.coverMap ⋯ = C.coverList B hT

The descended sequence pulls back along the cover map to the value on the cover.

theorem Manifold.AnalyticTriple.ShrunkMCCover.descent_unique {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) (hB : B.CommutesWithLocalIsos) {L : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)} (hL : L.pullback C.coverMap ⋯ = C.coverList B hT) : L = C.descent B hT ⋯

The descended sequence is the only sequence on U pulling back to the value on the cover (pull-back along the surjective cover map is injective).

theorem Manifold.AnalyticTriple.ShrunkMCCover.noEmptyCenters_descent {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} {m : ℕ} {U : TopologicalSpace.Opens M.carrier} (C : T.ShrunkMCCover m U) (B : Hironaka.Manifold.AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) (hT : BOClass m T) (hB : B.CommutesWithLocalIsos) : (C.descent B hT ⋯).NoEmptyCenters

The descended sequence has no empty centres: its pull-back along the surjective cover map has none.