Documentation

Mathlib.CategoryTheory.GuitartExact.Prod

External products of Guitart exact squares #

In this file, we show that the external product of two Guitart exact squares is a Guitart exact square.

source
@[implicit_reducible]
def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : (w.prod w').StructuredArrowRightwards g) :
w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2

Auxiliary definition for TwoSquare.StructuredArrowRightwards.prodEquivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functorObj_fst {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : (w.prod w').StructuredArrowRightwards g) :
    (functorObj w w' g X).1 = mk w g.1 ((Comma.mapLeft (Functor.fromPUnit ((B.prod B').obj Y₃)) (w.prod w')).obj ((CostructuredArrow.post (L.prod L') (B.prod B') Y₃).obj (StructuredArrow.right X))).left.1 (CostructuredArrow.Hom.left (StructuredArrow.hom X)).1 (StructuredArrow.right X).hom.1 ⋯
    source
    @[simp]
    theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functorObj_snd {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : (w.prod w').StructuredArrowRightwards g) :
    (functorObj w w' g X).2 = mk w' g.2 ((Comma.mapLeft (Functor.fromPUnit ((B.prod B').obj Y₃)) (w.prod w')).obj ((CostructuredArrow.post (L.prod L') (B.prod B') Y₃).obj (StructuredArrow.right X))).left.2 (CostructuredArrow.Hom.left (StructuredArrow.hom X)).2 (StructuredArrow.right X).hom.2 ⋯
    source
    @[implicit_reducible]
    def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
    Functor ((w.prod w').StructuredArrowRightwards g) (w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2)

    Auxiliary definition for TwoSquare.StructuredArrowRightwards.prodEquivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functor_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) {X✝ Y✝ : (w.prod w').StructuredArrowRightwards g} (f : X✝ ⟶ Y✝) :
      (functor w w' g).map f = Prod.mkHom (StructuredArrow.homMk (CostructuredArrow.homMk (CostructuredArrow.Hom.left (StructuredArrow.Hom.right f)).1 ⋯) ⋯) (StructuredArrow.homMk (CostructuredArrow.homMk (CostructuredArrow.Hom.left (StructuredArrow.Hom.right f)).2 ⋯) ⋯)
      source
      @[simp]
      theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functor_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : (w.prod w').StructuredArrowRightwards g) :
      (functor w w' g).obj X = functorObj w w' g X
      source
      @[implicit_reducible]
      def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
      (w.prod w').StructuredArrowRightwards g

      Auxiliary definition for TwoSquare.StructuredArrowRightwards.prodEquivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj_left_as {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
        (inverseObj w w' g X).left.as = PUnit.unit
        source
        @[simp]
        theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj_hom_left {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
        (inverseObj w w' g X).hom.left = (CostructuredArrow.Hom.left (StructuredArrow.hom X.1), CostructuredArrow.Hom.left (StructuredArrow.hom X.2))
        source
        @[simp]
        theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj_right_left {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
        (inverseObj w w' g X).right.left = ((StructuredArrow.right X.1).left, (StructuredArrow.right X.2).left)
        source
        @[simp]
        theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj_right_right_as {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
        (inverseObj w w' g X).right.right.as = PUnit.unit
        source
        @[simp]
        theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverseObj_right_hom {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
        (inverseObj w w' g X).right.hom = ((StructuredArrow.right X.1).hom, (StructuredArrow.right X.2).hom)
        source
        @[implicit_reducible]
        def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverse {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
        Functor (w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) ((w.prod w').StructuredArrowRightwards g)

        Auxiliary definition for TwoSquare.StructuredArrowRightwards.prodEquivalence.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverse_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) (X : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2) :
          (inverse w w' g).obj X = inverseObj w w' g X
          source
          @[simp]
          theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.inverse_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) {X✝ Y✝ : w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2} (f : X✝ ⟶ Y✝) :
          (inverse w w' g).map f = StructuredArrow.homMk (CostructuredArrow.homMk (CostructuredArrow.Hom.left (StructuredArrow.Hom.right f.1), CostructuredArrow.Hom.left (StructuredArrow.Hom.right f.2)) ⋯) ⋯
          source
          @[implicit_reducible]
          def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
          (w.prod w').StructuredArrowRightwards g ≌ w.StructuredArrowRightwards g.1 × w'.StructuredArrowRightwards g.2

          If w and w' are two 2-squares of functors, then the categories StructuredArrowRightwards (w.prod w') g decomposes as a product of two StructuredArrowRightwards for w and w'.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence_inverse {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
            (prodEquivalence w w' g).inverse = prodEquivalence.inverse w w' g
            source
            @[simp]
            theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence_counitIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
            (prodEquivalence w w' g).counitIso = Iso.refl ((prodEquivalence.inverse w w' g).comp (prodEquivalence.functor w w' g))
            source
            @[simp]
            theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence_unitIso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
            (prodEquivalence w w' g).unitIso = Iso.refl (Functor.id ((w.prod w').StructuredArrowRightwards g))
            source
            @[simp]
            theorem CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence_functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') {Y₂ : C₂ × D₂} {Y₃ : C₃ × D₃} (g : (R.prod R').obj Y₂ ⟶ (B.prod B').obj Y₃) :
            (prodEquivalence w w' g).functor = prodEquivalence.functor w w' g
            source
            instance CategoryTheory.TwoSquare.GuitartExact.prod {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {D₁ : Type u_5} {D₂ : Type u_6} {D₃ : Type u_7} {D₄ : Type u_8} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} C₄] [Category.{v_5, u_5} D₁] [Category.{v_6, u_6} D₂] [Category.{v_7, u_7} D₃] [Category.{v_8, u_8} D₄] {T : Functor C₁ C₂} {L : Functor C₁ C₃} {R : Functor C₂ C₄} {B : Functor C₃ C₄} {T' : Functor D₁ D₂} {L' : Functor D₁ D₃} {R' : Functor D₂ D₄} {B' : Functor D₃ D₄} (w : TwoSquare T L R B) (w' : TwoSquare T' L' R' B') [w.GuitartExact] [w'.GuitartExact] :
            (w.prod w').GuitartExact