Documentation

Mathlib.CategoryTheory.Comma.Arrow

The category of arrows #

The category of arrows, with morphisms commutative squares. We set this up as a specialization of the comma category Comma L R, where L and R are both the identity functor.

Tags #

comma, arrow

The arrow category of T has as objects all morphisms in T and as morphisms commutative squares in T.

Equations
Instances For
    theorem CategoryTheory.Arrow.hom_ext {T : Type u} [CategoryTheory.Category.{v, u} T] {X : CategoryTheory.Arrow T} {Y : CategoryTheory.Arrow T} (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
    f = g
    @[simp]
    theorem CategoryTheory.Arrow.mk_hom {T : Type u} [CategoryTheory.Category.{v, u} T] {X : T} {Y : T} (f : X Y) :
    @[simp]
    theorem CategoryTheory.Arrow.mk_left {T : Type u} [CategoryTheory.Category.{v, u} T] {X : T} {Y : T} (f : X Y) :
    @[simp]
    theorem CategoryTheory.Arrow.mk_right {T : Type u} [CategoryTheory.Category.{v, u} T] {X : T} {Y : T} (f : X Y) :

    An object in the arrow category is simply a morphism in T.

    Equations
    Instances For
      theorem CategoryTheory.Arrow.mk_injective {T : Type u} [CategoryTheory.Category.{v, u} T] (A : T) (B : T) :
      Function.Injective CategoryTheory.Arrow.mk
      Equations
      • CategoryTheory.Arrow.instCoeOutHom = { coe := CategoryTheory.Arrow.mk }

      A morphism in the arrow category is a commutative square connecting two objects of the arrow category.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Arrow.homMk'_left {T : Type u} [CategoryTheory.Category.{v, u} T] {X : T} {Y : T} {f : X Y} {P : T} {Q : T} {g : P Q} {u : X P} {v : Y Q} (w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v) :
        @[simp]
        theorem CategoryTheory.Arrow.homMk'_right {T : Type u} [CategoryTheory.Category.{v, u} T] {X : T} {Y : T} {f : X Y} {P : T} {Q : T} {g : P Q} {u : X P} {v : Y Q} (w : CategoryTheory.CategoryStruct.comp u g = CategoryTheory.CategoryStruct.comp f v) :

        We can also build a morphism in the arrow category out of any commutative square in T.

        Equations
        Instances For

          Create an isomorphism between arrows, by providing isomorphisms between the domains and codomains, and a proof that the square commutes.

          Equations
          Instances For
            @[reducible, inline]
            abbrev CategoryTheory.Arrow.isoMk' {T : Type u} [CategoryTheory.Category.{v, u} T] {W : T} {X : T} {Y : T} {Z : T} (f : W X) (g : Y Z) (e₁ : W Y) (e₂ : X Z) (h : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom g = CategoryTheory.CategoryStruct.comp f e₂.hom) _auto✝) :

            A variant of Arrow.isoMk that creates an iso between two Arrow.mks with a better type signature.

            Equations
            Instances For
              theorem CategoryTheory.Arrow.hom.congr_left {T : Type u} [CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {g : CategoryTheory.Arrow T} {φ₁ : f g} {φ₂ : f g} (h : φ₁ = φ₂) :
              φ₁.left = φ₂.left
              @[simp]
              theorem CategoryTheory.Arrow.hom.congr_right {T : Type u} [CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {g : CategoryTheory.Arrow T} {φ₁ : f g} {φ₂ : f g} (h : φ₁ = φ₂) :
              φ₁.right = φ₂.right
              @[simp]

              Given a square from an arrow i to an isomorphism p, express the source part of sq in terms of the inverse of p.

              Given a square from an isomorphism i to an arrow p, express the target part of sq in terms of the inverse of i.

              A helper construction: given a square between i and f ≫ g, produce a square between i and g, whose top leg uses f: A → X ↓f ↓i Y --> A → Y ↓g ↓i ↓g B → Z B → Z

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Arrow.leftFunc_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                ∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X Y), CategoryTheory.Arrow.leftFunc.map f = f.left

                The functor sending an arrow to its source.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Arrow.rightFunc_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  ∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X Y), CategoryTheory.Arrow.rightFunc.map f = f.right

                  The functor sending an arrow to its target.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Arrow.leftToRight_app {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) :
                    CategoryTheory.Arrow.leftToRight.app f = f.hom
                    def CategoryTheory.Arrow.leftToRight {C : Type u} [CategoryTheory.Category.{v, u} C] :
                    CategoryTheory.Arrow.leftFunc CategoryTheory.Arrow.rightFunc

                    The natural transformation from leftFunc to rightFunc, given by the arrow itself.

                    Equations
                    • CategoryTheory.Arrow.leftToRight = { app := fun (f : CategoryTheory.Arrow C) => f.hom, naturality := }
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Functor.mapArrow_map_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                      ∀ {X Y : CategoryTheory.Arrow C} (f : X Y), (F.mapArrow.map f).right = F.map f.right
                      @[simp]
                      theorem CategoryTheory.Functor.mapArrow_map_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                      ∀ {X Y : CategoryTheory.Arrow C} (f : X Y), (F.mapArrow.map f).left = F.map f.left

                      A functor C ⥤ D induces a functor between the corresponding arrow categories.

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

                        The functor (C ⥤ D) ⥤ (Arrow C ⥤ Arrow D) which sends a functor F : C ⥤ D to F.mapArrow.

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

                          The equivalence of categories Arrow C ≌ Arrow D induced by an equivalence C ≌ D.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            instance CategoryTheory.Functor.isEquivalence_mapArrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] :
                            F.mapArrow.IsEquivalence
                            Equations
                            • =

                            The images of f : Arrow C by two isomorphic functors F : C ⥤ D are isomorphic arrows in D.

                            Equations
                            Instances For