Documentation

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

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.

source
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
    Instances For
      source
      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
        Instances For
          source
          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 φ)
          source
          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
          source
          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
            Instances For
              source
              @[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 φ
              source
              @[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)
              source
              @[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✝
              source
              @[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)
              source
              @[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✝
              source
              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
                Instances For
                  source
                  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 β)
                  source
                  @[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₀)
                  source
                  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
                    Instances For
                      source
                      @[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₀
                      source
                      @[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
                      source
                      noncomputable 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
                        Instances For
                          source
                          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
                          source
                          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₀)
                          source
                          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.

                          source
                          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 φ)
                          source
                          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
                          source
                          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
                            Instances For
                              source
                              @[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 φ
                              source
                              @[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)
                              source
                              @[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✝
                              source
                              @[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)
                              source
                              @[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✝
                              source
                              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
                                Instances For
                                  source
                                  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
                                  source
                                  @[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₀)
                                  source
                                  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
                                    Instances For
                                      source
                                      @[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₀
                                      source
                                      @[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
                                      source
                                      noncomputable 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
                                        Instances For
                                          source
                                          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
                                          source
                                          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₀)
                                          source
                                          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.

                                          source
                                          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.

                                          Instances
                                            source
                                            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
                                            source
                                            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.

                                            Instances
                                              source
                                              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