Module

OverTotalPresheaf.lean

Nyll.SchemeTheory.CategoryTheory.OverTotalPresheaf

23 declarations indexed from sourceView source ↗

Module documentation

Total presheaves over a slice category

A presheaf on the slice over S determines a presheaf on the original category by collecting its values over all arrows to S. Fibrewise transport relates their representations, and the total presheaf is a sheaf when the slice presheaf is a sheaf for the induced topology.

Imports3

Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Sites.Canonical
Mathlib.CategoryTheory.Sites.Over

Imported by28

abbrev

OverTotal

L48 ↗

CategoryTheory.Functor.OverTotal

Documentation

The total set of presheaf values over all arrows from T to S.

Source context 5 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)

Lean source · statement

abbrev OverTotal (T : C) : Type (max w v)

lemma

map_op_apply_eq_of_left_eq

L52 ↗

CategoryTheory.Functor.map_op_apply_eq_of_left_eq

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_apply_eq_of_left_eq {A B : Over S} (k k' : A ⟶ B)
    (h : k.left = k'.left) (x : G.obj (op B)) :
    G.map k.op x = G.map k'.op x

lemma

map_op_apply_eq_self

L57 ↗

CategoryTheory.Functor.map_op_apply_eq_self

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_apply_eq_self {A : Over S} (k : A ⟶ A) (h : k.left = 𝟙 _) (x : G.obj (op A)) :
    G.map k.op x = x

lemma

map_op_map_op_apply

L61 ↗

CategoryTheory.Functor.map_op_map_op_apply

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_map_op_apply {A B B' : Over S} (k : A ⟶ B) (k' : B ⟶ B') (x : G.obj (op B')) :
    G.map k.op (G.map k'.op x) = G.map (k ≫ k').op x

lemma

map_op_map_op_apply_eq_self

L65 ↗

CategoryTheory.Functor.map_op_map_op_apply_eq_self

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_map_op_apply_eq_self {A B : Over S} (k : A ⟶ B) (k' : B ⟶ A) (h : (k ≫ k').left = 𝟙 _)
    (x : G.obj (op A)) : G.map k.op (G.map k'.op x) = x

lemma

map_op_map_op_map_op_apply_eq_self

L70 ↗

CategoryTheory.Functor.map_op_map_op_map_op_apply_eq_self

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_map_op_map_op_apply_eq_self {A B B' : Over S} (k : A ⟶ B) (k' : B ⟶ B') (k'' : B' ⟶ A)
    (h : (k ≫ k' ≫ k'').left = 𝟙 _) (x : G.obj (op A)) :
    G.map k.op (G.map k'.op (G.map k''.op x)) = x

lemma

map_op_map_op_apply_eq

L76 ↗

CategoryTheory.Functor.map_op_map_op_apply_eq

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · statement

lemma map_op_map_op_apply_eq {A B B' D : Over S} (k : A ⟶ B) (k' : B ⟶ B') (l : A ⟶ D) (l' : D ⟶ B')
    (h : (k ≫ k').left = (l ≫ l').left) (x : G.obj (op B')) :
    G.map k.op (G.map k'.op x) = G.map l.op (G.map l'.op x)

lemma

ext'

L82 ↗

CategoryTheory.Functor.OverTotal.ext'

Source context 6 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}

Lean source · full declaration

lemma OverTotal.ext' {T : C} {a b : G.OverTotal T} (h₁ : a.1 = b.1)
    (h₂ : G.map (Over.homMk (𝟙 T) (by simp [h₁]) : Over.mk b.1 ⟶ Over.mk a.1).op a.2 = b.2) :
    a = b := by
  obtain ⟨t, x⟩ := a
  obtain ⟨t', y⟩ := b
  obtain rfl : t = t' := h₁
  simp only [Sigma.mk.injEq, heq_eq_eq, true_and]
  dsimp only at h₂
  rw [← h₂]
  symm
  exact map_op_apply_eq_self _ (by simp) x

def

overTotal

L97 ↗

CategoryTheory.Functor.overTotal

Documentation

The presheaf on C obtained by taking the total set of values over arrows to S.

Source context 7 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)

Lean source · full declaration

def overTotal : Cᵒᵖ ⥤ Type (max w v) where
  obj T := G.OverTotal T.unop
  map {T T'} φ := TypeCat.ofHom fun a =>
    ⟨φ.unop ≫ a.1, G.map (Over.homMk φ.unop rfl : Over.mk (φ.unop ≫ a.1) ⟶ Over.mk a.1).op a.2⟩
  map_id T := TypeCat.homEquiv.injective (funext fun a =>
    OverTotal.ext' (by simp) (map_op_map_op_apply_eq_self _ _ (by
      change (𝟙 _) ≫ (𝟙 _) = 𝟙 _
      exact id_comp _) _))
  map_comp {T T' T''} φ ψ := TypeCat.homEquiv.injective (funext fun a =>
    OverTotal.ext' (by simp) (map_op_map_op_apply_eq _ _ _ _ (by
      change (𝟙 _) ≫ (ψ.unop ≫ φ.unop) = ψ.unop ≫ φ.unop
      exact id_comp _) _))

lemma

overTotal_map_fst

L110 ↗

CategoryTheory.Functor.overTotal_map_fst

Source context 7 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)

Lean source · statement

lemma overTotal_map_fst {T T' : Cᵒᵖ} (φ : T ⟶ T') (a : G.overTotal.obj T) :
    (G.overTotal.map φ a).1 = φ.unop ≫ a.1

def

toFibre

L116 ↗

CategoryTheory.Functor.OverTotal.toFibre

Documentation

Transport a total-presheaf element whose base arrow is T.hom to the fibre G(T).

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

def OverTotal.toFibre (T : Over S) (b : G.OverTotal T.left) (hb : b.1 = T.hom) : G.obj (op T)

lemma

toFibre_congr

L119 ↗

CategoryTheory.Functor.OverTotal.toFibre_congr

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

lemma OverTotal.toFibre_congr (T : Over S) {b b' : G.OverTotal T.left}
    (h : b = b') (hb : b.1 = T.hom)
    (hb' : b'.1 = T.hom) : OverTotal.toFibre T b hb = OverTotal.toFibre T b' hb'

def

ofFibre

L125 ↗

CategoryTheory.Functor.OverTotal.ofFibre

Documentation

Include a section of G(T) in the total presheaf over the arrow T.hom.

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

def OverTotal.ofFibre (T : Over S) (x : G.obj (op T)) : G.OverTotal T.left

lemma

ofFibre_fst

L128 ↗

CategoryTheory.Functor.OverTotal.ofFibre_fst

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

lemma OverTotal.ofFibre_fst (T : Over S) (x : G.obj (op T)) :
    (OverTotal.ofFibre T x).1 = T.hom

lemma

toFibre_ofFibre

L131 ↗

CategoryTheory.Functor.OverTotal.toFibre_ofFibre

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

lemma OverTotal.toFibre_ofFibre (T : Over S) (x : G.obj (op T)) :
    OverTotal.toFibre T (OverTotal.ofFibre T x) rfl = x

lemma

ofFibre_toFibre

L137 ↗

CategoryTheory.Functor.OverTotal.ofFibre_toFibre

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

lemma OverTotal.ofFibre_toFibre (T : Over S) (b : G.OverTotal T.left) (hb : b.1 = T.hom) :
    OverTotal.ofFibre T (OverTotal.toFibre T b hb) = b

lemma

toFibre_naturality

L143 ↗

CategoryTheory.Functor.OverTotal.toFibre_naturality

Source context 8 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}

Lean source · statement

lemma OverTotal.toFibre_naturality {T T' : Over S} (φ : T ⟶ T')
    (b : G.OverTotal T'.left) (hb : b.1 = T'.hom)
    (hb' : (G.overTotal.map φ.left.op b).1 = T.hom) :
    OverTotal.toFibre T (G.overTotal.map φ.left.op b) hb' =
      G.map φ.op (OverTotal.toFibre T' b hb)

def

overTotalBase

L158 ↗

CategoryTheory.Functor.RepresentableBy.overTotalBase

Documentation

The arrow from the representing object to S determined by its universal total-presheaf element.

Source context 10 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}
namespace RepresentableBy
variable {Y : C} (e : G.overTotal.RepresentableBy Y)

Lean source · statement

def overTotalBase : Y ⟶ S

lemma

overTotal_homEquiv_fst

L160 ↗

CategoryTheory.Functor.RepresentableBy.overTotal_homEquiv_fst

Source context 10 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}
namespace RepresentableBy
variable {Y : C} (e : G.overTotal.RepresentableBy Y)

Lean source · statement

lemma overTotal_homEquiv_fst {T : C} (k : T ⟶ Y) : (e.homEquiv k).1 = k ≫ e.overTotalBase

def

ofOverTotal

L168 ↗

CategoryTheory.Functor.RepresentableBy.ofOverTotal

Documentation

A representation of the total presheaf induces a representation of G by the representing object over S.

Source context 10 commands

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

section OverTotalPresheafImplementation
open CategoryTheory Category Opposite
namespace CategoryTheory.Functor
universe w v u
variable {C : Type u} [Category.{v} C] {S : C} (G : (Over S)ᵒᵖ ⥤ Type w)
variable {G}
variable (G)
variable {G}
namespace RepresentableBy
variable {Y : C} (e : G.overTotal.RepresentableBy Y)

Lean source · full declaration

def ofOverTotal : G.RepresentableBy (Over.mk e.overTotalBase) where
  homEquiv {T} :=
    { toFun := fun g => OverTotal.toFibre T (e.homEquiv g.left)
        (by rw [overTotal_homEquiv_fst]; exact Over.w g)
      invFun := fun x => Over.homMk (e.homEquiv.symm (OverTotal.ofFibre T x)) (by
        have h := e.overTotal_homEquiv_fst (e.homEquiv.symm (OverTotal.ofFibre T x))
        exact h.symm.trans
          (congrArg Sigma.fst (e.homEquiv.apply_symm_apply (OverTotal.ofFibre T x))))
      left_inv := fun g => by
        apply Over.OverMorphism.ext
        simp only [Over.homMk_left]
        apply e.homEquiv.injective
        exact (e.homEquiv.apply_symm_apply _).trans
          (OverTotal.ofFibre_toFibre T (e.homEquiv g.left) _)
      right_inv := fun x =>
        (OverTotal.toFibre_congr T
          (e.homEquiv.apply_symm_apply (OverTotal.ofFibre T x)) _ rfl).trans
          (OverTotal.toFibre_ofFibre T x) }
  homEquiv_comp {T T'} φ g := by
    have hg : (e.homEquiv g.left).1 = T'.hom := by
      rw [overTotal_homEquiv_fst]; exact Over.w g
    have hφg : (e.homEquiv (φ ≫ g).left).1 = T.hom := by
      rw [overTotal_homEquiv_fst]; exact Over.w (φ ≫ g)
    have hb' : (G.overTotal.map φ.left.op (e.homEquiv g.left)).1 = T.hom := by
      rw [overTotal_map_fst, overTotal_homEquiv_fst, Quiver.Hom.unop_op, ← assoc]
      exact Over.w (φ ≫ g)
    calc OverTotal.toFibre T (e.homEquiv (φ ≫ g).left) hφg
        = OverTotal.toFibre T (G.overTotal.map φ.left.op (e.homEquiv g.left)) hb' :=
          OverTotal.toFibre_congr T (e.homEquiv_comp φ.left g.left) hφg hb'
      _ = G.map φ.op (OverTotal.toFibre T' (e.homEquiv g.left) hg) :=
          OverTotal.toFibre_naturality φ _ hg hb'

lemma

map_op_map_op_apply_eq_map_op

L214 ↗

CategoryTheory.Functor.map_op_map_op_apply_eq_map_op

Source context 4 commands

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

universe w v u
namespace CategoryTheory.Functor
open CategoryTheory Category Opposite
variable {C : Type u} [Category.{v} C] {S : C} {G : (Over S)ᵒᵖ ⥤ Type w}

Lean source · statement

lemma map_op_map_op_apply_eq_map_op {A B B' : Over S} (k : A ⟶ B) (k' : B ⟶ B') (l : A ⟶ B')
    (h : (k ≫ k').left = l.left) (x : G.obj (op B')) :
    G.map k.op (G.map k'.op x) = G.map l.op x

lemma

ofFibre_mk

L220 ↗

CategoryTheory.Functor.OverTotal.ofFibre_mk

Source context 4 commands

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

universe w v u
namespace CategoryTheory.Functor
open CategoryTheory Category Opposite
variable {C : Type u} [Category.{v} C] {S : C} {G : (Over S)ᵒᵖ ⥤ Type w}

Lean source · statement

lemma OverTotal.ofFibre_mk {T : C} (s : T ⟶ S) (x : G.obj (op (Over.mk s))) :
    OverTotal.ofFibre (Over.mk s) x = ⟨s, x⟩

theorem

overTotal_isSheaf

L228 ↗

CategoryTheory.Functor.overTotal_isSheaf

Source context 5 commands

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

universe w v u
namespace CategoryTheory.Functor
open CategoryTheory Category Opposite
variable {C : Type u} [Category.{v} C] {S : C} {G : (Over S)ᵒᵖ ⥤ Type w}
variable (G)

Lean source · statement

theorem overTotal_isSheaf (J : GrothendieckTopology C) [J.Subcanonical]
    (hG : Presieve.IsSheaf (J.over S) G) : Presieve.IsSheaf J G.overTotal

Module documentation

Total presheaves over a slice category

Declarations