Documentation

Mathlib.CategoryTheory.GuitartExact.Opposite

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) :