Theorems · Theorem · category theory

CategoryTheory.Functor.surjective_toEventualRanges

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

If F satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a surjective functor.

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty