Module

Restriction.lean

Nyll.SchemeTheory.WeilRestriction.Restriction

1 declaration indexed from sourceView source ↗

Module documentation

Restricting local relative representers

If a presheaf on schemes over S is represented after restriction to schemes over X, then its restriction along Y ⟶ X ⟶ S is represented by the pullback of that local representer to Y. This transfers local representers to refinements of a cover.

Imports4

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Yoneda

Imported by2

def

representableByRestrictionBaseChange

L35 ↗

SchemeTheory.WeilRestriction.representableByRestrictionBaseChange

Documentation

Restriction along a composite is represented by the pullback of a local representer.

Source context 5 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

def representableByRestrictionBaseChange {S X Y : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ X)
    (F : (Over S)ᵒᵖ ⥤ Type u) (W : Over X)
    (h : ((Over.map f).op ⋙ F).RepresentableBy W) :
    ((Over.map (g ≫ f)).op ⋙ F).RepresentableBy ((Over.pullback g).obj W)

Module documentation

Restricting local relative representers

Declarations

representableByRestrictionBaseChange