Theorems · Definition · category theory

CategoryTheory.Presieve.FactorsThruAlong

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} → CategoryTheory.Presieve Y → CategoryTheory.Presieve X → (Y ⟶ X) → Prop

Given a morphism f : Y ⟶ X, a presieve S on Y and presieve T on X, we say that `S` factors through `T` along `f`, written S.FactorsThruAlong T f, provided that for any morphism g : Z ⟶ Y in S, there exists some morphism e : W ⟶ X in T and some morphism i : Z ⟶ W such that the obvious square commutes: i ≫ e = g ≫ f. This is used in the definition of a coverage.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

11 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category