The opposite of a Guitart exact square #
A 2
-square is Guitart exact iff the opposite (transposed) 2
-square
is Guitart exact.
def
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
Auxiliary definition for structuredArrowRightwardsOpEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_right_as
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
(f : (w.op.StructuredArrowRightwards g)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_right
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
(f : (w.op.StructuredArrowRightwards g)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
(f : (w.op.StructuredArrowRightwards g)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_map_left_right
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
{f f' : (w.op.StructuredArrowRightwards g)ᵒᵖ}
(φ : f ⟶ f')
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_hom_right
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
(f : (w.op.StructuredArrowRightwards g)ᵒᵖ)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor_obj_left_hom
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
(f : (w.op.StructuredArrowRightwards g)ᵒᵖ)
:
def
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
Auxiliary definition for structuredArrowRightwardsOpEquivalence
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
If w : TwoSquare T L R B
, and g : B.op.obj X₃ ⟶ R.op.obj X₂
, this is
the obvious equivalence of categories between
(w.op.StructuredArrowRightwards g)ᵒᵖ
and w.CostructuredArrowDownwards g.unop
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_inverse
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_functor
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
@[simp]
theorem
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_counitIso
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
{X₃ : C₃ᵒᵖ}
{X₂ : C₂ᵒᵖ}
(g : B.op.obj X₃ ⟶ R.op.obj X₂)
:
instance
CategoryTheory.TwoSquare.instGuitartExactOppositeOp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[w.GuitartExact]
:
theorem
CategoryTheory.TwoSquare.guitartExact_op_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
:
instance
CategoryTheory.TwoSquare.guitartExact_id'
{C₁ : Type u₁}
{C₂ : Type u₂}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
(F : Functor C₁ C₂)
:
(mk F (Functor.id C₁) (Functor.id C₂) F (CategoryStruct.id F)).GuitartExact