Theorems · Definition · category theory

CategoryTheory.GrothendieckTopology.pointBot

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.LocallySmall.{w, v, u} C] → C → ⊥.Point

If X is an object of C, this is the point of the site (C, ⊥) (whose sheaves are presheaves, see sheafBotEquivalence) corresponding to X.

Defined in

Mathlib.CategoryTheory.Sites.Point.Presheaf

Cited by

5 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall