Documentation

Mathlib.CategoryTheory.Sites.Subcanonical

Subcanonical Grothendieck topologies #

This file provides some API for the Yoneda embedding into the category of sheaves for a subcanonical Grothendieck topology.

The equivalence between natural transformations from the yoneda embedding (to the sheaf category) and elements of F.val.obj X.

Equations
Instances For

    Variant of yonedaEquiv_naturality with general g. This is technically strictly more general than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

    See also map_yonedaEquiv' for a more general version.

    Variant of map_yonedaEquiv with general g. This is technically strictly more general than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

    Two morphisms of sheaves of types P ⟶ Q coincide if the precompositions with morphisms yoneda.obj X ⟶ P agree.

    The Yoneda embedding into a category of sheaves taking values in sets possibly larger than the morphisms in the defining site.

    Equations
    Instances For

      A version of yonedaEquiv for yonedaULift.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]

        Variant of yonedaEquiv_naturality with general g. This is technically strictly more general than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

        theorem CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.Subcanonical] {X Y : C} {F : Sheaf J (Type (max v v'))} (f : (yonedaULift.{v', v, u} J).obj X F) (g : Y X) :
        F.val.map g.op (J.yonedaULiftEquiv f) = f.val.app (Opposite.op Y) { down := g }

        See also map_yonedaEquiv' for a more general version.

        Variant of map_yonedaEquiv with general g. This is technically strictly more general than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

        Two morphisms of sheaves of types P ⟶ Q coincide if the precompositions with morphisms yoneda.obj X ⟶ P agree.