ModuleGluedUniversal.lean
Nyll.SchemeTheory.WeilRestriction.GluedUniversal
5 declarations indexed from sourceView source ↗ Module documentation
The universal section of glued local representers
The canonical transitions between local representers preserve their universal elements. These elements therefore form a compatible family on the locally directed cover of the glued scheme. The sheaf condition supplies a global section whose restriction to every local representer is its universal element.
Declarations
SchemeTheory.WeilRestriction.localRepresenterUniversalSection
DocumentationThe universal element of a local representer, viewed over the original base.
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
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (F : (Over S)ᵒᵖ ⥤ Type u)
(𝒰 : S.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
(W : ∀ i : 𝒰.I₀, Over (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((Over.map (𝒰.f i)).op ⋙ F).RepresentableBy (W i))
SchemeTheory.WeilRestriction.gluedLocalRepresenterHypercover
DocumentationThe Zariski hypercover of the glued representer given by its local representing 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
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (F : (Over S)ᵒᵖ ⥤ Type u)
(𝒰 : S.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
(W : ∀ i : 𝒰.I₀, Over (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((Over.map (𝒰.f i)).op ⋙ F).RepresentableBy (W i))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
SchemeTheory.WeilRestriction.gluedLocalRepresenterCompatibleSections
DocumentationThe compatible universal sections on the hypercover of the glued local representers.
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
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (F : (Over S)ᵒᵖ ⥤ Type u)
(𝒰 : S.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
(W : ∀ i : 𝒰.I₀, Over (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((Over.map (𝒰.f i)).op ⋙ F).RepresentableBy (W i))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
SchemeTheory.WeilRestriction.gluedLocalRepresenterUniversalSection
DocumentationThe local universal elements glue to a section on the glued representer.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (F : (Over S)ᵒᵖ ⥤ Type u)
(𝒰 : S.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
(W : ∀ i : 𝒰.I₀, Over (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((Over.map (𝒰.f i)).op ⋙ F).RepresentableBy (W i))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
variable (hF : Presheaf.IsSheaf (Scheme.zariskiTopology.over S) F)
SchemeTheory.WeilRestriction.gluedLocalRepresenterUniversalSection_restrict
DocumentationRestricting the glued section recovers the corresponding local universal element.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (F : (Over S)ᵒᵖ ⥤ Type u)
(𝒰 : S.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
(W : ∀ i : 𝒰.I₀, Over (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((Over.map (𝒰.f i)).op ⋙ F).RepresentableBy (W i))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
variable (hF : Presheaf.IsSheaf (Scheme.zariskiTopology.over S) F)