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.

source
@[implicit_reducible]
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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
    source
    @[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 (StructuredArrow.right (Opposite.unop f)).left
    source
    @[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 = (StructuredArrow.right (Opposite.unop f)).hom.unop
    source
    @[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 = (CostructuredArrow.Hom.left (StructuredArrow.Hom.right φ.unop)).unop
    source
    @[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
    source
    @[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 = (CostructuredArrow.Hom.left (StructuredArrow.hom (Opposite.unop f))).unop
    source
    @[implicit_reducible]
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse_obj {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.CostructuredArrowDownwards g.unop) :
      (inverse w g).obj f = Opposite.op (StructuredArrowRightwards.mk w.op g (Opposite.op (CostructuredArrow.left f).right) (StructuredArrow.Hom.right (CostructuredArrow.hom f)).op (CostructuredArrow.left f).hom.op ⋯)
      source
      @[simp]
      theorem CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse_map {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.CostructuredArrowDownwards g.unop} (φ : f ⟶ f') :
      (inverse w g).map φ = (StructuredArrow.homMk (CostructuredArrow.homMk (StructuredArrow.Hom.right (CostructuredArrow.Hom.left φ)).op ⋯) ⋯).op
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[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)ᵒᵖ)
        source
        @[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
        source
        @[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))
        source
        @[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
        source
        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
        source
        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
        source
        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
        source
        instance CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso' {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) [T.IsEquivalence] [B.IsEquivalence] [IsIso w] :
        w.GuitartExact