Module

LocalRepresenters.lean

Nyll.SchemeTheory.WeilRestriction.LocalRepresenters

13 declarations indexed from sourceView source ↗

Module documentation

Canonical transitions between local representing objects

Restrict a presheaf on C to the slice over each object of C. Given representing objects on two slices, a morphism between the bases determines a canonical morphism between the representing objects. The universal elements make these transitions compatible with identities and composition.

If C has pullbacks, the transition square is a pullback. These constructions apply to C = Over S; the iterated slice equivalence then identifies the local restrictions with the usual presheaves on schemes over each local base.

Imports3

Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.Yoneda

Imported by6

abbrev

sliceRestriction

L40 ↗

SchemeTheory.WeilRestriction.sliceRestriction

Documentation

Restrict a presheaf to the slice over an object of its domain.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]

Lean source · statement

abbrev sliceRestriction (F : Cᵒᵖ ⥤ Type w) (U : C) : (Over U)ᵒᵖ ⥤ Type w

def

localRepresenterOverMap

L47 ↗

SchemeTheory.WeilRestriction.localRepresenterOverMap

Documentation

The canonical transition between local representers as a morphism over the target base.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

def localRepresenterOverMap
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    (Over.map a).obj WU ⟶ WV

def

localRepresenterMap

L55 ↗

SchemeTheory.WeilRestriction.localRepresenterMap

Documentation

The canonical transition sends the universal element on the target to the universal element on the source.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

def localRepresenterMap
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    WU.left ⟶ WV.left

lemma

localRepresenterMap_w

L62 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_w

Documentation

The transition commutes with the structure morphisms.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

lemma localRepresenterMap_w
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    localRepresenterMap hU hV a ≫ WV.hom = WU.hom ≫ a

lemma

localRepresenterMap_universal

L69 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_universal

Documentation

The defining compatibility between universal elements.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

lemma localRepresenterMap_universal
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    F.map (localRepresenterMap hU hV a).op (hV.homEquiv (𝟙 WV)) =
      hU.homEquiv (𝟙 WU)

lemma

localRepresenterMap_unique

L79 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_unique

Documentation

A transition is uniquely determined by its base map and universal element.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

lemma localRepresenterMap_unique
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V)
    (g : WU.left ⟶ WV.left) (hg : g ≫ WV.hom = WU.hom ≫ a)
    (hF : F.map g.op (hV.homEquiv (𝟙 WV)) = hU.homEquiv (𝟙 WU)) :
    g = localRepresenterMap hU hV a

lemma

localRepresenterMap_id

L95 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_id

Documentation

Canonical transitions preserve identity morphisms.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

lemma localRepresenterMap_id
    (hU : (sliceRestriction F U).RepresentableBy WU) :
    localRepresenterMap hU hU (𝟙 U) = 𝟙 WU.left

lemma

localRepresenterMap_comp

L107 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_comp

Documentation

Canonical transitions preserve composition.

Source context 7 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}

Lean source · statement

lemma localRepresenterMap_comp
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV)
    (hZ : (sliceRestriction F Z).RepresentableBy WZ)
    (a : U ⟶ V) (b : V ⟶ Z) :
    localRepresenterMap hU hZ (a ≫ b) =
      localRepresenterMap hU hV a ≫ localRepresenterMap hV hZ b

def

localRepresenterPullbackRepresentable

L134 ↗

SchemeTheory.WeilRestriction.localRepresenterPullbackRepresentable

Documentation

Restriction of a locally represented presheaf along a base morphism is represented by the pullback, via the map-pullback adjunction.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}
section Pullback
variable [HasPullbacks C]

Lean source · full declaration

def localRepresenterPullbackRepresentable
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    (sliceRestriction F U).RepresentableBy ((Over.pullback a).obj WV) where
  homEquiv {X} := ((Over.mapPullbackAdj a).homEquiv X WV).symm.trans hV.homEquiv
  homEquiv_comp {X X'} f g := by
    change hV.homEquiv
      (((Over.mapPullbackAdj a).homEquiv X WV).symm (f ≫ g)) = _
    rw [Adjunction.homEquiv_naturality_left_symm]
    exact hV.homEquiv_comp ((Over.map a).map f)
      (((Over.mapPullbackAdj a).homEquiv X' WV).symm g)

def

localRepresenterPullbackIso

L146 ↗

SchemeTheory.WeilRestriction.localRepresenterPullbackIso

Documentation

The canonical comparison with the pullback of a local representer.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}
section Pullback
variable [HasPullbacks C]

Lean source · statement

def localRepresenterPullbackIso
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    WU ≅ (Over.pullback a).obj WV

lemma

localRepresenterPullbackIso_homEquiv

L152 ↗

SchemeTheory.WeilRestriction.localRepresenterPullbackIso_homEquiv

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}
section Pullback
variable [HasPullbacks C]

Lean source · statement

lemma localRepresenterPullbackIso_homEquiv
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    (localRepresenterPullbackRepresentable hV a).homEquiv
      (localRepresenterPullbackIso hU hV a).hom = hU.homEquiv (𝟙 WU)

lemma

localRepresenterPullbackIso_hom_fst

L163 ↗

SchemeTheory.WeilRestriction.localRepresenterPullbackIso_hom_fst

Documentation

The pullback comparison recovers the canonical transition after projection.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}
section Pullback
variable [HasPullbacks C]

Lean source · statement

lemma localRepresenterPullbackIso_hom_fst
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    (localRepresenterPullbackIso hU hV a).hom.left ≫ pullback.fst WV.hom a =
      localRepresenterMap hU hV a

lemma

localRepresenterMap_isPullback

L182 ↗

SchemeTheory.WeilRestriction.localRepresenterMap_isPullback

Documentation

Canonical transitions give cartesian squares over their base morphisms.

Source context 9 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
universe u v w
noncomputable section
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C]
variable {F : Cᵒᵖ ⥤ Type w} {U V Z : C}
  {WU : Over U} {WV : Over V} {WZ : Over Z}
section Pullback
variable [HasPullbacks C]

Lean source · statement

lemma localRepresenterMap_isPullback
    (hU : (sliceRestriction F U).RepresentableBy WU)
    (hV : (sliceRestriction F V).RepresentableBy WV) (a : U ⟶ V) :
    IsPullback (localRepresenterMap hU hV a) WU.hom WV.hom a

Module documentation

Canonical transitions between local representing objects

Declarations