theorem
L29 ↗isStackFor_openCover
AlgebraicGeometry.Scheme.Modules.isStackFor_openCover
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isStackFor_openCover
universe v u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isStackFor_openCover (Y : Scheme.{u}) (𝒰 :
Y.OpenCover) :
((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).IsStackFor
(Presieve.ofArrows 𝒰.X 𝒰.f)