Documentation

Mathlib.CategoryTheory.StructuredArrow

The category of "structured arrows" #

For T : C ⥤ D, a T-structured arrow with source S : D is just a morphism S ⟶ T.obj Y, for some Y : C.

These form a category with morphisms g : Y ⟶ Y' making the obvious diagram commute.

We prove that 𝟙 (T.obj Y) is the initial object in T-structured objects with source T.obj Y.

The category of T-structured arrows with domain S : D (here T : C ⥤ D), has as its objects D-morphisms of the form S ⟶ T Y, for some Y : C, and morphisms C-morphisms Y ⟶ Y' making the obvious triangle commute.

Instances For

    The obvious projection functor from structured arrows.

    Instances For

      Construct a structured arrow from a morphism.

      Instances For

        To construct a morphism of structured arrows, we need a morphism of the objects underlying the target, and to check that the triangle commutes.

        Instances For

          Given a structured arrow X ⟶ T(Y), and an arrow Y ⟶ Y', we can construct a morphism of structured arrows given by (X ⟶ T(Y)) ⟶ (X ⟶ T(Y) ⟶ T(Y')).

          Instances For
            @[simp]
            theorem CategoryTheory.StructuredArrow.isoMk_inv_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} {f' : CategoryTheory.StructuredArrow S T} (g : f.right f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝) :
            (_ : f.left.as = f.left.as) = (_ : f.left.as = f.left.as)
            @[simp]
            theorem CategoryTheory.StructuredArrow.isoMk_hom_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} {f' : CategoryTheory.StructuredArrow S T} (g : f.right f'.right) (w : autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom) _auto✝) :
            (_ : f'.left.as = f'.left.as) = (_ : f'.left.as = f'.left.as)

            To construct an isomorphism of structured arrows, we need an isomorphism of the objects underlying the target, and to check that the triangle commutes.

            Instances For

              The converse of this is true with additional assumptions, see mono_iff_mono_right.

              Eta rule for structured arrows. Prefer StructuredArrow.eta for rewriting, since equality of objects tends to cause problems.

              @[simp]
              theorem CategoryTheory.StructuredArrow.eta_inv_left_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) :
              (_ : f.left.as = f.left.as) = (_ : f.left.as = f.left.as)

              A morphism between source objects S ⟶ S' contravariantly induces a functor between structured arrows, StructuredArrow S' T ⥤ StructuredArrow S T.

              Ideally this would be described as a 2-functor from D (promoted to a 2-category with equations as 2-morphisms) to Cat.

              Instances For

                An isomorphism S ≅ S' induces an equivalence StructuredArrow S T ≌ StructuredArrow S' T.

                Instances For
                  @[inline, reducible]

                  A structured arrow is called universal if it is initial.

                  Instances For

                    Two morphisms out of a universal T-structured arrow are equal if their image under T are equal after precomposing the universal arrow.

                    The category of S-costructured arrows with target T : D (here S : C ⥤ D), has as its objects D-morphisms of the form S Y ⟶ T, for some Y : C, and morphisms C-morphisms Y ⟶ Y' making the obvious triangle commute.

                    Instances For

                      The obvious projection functor from costructured arrows.

                      Instances For

                        Construct a costructured arrow from a morphism.

                        Instances For
                          @[simp]
                          theorem CategoryTheory.CostructuredArrow.homMk_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} {f' : CategoryTheory.CostructuredArrow S T} (g : f.left f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g) f'.hom = f.hom) _auto✝) :
                          (_ : f'.right.as = f'.right.as) = (_ : f'.right.as = f'.right.as)

                          To construct a morphism of costructured arrows, we need a morphism of the objects underlying the source, and to check that the triangle commutes.

                          Instances For

                            Given a costructured arrow S(Y) ⟶ X, and an arrow Y' ⟶ Y', we can construct a morphism of costructured arrows given by (S(Y) ⟶ X) ⟶ (S(Y') ⟶ S(Y) ⟶ X).

                            Instances For
                              @[simp]
                              theorem CategoryTheory.CostructuredArrow.isoMk_hom_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} {f' : CategoryTheory.CostructuredArrow S T} (g : f.left f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝) :
                              (_ : f'.right.as = f'.right.as) = (_ : f'.right.as = f'.right.as)
                              @[simp]
                              theorem CategoryTheory.CostructuredArrow.isoMk_inv_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} {f' : CategoryTheory.CostructuredArrow S T} (g : f.left f'.left) (w : autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom) _auto✝) :
                              (_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)

                              To construct an isomorphism of costructured arrows, we need an isomorphism of the objects underlying the source, and to check that the triangle commutes.

                              Instances For

                                The converse of this is true with additional assumptions, see epi_iff_epi_left.

                                Eta rule for costructured arrows. Prefer CostructuredArrow.eta for rewriting, as equality of objects tends to cause problems.

                                @[simp]
                                theorem CategoryTheory.CostructuredArrow.eta_inv_right_down_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) :
                                (_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)

                                A morphism between target objects T ⟶ T' covariantly induces a functor between costructured arrows, CostructuredArrow S T ⥤ CostructuredArrow S T'.

                                Ideally this would be described as a 2-functor from D (promoted to a 2-category with equations as 2-morphisms) to Cat.

                                Instances For

                                  A natural isomorphism S ≅ S' induces an equivalence CostrucutredArrow S T ≌ CostructuredArrow S' T.

                                  Instances For
                                    @[inline, reducible]

                                    A costructured arrow is called universal if it is terminal.

                                    Instances For

                                      Two morphisms into a universal S-costructured arrow are equal if their image under S are equal after postcomposing the universal arrow.

                                      @[simp]
                                      theorem CategoryTheory.Functor.toStructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (f : (Y : E) → X F.obj (G.obj Y)) (h : ∀ {Y Z : E} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) (Y : E) :
                                      @[simp]
                                      theorem CategoryTheory.Functor.toStructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (f : (Y : E) → X F.obj (G.obj Y)) (h : ∀ {Y Z : E} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) :
                                      ∀ {X Y : E} (g : X Y), (CategoryTheory.Functor.toStructuredArrow G X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g)

                                      Given X : D and F : C ⥤ D, to upgrade a functor G : E ⥤ C to a functor E ⥤ StructuredArrow X F, it suffices to provide maps X ⟶ F.obj (G.obj Y) for all Y making the obvious triangles involving all F.map (G.map g) commute.

                                      This is of course the same as providing a cone over F ⋙ G with cone point X, see Functor.toStructuredArrowIsoToStructuredArrow.

                                      Instances For

                                        Upgrading a functor E ⥤ C to a functor E ⥤ StructuredArrow X F and composing with the forgetful functor StructuredArrow X F ⥤ C recovers the original functor.

                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Functor.toCostructuredArrow_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (X : D) (f : (Y : E) → F.obj (G.obj Y) X) (h : ∀ {Y Z : E} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) (Y : E) :
                                          @[simp]
                                          theorem CategoryTheory.Functor.toCostructuredArrow_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (F : CategoryTheory.Functor C D) (X : D) (f : (Y : E) → F.obj (G.obj Y) X) (h : ∀ {Y Z : E} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) :
                                          ∀ {X Y : E} (g : X Y), (CategoryTheory.Functor.toCostructuredArrow G F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map g)

                                          Given F : C ⥤ D and X : D, to upgrade a functor G : E ⥤ C to a functor E ⥤ CostructuredArrow F X, it suffices to provide maps F.obj (G.obj Y) ⟶ X for all Y making the obvious triangles involving all F.map (G.map g) commute.

                                          This is of course the same as providing a cocone over F ⋙ G with cocone point X, see Functor.toCostructuredArrowIsoToCostructuredArrow.

                                          Instances For

                                            Upgrading a functor E ⥤ C to a functor E ⥤ CostructuredArrow F X and composing with the forgetful functor CostructuredArrow F X ⥤ C recovers the original functor.

                                            Instances For

                                              For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the category of structured arrows d ⟶ F.obj c to the category of costructured arrows F.op.obj c ⟶ (op d).

                                              Instances For

                                                For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the category of structured arrows op d ⟶ F.op.obj c to the category of costructured arrows F.obj c ⟶ d.

                                                Instances For

                                                  For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the category of costructured arrows F.obj c ⟶ d to the category of structured arrows op d ⟶ F.op.obj c.

                                                  Instances For

                                                    For a functor F : C ⥤ D and an object d : D, we obtain a contravariant functor from the category of costructured arrows F.op.obj c ⟶ op d to the category of structured arrows d ⟶ F.obj c.

                                                    Instances For

                                                      For a functor F : C ⥤ D and an object d : D, the category of structured arrows d ⟶ F.obj c is contravariantly equivalent to the category of costructured arrows F.op.obj c ⟶ op d.

                                                      Instances For

                                                        For a functor F : C ⥤ D and an object d : D, the category of costructured arrows F.obj c ⟶ d is contravariantly equivalent to the category of structured arrows op d ⟶ F.op.obj c.

                                                        Instances For