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.
@[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)
:
Auxiliary definition for TwoSquare.StructuredArrowRightwards.prodEquivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 ⋯
@[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 ⋯
@[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
@[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 ⋯) ⋯)
@[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)
:
@[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
@[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)
:
@[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))
@[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)
@[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)
:
@[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)
@[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
@[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)
:
@[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✝)
:
@[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
@[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₃)
:
@[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))
@[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₃)
:
@[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₃)
:
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