NYLL
Module

CoverHypercover.lean

Nyll.SchemeTheory.WeilRestriction.CoverHypercover
10 declarations indexed from sourceView source ↗

Module documentation

A relative hypercover from a locally directed open cover

The common lower indices of a locally directed open cover give a cover of each pairwise intersection. They therefore define a 1-hypercover, also in the category of schemes over a fixed base.

The relative construction accepts chosen structure maps on the cover components. Thus its objects can agree definitionally with local objects already in use. The zero indices are universe-lifted so that no smallness assumption on the category of cover indices is required.

Imports4
  • Mathlib.AlgebraicGeometry.Cover.Directed
  • Mathlib.AlgebraicGeometry.Sites.BigZariski
  • Mathlib.CategoryTheory.Sites.Hypercover.One
  • Mathlib.CategoryTheory.Sites.Over
Imported by3

Declarations

def

locallyDirectedCoverPreHypercover

L42 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverPreHypercover
Documentation

The pre-hypercover of a locally directed open cover with common lower indices as overlaps.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
Lean source · full declaration
def locallyDirectedCoverPreHypercover : PreOneHypercover.{max v w} X where
  I₀ := ULift.{v} 𝒰.I₀
  X i := 𝒰.X i.down
  f i := 𝒰.f i.down
  I₁ i j := Σ k : 𝒰.I₀, (k ⟶ i.down) × (k ⟶ j.down)
  Y {_ _} k := 𝒰.X k.1
  p₁ {_ _} k := 𝒰.trans k.2.1
  p₂ {_ _} k := 𝒰.trans k.2.2
  w {_ _} k := by rw [Scheme.Cover.trans_map, Scheme.Cover.trans_map]
lemma

locallyDirectedCoverPreHypercover_mem₀

L52 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverPreHypercover_mem₀
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
Lean source · statement
lemma locallyDirectedCoverPreHypercover_mem₀ :
    (locallyDirectedCoverPreHypercover 𝒰).sieve₀ ∈ Scheme.zariskiTopology X
def

locallyDirectedCoverHypercover

L64 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercover
Documentation

The hypercover whose overlap components are indexed by common lower indices.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
Lean source · statement
def locallyDirectedCoverHypercover :
    GrothendieckTopology.OneHypercover.{max v w} Scheme.zariskiTopology X
def

locallyDirectedCoverPreHypercoverOver

L76 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverPreHypercoverOver
Documentation

The pre-hypercover in the slice over the chosen base, retaining the specified component structure maps.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · full declaration
def locallyDirectedCoverPreHypercoverOver :
    PreOneHypercover.{max v w} (Over.mk f) where
  I₀ := ULift.{v} 𝒰.I₀
  X i := Over.mk (g i.down)
  f i := Over.homMk (𝒰.f i.down) (hg i.down)
  I₁ i j := Σ k : 𝒰.I₀, (k ⟶ i.down) × (k ⟶ j.down)
  Y {_ _} k := Over.mk (g k.1)
  p₁ {i j} k := Over.homMk (𝒰.trans k.2.1) (by
    change 𝒰.trans k.2.1 ≫ g i.down = g k.1
    rw [← hg i.down, ← Category.assoc, Scheme.Cover.trans_map, hg k.1])
  p₂ {i j} k := Over.homMk (𝒰.trans k.2.2) (by
    change 𝒰.trans k.2.2 ≫ g j.down = g k.1
    rw [← hg j.down, ← Category.assoc, Scheme.Cover.trans_map, hg k.1])
  w {i j} k := by
    apply (Over.forget S).map_injective
    change 𝒰.trans k.2.1 ≫ 𝒰.f i.down = 𝒰.trans k.2.2 ≫ 𝒰.f j.down
    rw [Scheme.Cover.trans_map, Scheme.Cover.trans_map]
def

locallyDirectedCoverHypercoverOver

L99 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver
Documentation

A locally directed open cover gives a 1-hypercover over S.

The specified equations hg let the components retain the chosen structure maps g, instead of replacing them by their composites through X.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · full declaration
def locallyDirectedCoverHypercoverOver :
    GrothendieckTopology.OneHypercover.{max v w}
      (Scheme.zariskiTopology.over S) (Over.mk f) where
  __ := locallyDirectedCoverPreHypercoverOver (𝒰 := 𝒰) f g hg
  mem₀ := by
    rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_ofArrows]
    exact (locallyDirectedCoverHypercover 𝒰).mem₀
  mem₁ i j T p₁ p₂ h := by
    rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁]
    exact (locallyDirectedCoverHypercover 𝒰).mem₁ i j p₁.left p₂.left
      (congrArg (fun k : T ⟶ Over.mk f => k.left) h)
lemma

locallyDirectedCoverHypercoverOver_X

L112 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver_X
Documentation

The zero component has exactly the chosen structure map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · statement
lemma locallyDirectedCoverHypercoverOver_X (i : ULift.{v} 𝒰.I₀) :
    (locallyDirectedCoverHypercoverOver (𝒰 := 𝒰) f g hg).X i =
      Over.mk (g i.down)
lemma

locallyDirectedCoverHypercoverOver_f_left

L117 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver_f_left
Documentation

The covering arrow is the original covering arrow on underlying schemes.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · statement
lemma locallyDirectedCoverHypercoverOver_f_left (i : ULift.{v} 𝒰.I₀) :
    ((locallyDirectedCoverHypercoverOver (𝒰 := 𝒰) f g hg).f i).left = 𝒰.f i.down
lemma

locallyDirectedCoverHypercoverOver_Y

L121 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver_Y
Documentation

A common lower index contributes the corresponding chosen relative object.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · statement
lemma locallyDirectedCoverHypercoverOver_Y
    {i j : ULift.{v} 𝒰.I₀} (k : Σ l : 𝒰.I₀, (l ⟶ i.down) × (l ⟶ j.down)) :
    (locallyDirectedCoverHypercoverOver (𝒰 := 𝒰) f g hg).Y (i₁ := i) (i₂ := j) k =
      Over.mk (g k.1)
lemma

locallyDirectedCoverHypercoverOver_p₁_left

L127 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver_p₁_left
Documentation

The first overlap projection is the first transition of the original cover.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · statement
lemma locallyDirectedCoverHypercoverOver_p₁_left
    {i j : ULift.{v} 𝒰.I₀} (k : Σ l : 𝒰.I₀, (l ⟶ i.down) × (l ⟶ j.down)) :
    ((locallyDirectedCoverHypercoverOver (𝒰 := 𝒰) f g hg).p₁ (i₁ := i) (i₂ := j) k).left =
      𝒰.trans k.2.1
lemma

locallyDirectedCoverHypercoverOver_p₂_left

L133 ↗
SchemeTheory.WeilRestriction.locallyDirectedCoverHypercoverOver_p₂_left
Documentation

The second overlap projection is the second transition of the original cover.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {X S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{w} X)
  [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (f : X ⟶ S) (g : ∀ i : 𝒰.I₀, 𝒰.X i ⟶ S)
  (hg : ∀ i : 𝒰.I₀, 𝒰.f i ≫ f = g i)
Lean source · statement
lemma locallyDirectedCoverHypercoverOver_p₂_left
    {i j : ULift.{v} 𝒰.I₀} (k : Σ l : 𝒰.I₀, (l ⟶ i.down) × (l ⟶ j.down)) :
    ((locallyDirectedCoverHypercoverOver (𝒰 := 𝒰) f g hg).p₂ (i₁ := i) (i₂ := j) k).left =
      𝒰.trans k.2.2

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.