Documentation

Mathlib.CategoryTheory.Comma.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.

Equations
Instances For

    Construct a structured arrow from a morphism.

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

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.StructuredArrow.homMk'_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right Y') :
        (f.homMk' g).right = g

        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')).

        Equations
        Instances For

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

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

            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.

            Equations
            Instances For

              The identity structured arrow is initial.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                If F is an equivalence, then so is the functor (S, F ⋙ G) ⥤ (S, G).

                Equations
                • =

                The functor (S, F) ⥤ (G(S), F ⋙ G).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  If G is fully faithful, then post S F G : (S, F) ⥤ (G(S), F ⋙ G) is an equivalence.

                  Equations
                  • =

                  The functor StructuredArrow L R ⥤ StructuredArrow L' R' that is deduced from a natural transformation R ⋙ G ⟶ F ⋙ R' and a morphism L' ⟶ G.obj L.

                  Equations
                  Instances For
                    Equations
                    • =
                    noncomputable instance CategoryTheory.StructuredArrow.isEquivalenceMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' G.obj L) (β : R.comp G F.comp R') [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :
                    Equations
                    • =
                    @[reducible, inline]

                    A structured arrow is called universal if it is initial.

                    Equations
                    Instances For

                      The family of morphisms out of a universal arrow.

                      Equations
                      Instances For
                        @[simp]

                        Any structured arrow factors through a universal arrow.

                        theorem CategoryTheory.StructuredArrow.IsUniversal.hom_ext {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} (h : f.IsUniversal) {c : C} {η : f.right c} {η' : f.right c} (w : CategoryTheory.CategoryStruct.comp f.hom (T.map η) = CategoryTheory.CategoryStruct.comp f.hom (T.map η')) :
                        η = η'

                        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.

                        Equations
                        Instances For

                          Construct a costructured arrow from a morphism.

                          Equations
                          Instances For

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

                            Equations
                            Instances For
                              @[simp]

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

                              Equations
                              Instances For

                                Variant of homMk' where both objects are applications of mk.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

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

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

                                    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.

                                    Equations
                                    Instances For

                                      The identity costructured arrow is terminal.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        If F is an equivalence, then so is the functor (F ⋙ G, S) ⥤ (G, S).

                                        Equations
                                        • =

                                        The functor (F, S) ⥤ (F ⋙ G, G(S)).

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          If G is fully faithful, then post F G S : (F, S) ⥤ (F ⋙ G, G(S)) is an equivalence.

                                          Equations
                                          • =

                                          The functor CostructuredArrow S T ⥤ CostructuredArrow U V that is deduced from a natural transformation F ⋙ U ⟶ S ⋙ G and a morphism G.obj T ⟶ V

                                          Equations
                                          Instances For
                                            noncomputable instance CategoryTheory.CostructuredArrow.isEquivalenceMap₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U S.comp G) (β : G.obj T V) [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :
                                            Equations
                                            • =
                                            @[reducible, inline]

                                            A costructured arrow is called universal if it is terminal.

                                            Equations
                                            Instances For

                                              The family of morphisms into a universal arrow.

                                              Equations
                                              Instances For
                                                @[simp]

                                                Any costructured arrow factors through a universal arrow.

                                                theorem CategoryTheory.CostructuredArrow.IsUniversal.hom_ext {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} (h : f.IsUniversal) {c : C} {η : c f.left} {η' : c f.left} (w : CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom) :
                                                η = η'

                                                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_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_1 Y : E} (g : X_1 Y), (G.toStructuredArrow X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g)
                                                @[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) :
                                                (G.toStructuredArrow X F f h).obj Y = CategoryTheory.StructuredArrow.mk (f Y)

                                                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.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def CategoryTheory.Functor.toStructuredArrowCompProj {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) :
                                                  (G.toStructuredArrow X F f ).comp (CategoryTheory.StructuredArrow.proj X F) G

                                                  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.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Functor.toStructuredArrow_comp_proj {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) :
                                                    (G.toStructuredArrow X F f ).comp (CategoryTheory.StructuredArrow.proj X F) = G
                                                    @[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_1 Y : E} (g : X_1 Y), (G.toCostructuredArrow F X f h).map g = CategoryTheory.CostructuredArrow.homMk (G.map g)
                                                    @[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) :
                                                    (G.toCostructuredArrow F X f h).obj Y = CategoryTheory.CostructuredArrow.mk (f Y)

                                                    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.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def CategoryTheory.Functor.toCostructuredArrowCompProj {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) :
                                                      (G.toCostructuredArrow F X f ).comp (CategoryTheory.CostructuredArrow.proj F X) G

                                                      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.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.Functor.toCostructuredArrow_comp_proj {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) :
                                                        (G.toCostructuredArrow F X f ).comp (CategoryTheory.CostructuredArrow.proj F X) = G

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

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        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.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          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.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            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.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              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.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                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.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For