Theorems · Definition · category theory

CategoryTheory.TwoSquare.EquivalenceJ.functor

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                CategoryTheory.Functor (w.StructuredArrowRightwards g) (w.CostructuredArrowDownwards g)

Given w : TwoSquare T L R B and a morphism g : R.obj X₂ ⟶ B.obj X₃, this is the obvious functor w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g.

Defined in

Mathlib.CategoryTheory.GuitartExact.Basic

Cited by

4 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category