Limits of eventually constant functors

If F : J ⥤ C is a functor from a cofiltered category, and j : J, we introduce a property F.IsEventuallyConstantTo j which says that for any f : i ⟶ j, the induced morphism F.map f is an isomorphism. Under this assumption, it is shown that F admits F.obj j as a limit (Functor.IsEventuallyConstantTo.isLimitCone).

A typeclass Cofiltered.IsEventuallyConstant is also introduced, and the dual results for filtered categories and colimits are also obtained.

def CategoryTheory.Functor.IsEventuallyConstantTo {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) (j : J) : Prop

A functor F : J ⥤ C is eventually constant to j : J if for any map f : i ⟶ j, the induced morphism F.map f is an isomorphism. If J is cofiltered, this implies F has a limit.

Equations

• F.IsEventuallyConstantTo j = ∀ ⦃i : J⦄ (f : i ⟶ j), CategoryTheory.IsIso (F.map f)

def CategoryTheory.Functor.IsEventuallyConstantFrom {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) (i : J) : Prop

A functor F : J ⥤ C is eventually constant from i : J if for any map f : i ⟶ j, the induced morphism F.map f is an isomorphism. If J is filtered, this implies F has a colimit.

Equations

• F.IsEventuallyConstantFrom i = ∀ ⦃j : J⦄ (f : i ⟶ j), CategoryTheory.IsIso (F.map f)

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isIso_map {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (π : j ⟶ i₀) : IsIso (F.map φ)

theorem CategoryTheory.Functor.IsEventuallyConstantTo.precomp {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {j : J} (f : j ⟶ i₀) : F.IsEventuallyConstantTo j

noncomputable def CategoryTheory.Functor.IsEventuallyConstantTo.isoMap {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) : F.obj i ≅ F.obj j

The isomorphism F.obj i ≅ F.obj j induced by φ : i ⟶ j, when h : F.IsEventuallyConstantTo i₀ and there exists a map j ⟶ i₀.

Equations

• h.isoMap φ hφ = CategoryTheory.asIso (F.map φ)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) : (h.isoMap φ hφ).hom = F.map φ

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) : CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryStruct.id (F.obj i)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) {Z : C} (h✝ : F.obj i ⟶ Z) : CategoryStruct.comp (F.map φ) (CategoryStruct.comp (h.isoMap φ hφ).inv h✝) = h✝

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) : CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryStruct.id (F.obj j)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id_assoc {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) {Z : C} (h✝ : F.obj j ⟶ Z) : CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryStruct.comp (F.map φ) h✝) = h✝

noncomputable def CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] (j : J) : F.obj i₀ ⟶ F.obj j

Auxiliary definition for IsEventuallyConstantTo.cone.

Equations

• h.coneπApp j = CategoryTheory.CategoryStruct.comp (h.isoMap (CategoryTheory.IsCofiltered.minToLeft i₀ j) ⋯).inv (F.map (CategoryTheory.IsCofiltered.minToRight i₀ j))

theorem CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] (j j' : J) (α : j' ⟶ i₀) (β : j' ⟶ j) : h.coneπApp j = CategoryStruct.comp (h.isoMap α ⋯).inv (F.map β)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] : h.coneπApp i₀ = CategoryStruct.id (F.obj i₀)

noncomputable def CategoryTheory.Functor.IsEventuallyConstantTo.cone {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] : Limits.Cone F

Given h : F.IsEventuallyConstantTo i₀, this is the (limit) cone for F whose point is F.obj i₀.

Equations

• h.cone = { pt := F.obj i₀, π := { app := h.coneπApp, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] : h.cone.pt = F.obj i₀

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantTo.cone_π_app {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] (j : J) : h.cone.π.app j = h.coneπApp j

def CategoryTheory.Functor.IsEventuallyConstantTo.isLimitCone {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] : Limits.IsLimit h.cone

When h : F.IsEventuallyConstantTo i₀, the limit of F exists and is F.obj i₀.

Equations

• h.isLimitCone = { lift := fun (s : CategoryTheory.Limits.Cone F) => s.π.app i₀, fac := ⋯, uniq := ⋯ }

theorem CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] : Limits.HasLimit F

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] {c : Limits.Cone F} (hc : Limits.IsLimit c) : IsIso (c.π.app i₀)

theorem CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit' {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantTo i₀) [IsCofiltered J] {c : Limits.Cone F} (hc : Limits.IsLimit c) (j : J) (π : j ⟶ i₀) : IsIso (c.π.app j)

