Theorems · Theorem · category theory

CategoryTheory.Functor.toPreimages_nonempty_of_surjective

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

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmptyNonempty