Documentation

Hironaka.AnalyticSpace.Glue.Compat

The constants of the pieces agree on the overlaps of a glued space #

For K-gluing data D, the constant sections constOn c i on the images of the pieces (Hironaka.AnalyticSpace.Glue.Space) form a compatible family for Mathlib's sheaf gluing: on pieceOpens i ⊓ pieceOpens j the restrictions of constOn c i and constOn c j coincide (isCompatible_constOn). The reason is that the transitions t i j are K-morphisms: they carry the constant c of Y j | W j i to the constant c of Y i | W i j. This is the compatibility that makes the glued space a K-space (Hironaka.AnalyticSpace.Glue.KSpace).

Conventions. constSec X U c is the restriction of the constant c ∈ Γ(X) to the open subset U; a K-morphism pulls constSec back to constSec (c_app_constSec, from the defining property of K-morphisms on global sections and the naturality of the sheaf component). Sections on an open subset inside the range of an open immersion are compared after pulling back along it (c_app_injective_of_le_range, Mathlib's c_iso). The glue condition f i j ≫ ι i = t i j ≫ f j i ≫ ι j enters through PresheafedSpace.congr_app. For i = j both sides are the restriction of constOn c i; for disjoint pieces the overlap is empty.

Constant sections and K-morphisms #

source
noncomputable def AnalyticSpace.Glue.globalConst {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (c : K) :
↑(X.presheaf.obj (Opposite.op ⊤))

The constant c as a global section of the structure sheaf.

Equations
Instances For
    source
    noncomputable def AnalyticSpace.Glue.constSec {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (c : K) :
    ↑(X.presheaf.obj (Opposite.op U))

    The constant c restricted to the open U of a K-space.

    Equations
    Instances For
      source
      theorem AnalyticSpace.Glue.map_constSec {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (φ : Opposite.op V ⟶ Opposite.op U) (c : K) :
      (CommRingCat.Hom.hom (X.presheaf.map φ)) (constSec X V c) = constSec X U c

      Restricting a constant section (along any morphism of the opposite category of opens) gives the constant section.

      source
      theorem AnalyticSpace.Glue.map_globalConst {K : Type} [RCLike K] (X : KLocallyRingedSpace K) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (i : Opposite.op ⊤ ⟶ Opposite.op U) (c : K) :
      (CommRingCat.Hom.hom (X.presheaf.map i)) (globalConst X c) = constSec X U c

      A restriction of the global constant along any morphism of opens is the constant section.

      source
      theorem AnalyticSpace.Glue.c_app_top_globalConst {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (c : K) :
      (CommRingCat.Hom.hom ((↑g).c.app (Opposite.op ⊤))) (globalConst B c) = globalConst A c

      A K-morphism sends the global constant to the global constant.

      source
      theorem AnalyticSpace.Glue.c_app_constSec {K : Type} [RCLike K] {A B : KLocallyRingedSpace K} (g : A ⟶ B) (U : TopologicalSpace.Opens ↑↑B.toPresheafedSpace) (c : K) :
      (CommRingCat.Hom.hom ((↑g).c.app (Opposite.op U))) (constSec B U c) = constSec A ((TopologicalSpace.Opens.map (↑g).base).obj U) c

      A K-morphism pulls the constant sections back to the constant sections.

      The sheaf component of an open immersion inside its range #

      source
      theorem AnalyticSpace.Glue.opensFunctor_map_eq_of_subset {A B : AlgebraicGeometry.LocallyRingedSpace} (g : A ⟶ B) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g] (O : TopologicalSpace.Opens ↑B.toTopCat) (hO : ↑O ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) :
      (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor g).obj ((TopologicalSpace.Opens.map g.base).obj O) = O

      An open inside the range of an open immersion is the image of its preimage.

      source
      theorem AnalyticSpace.Glue.isIso_c_app_of_le_range {A B : AlgebraicGeometry.LocallyRingedSpace} (g : A ⟶ B) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g] (O : TopologicalSpace.Opens ↑B.toTopCat) (hO : ↑O ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) :
      CategoryTheory.IsIso (g.c.app (Opposite.op O))

      The sheaf component of an open immersion is an isomorphism on opens inside its range.

      source
      theorem AnalyticSpace.Glue.c_app_injective_of_le_range {A B : AlgebraicGeometry.LocallyRingedSpace} (g : A ⟶ B) [AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g] (O : TopologicalSpace.Opens ↑B.toTopCat) (hO : ↑O ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)) :
      Function.Injective ⇑(CommRingCat.Hom.hom (g.c.app (Opposite.op O)))
      source
      theorem AnalyticSpace.Glue.KGlueData.c_app_constOn {K : Type} [RCLike K] (D : KGlueData K) (c : K) (i : D.J) :
      (CommRingCat.Hom.hom ((D.ι i).c.app (Opposite.op (D.pieceOpens i)))) (D.constOn c i) = constSec (D.Y i) ((TopologicalSpace.Opens.map (D.ι i).base).obj (D.pieceOpens i)) c

      Pulling the constant of the i-th image back along ι i gives the constant of Y i.

      source
      theorem AnalyticSpace.Glue.KGlueData.c_app_constOn_other {K : Type} [RCLike K] (D : KGlueData K) (c : K) (i j : D.J) :
      (CommRingCat.Hom.hom ((D.ι i).c.app (Opposite.op (D.pieceOpens j)))) (D.constOn c j) = constSec (D.Y i) ((TopologicalSpace.Opens.map (D.ι i).base).obj (D.pieceOpens j)) c

      Pulling the constant of the j-th image back along ι i gives the constant of Y i on (ι i)⁻¹ (pieceOpens j): the glue condition and the K-morphism property of t i j.

      source
      theorem AnalyticSpace.Glue.KGlueData.isCompatible_constOn {K : Type} [RCLike K] (D : KGlueData K) (c : K) :
      D.glued.presheaf.IsCompatible D.pieceOpens (D.constOn c)

      The constants of the pieces form a compatible family on the images.