Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ (Type u_1)}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P],
  CategoryTheory.Presieve.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F →
    ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
      [Finite 𝒰.I₀],
      CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)

Defined in

Mathlib.AlgebraicGeometry.Sites.BigZariski

Cited by

1 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsZariskiLocalAtSourceFinite