ModuleGluingData.lean
Nyll.SchemeTheory.WeilRestriction.GluingData
4 declarations indexed from sourceView source ↗ Module documentation
Gluing data from local relative representers
Local representations of one presheaf on Over S determine relative gluing data on a locally directed open cover. The transition maps and cartesian squares are constructed from universal elements, using the iterated slice equivalence to work in Over S throughout.
The resulting glued scheme is finite étale if each local representer is. Its global representing property is a separate sheaf-descent step.
Declarations
SchemeTheory.WeilRestriction.localRepresenterGluingData
DocumentationConstruct all the transition maps and pullback squares for local representers.
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.localRepresenterGluingData_app
DocumentationThe local structure maps of the constructed gluing data are the given ones.
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.gluedLocalRepresenter
DocumentationThe scheme obtained by gluing the local representers, with its map to the base.
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.gluedLocalRepresenter_isFiniteEtale
DocumentationFinite étaleness of the local representers descends to their glued scheme.
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₀]