Rigidity transfer on a gluing over a base

The resolutions of two pieces are identified over their overlap by the functoriality of the resolution: it is independent of the embedding up to a canonical isomorphism Kol07, Theorem 36, proof, the blow-up sequences of the pieces agree on the overlaps [Kol07, Proposition 37, (37.2)], and the canonical desingularization commutes with local analytic isomorphisms Wlo09, Theorem 6.0.6, (2). The gluing needs one more fact, which the sources use without stating it: an isomorphism over the base between two resolutions of one open subset is unique. It is a hypothesis here. Read on a gluing datum G : GlueOver X R π dom (Hironaka.AnalyticSpace.Glue.Over): the chosen transitions t i j are isomorphisms over X between the parts of the pieces over the overlaps, and where the parts over an open subset P of the base have no non-trivial automorphism over X (RigidOver (π i) P), every isomorphism over X between the parts over P is the restricted transition. Consequently the compatibility of closed subspaces of the pieces along a transition, comap (t i j) (C j) = C i on the gluing open subset, follows from local isomorphisms over X carrying C j to C i:

• KLocallyRingedSpace.RigidOver πA O: no non-trivial automorphism over Z of the part over O;
• the locality tools stalkIdeal_toFun_eq_of_comap_eq_of_isIso_stalkMap and idealSheaf_eq_of_forall_exists_comap_eq: two ideal sheaves agreeing along stalk-isomorphic morphisms through every point are equal;
• GlueOver.tComap (the transition in the Opens.comap spelling of restrictOver, an eqToHom conjugate), GlueOver.tOver P hP (the transition restricted to the parts over P, restrictOver of Hironaka.AnalyticSpace.Glue.GlueIsoOver), tOver_over, isIso_tOver, tOver_comp_ofRestrict;
• GlueOver.eq_tOver_of_isoOver: over a rigid P, θ = tOver (isoOver_unique_of_aut, Hironaka.Resolution.Analytic.Kol07Thm45.LocalModel);
• GlueOver.compatClosedSubspaces_pair_of_forall_exists_isoOver: pair compatibility from local isomorphisms over X (locality and the preceding item).

The rigidity of the local resolutions over X is supplied by Hironaka.Resolution.Analytic.Kol07Thm45.RigidOverLocalResolution, from the uniqueness of the isomorphism over the base between two local resolutions; the pair compatibility feeds the gluing of the exceptional families of the local resolutions (CoproductGluedFamilyCompat, ExhaustionChainFamilies, RigidOverLocalResolution).

theorem AnalyticSpace.KLocallyRingedSpace.eqToHom_restrictOpen_comp_ofRestrict {K : Type} [RCLike K] {Y : KLocallyRingedSpace K} {O₁ O₂ : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (h : O₁ = O₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Y.ofRestrict O₂) = Y.ofRestrict O₁

The identification of the restrictions along an equality of opens lies over the space.

def AnalyticSpace.KLocallyRingedSpace.RigidOver {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) : Prop

The parts of A over O are rigid over Z: every automorphism over Z of A|πA⁻¹O is the identity; the hypothesis of isoOver_unique_of_aut, named.

Equations

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

theorem AnalyticSpace.KLocallyRingedSpace.stalkIdeal_toFun_eq_of_comap_eq_of_isIso_stalkMap {K : Type} [RCLike K] {Y Z : KLocallyRingedSpace K} (f : Z ⟶ Y) {A B : Manifold.IdealSheaf Y.𝒪} (h : QuotientSpace.comap (↑f) A = QuotientSpace.comap (↑f) B) (z : ↑↑Z.toPresheafedSpace) (hz : CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑f) z)) : A.stalkIdeal (Hom.toFun f z) = B.stalkIdeal (Hom.toFun f z)

Equal pull-backs along a morphism that is an isomorphism on the stalk at z give equal stalk ideals at the image of z: the stalk ideal of a pull-back is the image of the stalk ideal under the stalk map (QuotientSpace.stalkIdeal_comap), and a bijective ring map is injective on ideals (Ideal.comap_map_of_bijective).

theorem AnalyticSpace.KLocallyRingedSpace.idealSheaf_eq_of_forall_exists_comap_eq {K : Type} [RCLike K] {Y : KLocallyRingedSpace K} {A B : Manifold.IdealSheaf Y.𝒪} (h : ∀ (y : ↑↑Y.toPresheafedSpace), ∃ (Z : KLocallyRingedSpace K) (f : Z ⟶ Y) (z : ↑↑Z.toPresheafedSpace), Hom.toFun f z = y ∧ CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑f) z) ∧ QuotientSpace.comap (↑f) A = QuotientSpace.comap (↑f) B) : A = B

Two ideal sheaves that agree along stalk-isomorphic morphisms through every point are equal: IdealSheaf.ext stalk by stalk, each stalk reached through the given morphism.

theorem AnalyticSpace.GlueOver.glueOpens_eq_comap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i j : ι) : glueOpens X R π dom i j = (TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) (dom i ⊓ dom j)

