Module

GluedRepresentable.lean

Nyll.SchemeTheory.WeilRestriction.GluedRepresentable

4 declarations indexed from sourceView source ↗

Module documentation

Representability by gluing local relative representers

The universal section constructed from the local universal elements induces a map from the Yoneda presheaf of the glued scheme. Its restriction to each cover member is a bijection, by the cartesian gluing square and the local representing equivalence. The sheaf condition then makes this map an isomorphism globally.

Imports7

Nyll.SchemeTheory.WeilRestriction.GluedUniversal
Nyll.SchemeTheory.WeilRestriction.LocalIsomorphism
Mathlib.CategoryTheory.Sites.Subcanonical
Mathlib.CategoryTheory.Sites.SubcanonicalOver
Nyll.SchemeTheory.WeilRestriction.GluedComparison
Nyll.SchemeTheory.WeilRestriction.GluingData
Nyll.SchemeTheory.WeilRestriction.IteratedSlice

Imported by4

def

gluedLocalRepresenterEvaluationEquiv

L45 ↗

SchemeTheory.WeilRestriction.gluedLocalRepresenterEvaluationEquiv

Documentation

The local representing equivalence, expressed on maps into the glued scheme.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite 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₀]

Lean source · statement

def gluedLocalRepresenterEvaluationEquiv (i : 𝒰.I₀) (T : Over (𝒰.X i)) :
    ((Over.map (𝒰.f i)).obj T ⟶ gluedLocalRepresenter F 𝒰 W h) ≃
      F.obj (op ((Over.map (𝒰.f i)).obj T))

lemma

gluedLocalRepresenterUniversalSection_eval

L56 ↗

SchemeTheory.WeilRestriction.gluedLocalRepresenterUniversalSection_eval

Documentation

Evaluation of the glued universal section agrees with the local representing equivalence.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite 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₀]
variable (hF : Presheaf.IsSheaf (Scheme.zariskiTopology.over S) F)

Lean source · statement

lemma gluedLocalRepresenterUniversalSection_eval (i : 𝒰.I₀) (T : Over (𝒰.X i))
    (g : (Over.map (𝒰.f i)).obj T ⟶ gluedLocalRepresenter F 𝒰 W h) :
    (yonedaEquiv.symm (gluedLocalRepresenterUniversalSection F 𝒰 W h hF)).app
        (op ((Over.map (𝒰.f i)).obj T)) g =
      gluedLocalRepresenterEvaluationEquiv F 𝒰 W h i T g

lemma

gluedLocalRepresenterUniversalSection_bijective

L77 ↗

SchemeTheory.WeilRestriction.gluedLocalRepresenterUniversalSection_bijective

Documentation

Evaluation at the glued universal section is bijective on every local test scheme.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite 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₀]
variable (hF : Presheaf.IsSheaf (Scheme.zariskiTopology.over S) F)

Lean source · statement

lemma gluedLocalRepresenterUniversalSection_bijective (i : 𝒰.I₀) (T : Over (𝒰.X i)) :
    Function.Bijective
      ((yonedaEquiv.symm (gluedLocalRepresenterUniversalSection F 𝒰 W h hF)).app
        (op ((Over.map (𝒰.f i)).obj T)))

def

gluedLocalRepresentable

L94 ↗

SchemeTheory.WeilRestriction.gluedLocalRepresentable

Documentation

A sheaf with local relative representers is represented by their glued scheme.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite 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₀]
variable (hF : Presheaf.IsSheaf (Scheme.zariskiTopology.over S) F)

Lean source · statement

def gluedLocalRepresentable : F.RepresentableBy (gluedLocalRepresenter F 𝒰 W h)

Module documentation

Representability by gluing local relative representers

Declarations

gluedLocalRepresenterEvaluationEquiv

gluedLocalRepresenterUniversalSection_eval

gluedLocalRepresenterUniversalSection_bijective

gluedLocalRepresentable