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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
(j : J)
:
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)
Instances For
def
CategoryTheory.Functor.IsEventuallyConstantFrom
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
(i : J)
:
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)
Instances For
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_map
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
{i j : J}
(φ : i ⟶ j)
(π : j ⟶ i₀)
:
CategoryTheory.IsIso (F.map φ)
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.precomp
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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 φ)
Instances For
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
{i j : J}
(φ : i ⟶ j)
(hφ : Nonempty (j ⟶ i₀))
:
CategoryTheory.CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryTheory.CategoryStruct.id (F.obj i)
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp (F.map φ) (CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
{i j : J}
(φ : i ⟶ j)
(hφ : Nonempty (j ⟶ i₀))
:
CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryTheory.CategoryStruct.id (F.obj j)
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id_assoc
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryTheory.CategoryStruct.comp (F.map φ) h✝) = h✝
noncomputable def
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.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))
Instances For
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
(j j' : J)
(α : j' ⟶ i₀)
(β : j' ⟶ j)
:
h.coneπApp j = CategoryTheory.CategoryStruct.comp (h.isoMap α ⋯).inv (F.map β)
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
:
h.coneπApp i₀ = CategoryTheory.CategoryStruct.id (F.obj i₀)
noncomputable def
CategoryTheory.Functor.IsEventuallyConstantTo.cone
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
:
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 := ⋯ } }
Instances For
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
:
h.cone.pt = F.obj i₀
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.cone_π_app
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
:
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 := ⋯ }
Instances For
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
:
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
:
CategoryTheory.IsIso (c.π.app i₀)
theorem
CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit'
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantTo i₀)
[CategoryTheory.IsCofiltered J]
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(j : J)
(π : j ⟶ i₀)
:
CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
{i j : J}
(φ : i ⟶ j)
(ι : i₀ ⟶ i)
:
CategoryTheory.IsIso (F.map φ)
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.postcomp
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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 φ)
Instances For
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
{i j : J}
(φ : i ⟶ j)
(hφ : Nonempty (i₀ ⟶ i))
:
CategoryTheory.CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryTheory.CategoryStruct.id (F.obj i)
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id_assoc
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp (F.map φ) (CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
{i j : J}
(φ : i ⟶ j)
(hφ : Nonempty (i₀ ⟶ i))
:
CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (F.map φ) = CategoryTheory.CategoryStruct.id (F.obj j)
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.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)
:
CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryTheory.CategoryStruct.comp (F.map φ) h✝) = h✝
noncomputable def
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.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
Instances For
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
(j j' : J)
(α : j ⟶ j')
(β : i₀ ⟶ j')
:
h.coconeιApp j = CategoryTheory.CategoryStruct.comp (F.map α) (h.isoMap β ⋯).inv
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq_id
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_4, u_1} J]
[CategoryTheory.Category.{u_3, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
:
h.coconeιApp i₀ = CategoryTheory.CategoryStruct.id (F.obj i₀)
noncomputable def
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
:
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 := ⋯ } }
Instances For
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_pt
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
:
h.cocone.pt = F.obj i₀
@[simp]
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_ι_app
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
:
CategoryTheory.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 := ⋯ }
Instances For
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.hasColimit
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
:
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
:
CategoryTheory.IsIso (c.ι.app i₀)
theorem
CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit'
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
{F : CategoryTheory.Functor J C}
{i₀ : J}
(h : F.IsEventuallyConstantFrom i₀)
[CategoryTheory.IsFiltered J]
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
(j : J)
(ι : i₀ ⟶ j)
:
CategoryTheory.IsIso (c.ι.app j)
More general version of isIso_ι_of_isColimit.
class
CategoryTheory.IsCofiltered.IsEventuallyConstant
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
:
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
Instances
instance
CategoryTheory.IsCofiltered.instHasLimitOfIsEventuallyConstant
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
[hF : CategoryTheory.IsCofiltered.IsEventuallyConstant F]
[CategoryTheory.IsCofiltered J]
:
Equations
- ⋯ = ⋯
class
CategoryTheory.IsFiltered.IsEventuallyConstant
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
:
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
Instances
instance
CategoryTheory.IsFiltered.instHasColimitOfIsEventuallyConstant
{J : Type u_1}
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_1} J]
[CategoryTheory.Category.{u_4, u_2} C]
(F : CategoryTheory.Functor J C)
[hF : CategoryTheory.IsFiltered.IsEventuallyConstant F]
[CategoryTheory.IsFiltered J]
:
Equations
- ⋯ = ⋯