The gluing open subset in Mathlib's Opens.comap spelling (overOpens_eq_comap at the overlap).

theorem AnalyticSpace.GlueOver.glueOpens_symm_eq_comap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i j : ι) : glueOpens X R π dom j i = (TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) (dom i ⊓ dom j)

The opposite gluing open subset in the Opens.comap spelling of the same overlap dom i ⊓ dom j (inf_comm).

theorem AnalyticSpace.GlueOver.comap_le_glueOpens {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) : (TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P ≤ glueOpens X R π dom i j

The parts over P ≤ dom i ⊓ dom j lie in the gluing open subset.

def AnalyticSpace.GlueOver.tComap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) (dom i ⊓ dom j)) ⟶ (R j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) (dom i ⊓ dom j))

The transition in the Opens.comap spelling of restrictOver: t i j conjugated by the identifications of the gluing open subsets with the Opens.comap of the overlap (glueOpens_eq_comap).

Equations

• G.tComap i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.t i j) (CategoryTheory.eqToHom ⋯))

theorem AnalyticSpace.GlueOver.tComap_comp_ofRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) : CategoryTheory.CategoryStruct.comp (G.tComap i j) ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) (dom i ⊓ dom j))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.t i j) ((R j).ofRestrict (glueOpens X R π dom j i)))

The Opens.comap transition followed by the inclusion is the identification followed by t i j and the inclusion of the gluing open subset.

theorem AnalyticSpace.GlueOver.compat_tComap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) (dom i ⊓ dom j))) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.tComap i j) ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) (dom i ⊓ dom j)))) (π j)

The Opens.comap transition lies over X (G.compat, transported along the identifications).

theorem AnalyticSpace.GlueOver.isIso_tComap {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) : CategoryTheory.IsIso (G.tComap i j)

The Opens.comap transition is an isomorphism (t i j is one: the glue data's t_isIso, lifted to K-morphisms by isIso_of_isIso_val).

noncomputable def AnalyticSpace.GlueOver.tOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)

The transition restricted to the parts over P ≤ dom i ⊓ dom j (restrictOver at t i j).

Equations

• G.tOver i j hP = AnalyticSpace.KLocallyRingedSpace.restrictOver (π i) (π j) hP (G.tComap i j) ⋯

theorem AnalyticSpace.GlueOver.tOver_over {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.tOver i j hP) ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P))) (π j)

The restricted transition lies over X.

theorem AnalyticSpace.GlueOver.isIso_tOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) : CategoryTheory.IsIso (G.tOver i j hP)

The restricted transition is an isomorphism.

theorem AnalyticSpace.GlueOver.tOver_comp_ofRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) : CategoryTheory.CategoryStruct.comp (G.tOver i j hP) ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)) = CategoryTheory.CategoryStruct.comp ((R i).restrictIncl ⋯) (CategoryTheory.CategoryStruct.comp (G.t i j) ((R j).ofRestrict (glueOpens X R π dom j i)))

The restricted transition followed by the inclusion is the inclusion of the parts over P into the gluing open subset, followed by t i j and the inclusion of the gluing open subset (restrictOver_comp_ofRestrict with the identifications absorbed).

theorem AnalyticSpace.GlueOver.eq_tOver_of_isoOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (i j : ι) {P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hP : P ≤ dom i ⊓ dom j) (haut : KLocallyRingedSpace.RigidOver (π i) P) (θ : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)) (hθ : CategoryTheory.IsIso θ) (hθc : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P))) (π j)) : θ = G.tOver i j hP

Rigidity transfer: over a rigid P ≤ dom i ⊓ dom j, every isomorphism θ over X between the parts of R i and of R j over P is the restricted transition tOver (isoOver_unique_of_aut at θ and tOver).

theorem AnalyticSpace.GlueOver.compatClosedSubspaces_pair_of_forall_exists_isoOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) (C : (i : ι) → (R i).ClosedSubspace) (i j : ι) (h : ∀ y ∈ glueOpens X R π dom i j, ∃ (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : P ≤ dom i ⊓ dom j), KLocallyRingedSpace.Hom.toFun (π i) y ∈ P ∧ KLocallyRingedSpace.RigidOver (π i) P ∧ ∃ (θ : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P))) (π j) ∧ QuotientSpace.comap (↑(CategoryTheory.CategoryStruct.comp θ ((R j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π j), continuous_toFun := ⋯ }) P)))) (C j) = QuotientSpace.comap (↑((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P))) (C i)) : QuotientSpace.comap (↑(G.t i j)) (restrictGlue π dom j i (C j)) = restrictGlue π dom i j (C i)

Pair compatibility from local isomorphisms over X: if every point of the gluing open subset has a rigid P ≤ dom i ⊓ dom j through its image and an isomorphism θ over X of the parts over P carrying C j to C i, then the transition t i j carries C j to C i on the whole gluing open subset: locality (idealSheaf_eq_of_forall_exists_comap_eq along the open inclusions of the parts over P), θ = tOver (eq_tOver_of_isoOver), tOver_comp_ofRestrict.