Module

LocalRepresenterDiagram.lean

Nyll.SchemeTheory.WeilRestriction.LocalRepresenterDiagram

3 declarations indexed from sourceView source ↗

Module documentation

The diagram of local representing objects

Representers of restrictions of a fixed presheaf form a diagram over the base diagram. Its transition maps come from the representing equivalences, so their identity, composition, and pullback properties are consequences rather than additional gluing assumptions.

Imports2

Nyll.SchemeTheory.WeilRestriction.LocalRepresenters
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered

Imported by3

def

localRepresenterDiagram

L38 ↗

SchemeTheory.WeilRestriction.localRepresenterDiagram

Documentation

Local representers form a functor, with the transition maps determined by their universal elements.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
noncomputable section
universe u v w uJ vJ
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C] {J : Type uJ} [Category.{vJ} J]
  (F : Cᵒᵖ ⥤ Type w) (D : J ⥤ C) (W : ∀ j : J, Over (D.obj j))
  (h : ∀ j : J, (sliceRestriction F (D.obj j)).RepresentableBy (W j))

Lean source · full declaration

def localRepresenterDiagram : J ⥤ C where
  obj j := (W j).left
  map {i j} f := localRepresenterMap (h i) (h j) (D.map f)
  map_id i := by
    rw [D.map_id, localRepresenterMap_id]
  map_comp f g := by
    rw [D.map_comp, localRepresenterMap_comp]

def

localRepresenterProjection

L48 ↗

SchemeTheory.WeilRestriction.localRepresenterProjection

Documentation

The structure maps of local representers form a natural transformation to the base diagram.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
noncomputable section
universe u v w uJ vJ
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C] {J : Type uJ} [Category.{vJ} J]
  (F : Cᵒᵖ ⥤ Type w) (D : J ⥤ C) (W : ∀ j : J, Over (D.obj j))
  (h : ∀ j : J, (sliceRestriction F (D.obj j)).RepresentableBy (W j))

Lean source · full declaration

def localRepresenterProjection : localRepresenterDiagram F D W h ⟶ D where
  app j := (W j).hom
  naturality i j f := localRepresenterMap_w (h i) (h j) (D.map f)

lemma

localRepresenterProjection_equifibered

L53 ↗

SchemeTheory.WeilRestriction.localRepresenterProjection_equifibered

Documentation

Every transition square of the diagram of local representers is a pullback.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits
noncomputable section
universe u v w uJ vJ
namespace SchemeTheory.WeilRestriction
variable {C : Type u} [Category.{v} C] {J : Type uJ} [Category.{vJ} J]
  (F : Cᵒᵖ ⥤ Type w) (D : J ⥤ C) (W : ∀ j : J, Over (D.obj j))
  (h : ∀ j : J, (sliceRestriction F (D.obj j)).RepresentableBy (W j))

Lean source · statement

lemma localRepresenterProjection_equifibered [HasPullbacks C] :
    (localRepresenterProjection F D W h).Equifibered

Module documentation

The diagram of local representing objects

Declarations

localRepresenterDiagram

localRepresenterProjection

localRepresenterProjection_equifibered