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.

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.

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀ (D : AlgebraicGeometry.Scheme.GlueData) : D.oneHypercover.I₀ = D.J

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_f (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J) : D.oneHypercover.f i = D.ι i

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁ (D : AlgebraicGeometry.Scheme.GlueData) (x✝ x✝¹ : D.J) : D.oneHypercover.I₁ x✝ x✝¹ = PUnit.{u + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x✝ : PUnit.{u + 1} ) : D.oneHypercover.Y x✝ = D.V (i₁, i₂)

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x✝ : PUnit.{u + 1} ) : D.oneHypercover.p₁ x✝ = D.f i₁ i₂

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_X (D : AlgebraicGeometry.Scheme.GlueData) (a✝ : D.J) : D.oneHypercover.X a✝ = D.U a✝

@[simp]

theorem AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂ (D : AlgebraicGeometry.Scheme.GlueData) (i₁ i₂ : D.J) (x✝ : PUnit.{u + 1} ) : D.oneHypercover.p₂ x✝ = CategoryTheory.CategoryStruct.comp (D.t i₁ i₂) (D.f i₂ i₁)

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

• D.sheafValGluedMk s h = (CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv (D.oneHypercover.isLimitMultifork F)) { val := s, property := ⋯ }

@[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