Documentation

Mathlib.CategoryTheory.Sites.Over

Localization

In this file, given a Grothendieck topology J on a category C and X : C, we construct a Grothendieck topology J.over X on the category Over X. In order to do this, we first construct a bijection Sieve.overEquiv Y : Sieve Y ≃ Sieve Y.left for all Y : Over X. Then, as it is stated in SGA 4 III 5.2.1, a sieve of Y : Over X is covering for J.over X if and only if the corresponding sieve of Y.left is covering for J. As a result, the forgetful functor Over.forget X : Over X ⥤ X is both cover-preserving and cover-lifting.

The equivalence Sieve Y ≃ Sieve Y.left for all Y : Over X.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Sieve.overEquiv_symm_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y.left) {Z : CategoryTheory.Over X} (f : Z Y) :
    ((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f S.arrows f.left

    The Grothendieck topology on the category Over X for any X : C that is induced by a Grothendieck topology on C.

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

      The pullback functor Sheaf J A ⥤ Sheaf (J.over X) A

      Equations
      Instances For
        Equations
        • =
        @[reducible, inline]

        The pullback functor Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A induced by a morphism f : X ⟶ Y.

        Equations
        Instances For
          @[reducible, inline]

          Given F : Sheaf J A and X : C, this is the pullback of F on J.over X.

          Equations
          • F.over X = (J.overPullback A X).obj F
          Instances For