Documentation

Mathlib.AlgebraicGeometry.GluingOneHypercover

The 1-hypercover of a glue data #

In this file, given D : Scheme.GlueData, we construct a 1-hypercover D.openHypercover of the scheme D.glued in the big Zariski site. We use this 1-hypercover in order to define a constructor D.sheafValGluedMk for sections over D.glued of a sheaf of types over the big Zariski site.

Notes #

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ : D.J) (i₂ : D.J) :
∀ (x : PUnit.{u + 1} ), D.oneHypercover.p₁ x = D.f i₁ i₂
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀ (D : AlgebraicGeometry.Scheme.GlueData) :
D.oneHypercover.I₀ = D.J
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_X (D : AlgebraicGeometry.Scheme.GlueData) :
∀ (a : D.J), D.oneHypercover.X a = D.U a
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ : D.J) (i₂ : D.J) (j : PUnit.{u + 1} ) :
D.oneHypercover.p₂ j = CategoryTheory.CategoryStruct.comp (D.t i₁ i₂) (D.f i₂ i₁)
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁ (D : AlgebraicGeometry.Scheme.GlueData) :
∀ (x x_1 : D.J), D.oneHypercover.I₁ x x_1 = PUnit.{u + 1}
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_f (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) :
D.oneHypercover.f i = D.ι i
source
@[simp]
theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y (D : AlgebraicGeometry.Scheme.GlueData) (i₁ : D.J) (i₂ : D.J) :
∀ (x : PUnit.{u + 1} ), D.oneHypercover.Y x = D.V (i₁, i₂)
source
noncomputable def AlgebraicGeometry.Scheme.GlueData.oneHypercover (D : AlgebraicGeometry.Scheme.GlueData) :
AlgebraicGeometry.Scheme.zariskiTopology.OneHypercover D.glued

The 1-hypercover of D.glued in the big Zariski site that is given by the open cover D.U from the glue data D. The "covering of the intersection of two such open subsets" is the trivial covering given by D.V.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk (D : AlgebraicGeometry.Scheme.GlueData) {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)} (s : (j : D.J) → F.val.obj (Opposite.op (D.U j))) (h : ∀ (i j : D.J), F.val.map (D.f i j).op (s i) = F.val.map (CategoryTheory.CategoryStruct.comp (D.f j i).op (D.t i j).op) (s j)) :
    F.val.obj (Opposite.op D.glued)

    Constructor for sections over D.glued of a sheaf of types on the big Zariski site.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val (D : AlgebraicGeometry.Scheme.GlueData) {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)} (s : (j : D.J) → F.val.obj (Opposite.op (D.U j))) (h : ∀ (i j : D.J), F.val.map (D.f i j).op (s i) = F.val.map (CategoryTheory.CategoryStruct.comp (D.f j i).op (D.t i j).op) (s j)) (j : D.J) :
      F.val.map (D.ι j).op (D.sheafValGluedMk s h) = s j