More general version of isIso_π_of_isLimit.

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_map {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (ι : i₀ ⟶ i) : IsIso (F.map φ)

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.postcomp {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {j : J} (f : i₀ ⟶ j) : F.IsEventuallyConstantFrom j

noncomputable def CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) : F.obj i ≅ F.obj j

The isomorphism F.obj i ≅ F.obj j induced by φ : i ⟶ j, when h : F.IsEventuallyConstantFrom i₀ and there exists a map i₀ ⟶ i.

Equations

• h.isoMap φ hφ = CategoryTheory.asIso (F.map φ)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) : (h.isoMap φ hφ).hom = F.map φ

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) : CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryStruct.id (F.obj i)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id_assoc {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) {Z : C} (h✝ : F.obj i ⟶ Z) : CategoryStruct.comp (F.map φ) (CategoryStruct.comp (h.isoMap φ hφ).inv h✝) = h✝

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) : CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryStruct.id (F.obj j)

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) {Z : C} (h✝ : F.obj j ⟶ Z) : CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryStruct.comp (F.map φ) h✝) = h✝

noncomputable def CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] (j : J) : F.obj j ⟶ F.obj i₀

Auxiliary definition for IsEventuallyConstantFrom.cocone.

Equations

• h.coconeιApp j = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.IsFiltered.rightToMax i₀ j)) (h.isoMap (CategoryTheory.IsFiltered.leftToMax i₀ j) ⋯).inv

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] (j j' : J) (α : j ⟶ j') (β : i₀ ⟶ j') : h.coconeιApp j = CategoryStruct.comp (F.map α) (h.isoMap β ⋯).inv

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq_id {J : Type u_1} {C : Type u_2} [Category.{u_4, u_1} J] [Category.{u_3, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] : h.coconeιApp i₀ = CategoryStruct.id (F.obj i₀)

noncomputable def CategoryTheory.Functor.IsEventuallyConstantFrom.cocone {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] : Limits.Cocone F

Given h : F.IsEventuallyConstantFrom i₀, this is the (limit) cocone for F whose point is F.obj i₀.

Equations

• h.cocone = { pt := F.obj i₀, ι := { app := h.coconeιApp, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_pt {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] : h.cocone.pt = F.obj i₀

@[simp]

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ι_app {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] (j : J) : h.cocone.ι.app j = h.coconeιApp j

def CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitCocone {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] : Limits.IsColimit h.cocone

When h : F.IsEventuallyConstantFrom i₀, the colimit of F exists and is F.obj i₀.

Equations

• h.isColimitCocone = { desc := fun (s : CategoryTheory.Limits.Cocone F) => s.ι.app i₀, fac := ⋯, uniq := ⋯ }

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] : Limits.HasColimit F

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] {c : Limits.Cocone F} (hc : Limits.IsColimit c) : IsIso (c.ι.app i₀)

theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit' {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] {F : Functor J C} {i₀ : J} (h : F.IsEventuallyConstantFrom i₀) [IsFiltered J] {c : Limits.Cocone F} (hc : Limits.IsColimit c) (j : J) (ι : i₀ ⟶ j) : IsIso (c.ι.app j)

More general version of isIso_ι_of_isColimit.

class CategoryTheory.IsCofiltered.IsEventuallyConstant {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) : Prop

A functor F : J ⥤ C from a cofiltered category is eventually constant if there exists j : J, such that for any f : i ⟶ j, the induced map F.map f is an isomorphism.

• exists_isEventuallyConstantTo : ∃ (j : J), F.IsEventuallyConstantTo j

instance CategoryTheory.IsCofiltered.instHasLimitOfIsEventuallyConstant {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) [hF : IsEventuallyConstant F] [IsCofiltered J] : Limits.HasLimit F

class CategoryTheory.IsFiltered.IsEventuallyConstant {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) : Prop

A functor F : J ⥤ C from a filtered category is eventually constant if there exists i : J, such that for any f : i ⟶ j, the induced map F.map f is an isomorphism.

• exists_isEventuallyConstantFrom : ∃ (i : J), F.IsEventuallyConstantFrom i

instance CategoryTheory.IsFiltered.instHasColimitOfIsEventuallyConstant {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) [hF : IsEventuallyConstant F] [IsFiltered J] : Limits.HasColimit F