Theorems · Theorem · category theory

CategoryTheory.Functor.thin_diagram_of_surjective

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J],
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    ∀ {i j : J} (f g : i ⟶ j), F.map f = F.map g

If F has all arrows surjective, then it "factors through a poset".

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty