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₂) : Functor (w.op.StructuredArrowRightwards g)ᵒᵖ (w.CostructuredArrowDownwards g.unop)

Auxiliary definition for structuredArrowRightwardsOpEquivalence.

@[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)ᵒᵖ) : ((functor w g).obj f).right.as = PUnit.unit

@[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)ᵒᵖ) : ((functor w g).obj f).left.hom = (Opposite.unop f).right.hom.unop

@[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') : ((functor w g).map φ).left.right = φ.unop.right.left.unop

@[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)ᵒᵖ) : ((functor w g).obj f).left.right = Opposite.unop (Opposite.unop f).right.left

@[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)ᵒᵖ) : ((functor w g).obj f).left.left.as = PUnit.unit

@[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)ᵒᵖ) : ((functor w g).obj f).hom.right = (Opposite.unop f).hom.left.unop

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₂) : Functor (w.CostructuredArrowDownwards g.unop) (w.op.StructuredArrowRightwards g)ᵒᵖ

Auxiliary definition for structuredArrowRightwardsOpEquivalence.

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₂) : (w.op.StructuredArrowRightwards g)ᵒᵖ ≌ w.CostructuredArrowDownwards g.unop

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.

@[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₂) : (w.structuredArrowRightwardsOpEquivalence g).functor = structuredArrowRightwardsOpEquivalence.functor w g

@[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₂) : (w.structuredArrowRightwardsOpEquivalence g).unitIso = Iso.refl (Functor.id (w.op.StructuredArrowRightwards g)ᵒᵖ)

@[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₂) : (w.structuredArrowRightwardsOpEquivalence g).inverse = structuredArrowRightwardsOpEquivalence.inverse w g

@[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₂) : (w.structuredArrowRightwardsOpEquivalence g).counitIso = Iso.refl ((structuredArrowRightwardsOpEquivalence.inverse w g).comp (structuredArrowRightwardsOpEquivalence.functor w g))

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] : w.op.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) : w.op.GuitartExact ↔ w.GuitartExact

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