Theorems · Theorem · category theory

CategoryTheory.Functor.eventualRange_eq_iff

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J}
  [CategoryTheory.IsCofilteredOrEmpty J] {f : i ⟶ j},
  F.eventualRange j = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⊆
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp g f)))

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty