Theorems · Theorem · category theory

CategoryTheory.Functor.eventually_injective

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

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmptyNonemptyFiniteNonemptyFinite