Ambient blow-up factorizations: restriction to a smaller open, transport along an isomorphism

Two functorialities of the structure f.AmbientBlowUpFactorization U (clause (4) of the resolution theorem, [Kol07, Theorem 45 (4)] read through [Kol07, Warning 23]; the factorization (∗) of [Wlo09, Theorem 2.0.2]), used when the factorization of the glued resolution morphism over an exhaustion open Uₙ is transported to the resolution morphism itself over a relatively compact U ⊆ Uₙ (Hironaka/Resolution/Analytic/Kol07Thm45/AmbientFactorization.lean, Hironaka/Resolution/Analytic/Kol07Thm45/IsoOverLemmas.lean):

• AmbientBlowUpFactorization.ofSubset: a factorization over U is one over any U' ⊆ U — the same data, the covering clause weakened;
• AmbientBlowUpFactorization.ofIsoOver: a factorization of f' : Y' → X over U transports along an isomorphism e : Y|f⁻¹O ≅ Y'|f'⁻¹O over X|O to a factorization of f : Y → X over U, when the pieces lie inside O (the lift over a piece is an isomorphism over the whole piece, and e identifies f with f' over O only) — every field of the ambient side is kept, and the lift over a piece is composed with the restriction of e over the piece;
• the restriction of an isomorphism over O to an isomorphism over an open P ⊆ O (exists_restrictSet_isIso_of_restrictSet_isIso_of_subset, in the vocabulary's form Hom.exists_restrictSet_isIso_of_isIso_restrictSet_of_subset): two applications of exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion (Hironaka/Resolution/Analytic/Kol07Thm45/LocalResolutionRestrict.lean) at N := P — to the open immersion Y|f⁻¹O ⟶ Y' through e and to the open immersion Y|f⁻¹O ⟶ Y, both over X — composed.

Bookkeeping; not in the sources.

def AnalyticSpace.AmbientBlowUpFactorization.ofSubset {K : Type} [RCLike K] {X Y : AnalyticSpace K} {f : Y ⟶ X} {U U' : Set ↑↑X.toPresheafedSpace} (h : U' ⊆ U) (F : Hom.AmbientBlowUpFactorization f U) : Hom.AmbientBlowUpFactorization f U'

An ambient blow-up factorization of f over U is one over any U' ⊆ U: the same pieces, ambient, blow-up sequence, strict transforms and lifts; only the covering clause U' ⊆ ⋃ Uᵢ changes.

Equations

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

theorem AnalyticSpace.exists_restrictSet_isIso_of_restrictSet_isIso_of_subset {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} (f : Y ⟶ X) (f' : Y' ⟶ X) {O P : Set ↑↑X.toPresheafedSpace} (e : Y.restrictSet (KLocallyRingedSpace.Hom.toFun f ⁻¹' O) ⟶ Y'.restrictSet (KLocallyRingedSpace.Hom.toFun f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (hP : IsOpen P) (hPO : P ⊆ O) : ∃ (e' : Y.restrictOpen (Y.openOf (KLocallyRingedSpace.Hom.toFun f ⁻¹' P)) ⟶ Y'.restrictOpen (Y'.openOf (KLocallyRingedSpace.Hom.toFun f' ⁻¹' P))), CategoryTheory.IsIso e' ∧ CategoryTheory.CategoryStruct.comp e' (Hom.restrictSet f' P) = Hom.restrictSet f P

An isomorphism e : Y|f⁻¹O ≅ Y'|f'⁻¹O over X restricts to an isomorphism over every open P ⊆ O: exists_restrictSet_isIso_of_comp_eq_of_isOpenImmersion (Hironaka/Resolution/Analytic/Kol07Thm45/LocalResolutionRestrict.lean) applied to the open immersion Y|f⁻¹O ⟶ Y' through e and to the open immersion Y|f⁻¹O ⟶ Y, both over X, at N := P; the two restricted isomorphisms have the same source, and the composite of the inverse of the second with the first is the restriction of e.

theorem AnalyticSpace.Hom.exists_restrictSet_isIso_of_isIso_restrictSet_of_subset {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {O P : Set ↑↑X.toPresheafedSpace} (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (restrictSet f' O) = restrictSet f O) (hP : IsOpen P) (hPO : P ⊆ O) : ∃ (e' : Y.restrictSet (↑f ⁻¹' P) ⟶ Y'.restrictSet (↑f' ⁻¹' P)), CategoryTheory.IsIso e' ∧ CategoryTheory.CategoryStruct.comp e' (restrictSet f' P) = restrictSet f P

exists_restrictSet_isIso_of_restrictSet_isIso_of_subset for morphisms of An/K (restrictSet, Hom.restrictSet, ≫): an isomorphism e : Y|f⁻¹O ≅ Y'|f'⁻¹O over X|O restricts to an isomorphism over every open P ⊆ O.

noncomputable def AnalyticSpace.AmbientBlowUpFactorization.ofIsoOver {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {U O : Set ↑↑X.toPresheafedSpace} (_hO : IsOpen O) (_hUO : U ⊆ O) (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (F : Hom.AmbientBlowUpFactorization f' U) (hpieces : ∀ (i : F.ι), F.piece i ⊆ O) : Hom.AmbientBlowUpFactorization f U

An ambient blow-up factorization of f' : Y' → X over U transports along an isomorphism e : Y|f⁻¹O ≅ Y'|f'⁻¹O over X|O, O ⊇ U open, to one of f : Y → X over U, when every piece lies inside O: the pieces, the ambient ⊔ Gᵢ, the ideal, the blow-up sequence, the strict transforms and Π_r|_{Y_r} are those of the given factorization; the lift over the piece Uᵢ is the given lift composed with the restriction of e over Uᵢ (Hom.exists_restrictSet_isIso_of_isIso_restrictSet_of_subset), an isomorphism, compatible with f by the compatibility of e with f, f' over Uᵢ.

Equations

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

theorem AnalyticSpace.AmbientBlowUpFactorization.ofSubset_piece {K : Type} [RCLike K] {X Y : AnalyticSpace K} {f : Y ⟶ X} {U U' : Set ↑↑X.toPresheafedSpace} (h : U' ⊆ U) (F : Hom.AmbientBlowUpFactorization f U) : (ofSubset h F).piece = F.piece

The pieces of ofSubset are those of the given factorization.

theorem AnalyticSpace.AmbientBlowUpFactorization.ofSubset_seq {K : Type} [RCLike K] {X Y : AnalyticSpace K} {f : Y ⟶ X} {U U' : Set ↑↑X.toPresheafedSpace} (h : U' ⊆ U) (F : Hom.AmbientBlowUpFactorization f U) : (ofSubset h F).seq = F.seq

The blow-up sequence of ofSubset is that of the given factorization.

theorem AnalyticSpace.AmbientBlowUpFactorization.ofIsoOver_piece {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {U O : Set ↑↑X.toPresheafedSpace} (hO : IsOpen O) (hUO : U ⊆ O) (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (F' : Hom.AmbientBlowUpFactorization f' U) (hpieces' : ∀ (i : F'.ι), F'.piece i ⊆ O) : (ofIsoOver hO hUO e he hcomm F' hpieces').piece = F'.piece

The pieces of ofIsoOver are those of the given factorization.

theorem AnalyticSpace.AmbientBlowUpFactorization.ofIsoOver_G {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {U O : Set ↑↑X.toPresheafedSpace} (hO : IsOpen O) (hUO : U ⊆ O) (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (F' : Hom.AmbientBlowUpFactorization f' U) (hpieces' : ∀ (i : F'.ι), F'.piece i ⊆ O) : (ofIsoOver hO hUO e he hcomm F' hpieces').G = F'.G

The ambient opens of ofIsoOver are those of the given factorization.

theorem AnalyticSpace.AmbientBlowUpFactorization.ofIsoOver_seq {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {U O : Set ↑↑X.toPresheafedSpace} (hO : IsOpen O) (hUO : U ⊆ O) (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (F' : Hom.AmbientBlowUpFactorization f' U) (hpieces' : ∀ (i : F'.ι), F'.piece i ⊆ O) : (ofIsoOver hO hUO e he hcomm F' hpieces').seq = F'.seq

The blow-up sequence of ofIsoOver is that of the given factorization.

theorem AnalyticSpace.AmbientBlowUpFactorization.ofIsoOver_map {K : Type} [RCLike K] {X Y Y' : AnalyticSpace K} {f : Y ⟶ X} {f' : Y' ⟶ X} {U O : Set ↑↑X.toPresheafedSpace} (hO : IsOpen O) (hUO : U ⊆ O) (e : Y.restrictSet (↑f ⁻¹' O) ⟶ Y'.restrictSet (↑f' ⁻¹' O)) (he : CategoryTheory.IsIso e) (hcomm : CategoryTheory.CategoryStruct.comp e (Hom.restrictSet f' O) = Hom.restrictSet f O) (F' : Hom.AmbientBlowUpFactorization f' U) (hpieces' : ∀ (i : F'.ι), F'.piece i ⊆ O) : (ofIsoOver hO hUO e he hcomm F' hpieces').map = F'.map

The morphism Π_r|_{Y_r} of ofIsoOver is that of the given factorization.