Theorems · Theorem · category theory

CategoryTheory.Coverage.pullback

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Coverage C) ⦃X Y : C⦄ (f : Y ⟶ X),
  ∀ S ∈ self.coverings X, ∃ T ∈ self.coverings Y, T.FactorsThruAlong S f

Given any covering sieve S on X and a morphism f : Y ⟶ X, there exists some covering sieve T on Y such that T factors through S along f.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

2 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Category