ModuleGluedComparison.lean
Nyll.SchemeTheory.WeilRestriction.GluedComparison
4 declarations indexed from sourceView source ↗ Module documentation
Comparing glued representers with their local pieces
The cartesian squares of relative gluing identify each local representer with the pullback of the glued scheme. The resulting hom-set equivalence has an explicit inverse: compose a local map with its gluing inclusion.
Declarations
SchemeTheory.WeilRestriction.gluedLocalRepresenterInclusion
DocumentationThe local representer maps to the glued scheme 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))
[Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
SchemeTheory.WeilRestriction.gluedLocalRepresenterPullbackIso
DocumentationPulling the glued scheme back to a cover member recovers its local representer.
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))
[Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
SchemeTheory.WeilRestriction.gluedLocalRepresenterHomEquiv
DocumentationMaps from a test scheme over a cover member into the glued scheme are equivalent to maps into the corresponding local representer.
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))
[Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
SchemeTheory.WeilRestriction.gluedLocalRepresenterHomEquiv_symm
DocumentationThe inverse comparison is composition with the gluing inclusion.
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))
[Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]