Theorems · Definition · category theory

CategoryTheory.GrothendieckTopology.Point.over

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [CategoryTheory.LocallySmall.{w, v, u} C] → (Φ : J.Point) → {X : C} → Φ.fiber.obj X → (J.over X).Point

Given a point Φ of a site (C, J), an object X : C, and x : Φ.fiber.obj X, this is the point of the site (Over X, J.over X) such that the fiber of an object of Over X corresponding to a morphism f : Y ⟶ X identifies to subtype of Φ.fiber.obj Y consisting of elements y such that Φ.fiber.map f y = x.

Defined in

Mathlib.CategoryTheory.Sites.Point.Over

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmall