Documentation

Hironaka.AnalyticSpace.Glue.Desc

K-morphisms out of a glued K-space #

For K-gluing data D (Hironaka.AnalyticSpace.Glue.Data) and K-morphisms g i : Y i ⟶ Z compatible with the transitions (f i j ≫ g i = t i j ≫ f j i ≫ g j on the overlaps), the universal property of the multicoequalizer gives a morphism descLRS g : glued ⟶ Z of locally ringed spaces with ι i ≫ descLRS g = g i; it is a K-morphism descK g : gluedK ⟶ Z (Hironaka.AnalyticSpace.Glue.KSpace): the constant c of Z pulls back to the glued constant, because on every image ι i '' ⊤ its pull-back is the constant of Y i (the K-morphism property of g i) and the glued constant is the unique section with these restrictions. Two K-morphisms out of the glued K-space agreeing after every ιK i are equal (hom_ext_gluedK).

Conventions. The compatibility is stated at the level of locally ringed spaces ((g i).1), in the parenthesisation of Mathlib's multispan diagram (D.f i j, D.t i j ≫ D.f j i). With one piece, descK g is g 0 up to the identification of the glued space with the piece; for Z = gluedK and g i = ιK i the descent is the identity (hom_ext_gluedK).

This is how the morphism from the complexified space into the glued space is assembled from the local complexifications (Hironaka.AnalyticSpace.Glue.Morphism), and how the map from a glued space of local resolutions to the base is defined (Hironaka.AnalyticSpace.Glue.Over).

source
theorem AnalyticSpace.Glue.KGlueData.exists_ι_base_eq {K : Type} [RCLike K] (D : KGlueData K) (z : ↑D.glued.toTopCat) :
∃ (i : D.J) (y : ↑↑(D.Y i).toPresheafedSpace), (CategoryTheory.ConcreteCategory.hom (D.ι i).base) y = z

Every point of the glued space comes from a piece (Mathlib's ι_jointly_surjective, restated with the index and piece types of the K-gluing data).

source
noncomputable def AnalyticSpace.Glue.KGlueData.descLRS {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) :
D.glued ⟶ Z.toLocallyRingedSpace

The descent of compatible morphisms on the pieces to the glued locally ringed space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AnalyticSpace.Glue.KGlueData.ι_descLRS {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) (i : D.J) :
    CategoryTheory.CategoryStruct.comp (D.ι i) (D.descLRS g hg) = ↑(g i)
    source
    theorem AnalyticSpace.Glue.KGlueData.c_app_top_descLRS {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) (c : K) :
    (CommRingCat.Hom.hom ((D.descLRS g hg).c.app (Opposite.op ⊤))) (globalConst Z c) = D.glueConst c

    The pull-back of the constant c of Z along the descent is the glued constant.

    source
    noncomputable def AnalyticSpace.Glue.KGlueData.descK {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) :
    D.gluedK ⟶ Z

    The descent as a K-morphism out of the glued K-space.

    Equations
    Instances For
      source
      theorem AnalyticSpace.Glue.KGlueData.descK_val {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) :
      ↑(D.descK g hg) = D.descLRS g hg
      source
      theorem AnalyticSpace.Glue.KGlueData.ιK_descK {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) (i : D.J) :
      CategoryTheory.CategoryStruct.comp (D.ιK i) (D.descK g hg) = g i
      source
      theorem AnalyticSpace.Glue.KGlueData.toFun_descK_ιK {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} (g : (i : D.J) → D.Y i ⟶ Z) (hg : ∀ (i j : D.J), CategoryTheory.CategoryStruct.comp (D.f i j) ↑(g i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (↑(D.t i j)) (D.f j i)) ↑(g j)) (i : D.J) (y : ↑↑(D.Y i).toPresheafedSpace) :
      KLocallyRingedSpace.Hom.toFun (D.descK g hg) (KLocallyRingedSpace.Hom.toFun (D.ιK i) y) = KLocallyRingedSpace.Hom.toFun (g i) y
      source
      theorem AnalyticSpace.Glue.KGlueData.hom_ext_gluedK {K : Type} [RCLike K] (D : KGlueData K) {Z : KLocallyRingedSpace K} {h h' : D.gluedK ⟶ Z} (H : ∀ (i : D.J), CategoryTheory.CategoryStruct.comp (D.ιK i) h = CategoryTheory.CategoryStruct.comp (D.ιK i) h') :
      h = h'

      Two K-morphisms out of the glued K-space agreeing on every piece are equal.