Module

IteratedSlice.lean

Nyll.SchemeTheory.WeilRestriction.IteratedSlice

1 declaration indexed from sourceView source ↗

Module documentation

Relative representers on an iterated slice

A representation on schemes over U, obtained by composition along U ⟶ S, also gives a representation on the slice of Over S over U ⟶ S. This is the form needed to glue local representers within the category Over S.

Imports4

Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Yoneda

Imported by4

def

representableByIteratedSlice

L34 ↗

SchemeTheory.WeilRestriction.representableByIteratedSlice

Documentation

Regard a local relative representer as a representer on the corresponding iterated slice.

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 representableByIteratedSlice {S U : Scheme.{u}} (f : U ⟶ S)
    (F : (Over S)ᵒᵖ ⥤ Type u) (W : Over U)
    (h : ((Over.map f).op ⋙ F).RepresentableBy W) :
    ((Over.forget (Over.mk f)).op ⋙ F).RepresentableBy
      ((Over.iteratedSliceEquiv (Over.mk f)).inverse.obj W)

Module documentation

Relative representers on an iterated slice

Declarations

representableByIteratedSlice