ModuleLocalRepresenterGluing.lean
Nyll.EtaleCohomology.Constructible.LocalRepresenterGluing
6 declarations indexed from sourceView source ↗ Module documentation
Gluing finite étale local representers on a directed open cover
The actual representing equivalences on the small étale sites determine all transition maps and their cartesian squares. Relative gluing then constructs a finite étale scheme on the whole base, whose restrictions are the chosen local schemes. No gluing comparisons or cocycle laws are assumed.
Declarations
EtaleCohomology.etaleOpenCoverDiagram
DocumentationRegard the directed open cover as a diagram in the base's small étale category.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
EtaleCohomology.etaleLocalRepresenterGluingData
DocumentationOrdinary local representations give actual relative gluing data via the slice equivalences of the small étale category.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
EtaleCohomology.etaleLocalRepresenterGluingData_app
DocumentationThe local structural maps of the gluing data are the original finite étale maps.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
EtaleCohomology.etaleLocalRepresenterGluingData_isFiniteEtale
DocumentationThe actual glued morphism is finite étale, by its cartesian local models.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
EtaleCohomology.etaleGluedLocalRepresenter
DocumentationThe finite étale scheme obtained by gluing the given local representers.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
EtaleCohomology.etaleGluedLocalRepresenter_isPullback
DocumentationEach original local representer is the genuine pullback of the glued scheme.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits SchemeTheory.WeilRestriction
universe u v
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
(𝒰 : X.OpenCover) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
variable (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
(h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
variable [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]