Theorems · Inductive type · category theory

CategoryTheory.GrothendieckTopology.Point

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → Type (max (max u v) (w + 1))

Given J a Grothendieck topology on a category C, a point of the site (C, J) consists of a functor fiber : C ⥤ Type w such that the category fiber.Elements is initially small (which allows defining the fiber functor on presheaves by taking colimits) and cofiltered (so that the fiber functor on presheaves is exact), and such that covering sieves induce jointly surjective maps on fibers (which allows to show that the fibers of a presheaf and its associated sheaf are isomorphic).

Defined in

Mathlib.CategoryTheory.Sites.Point.Basic

Cited by

123 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.Category