Opposite categories #

We provide a category instance on Cᵒᵖ. The morphisms X ⟶ Y are defined to be the morphisms unop Y ⟶ unop X in C.

Here Cᵒᵖ is an irreducible typeclass synonym for C (it is the same one used in the algebra library).

We also provide various mechanisms for constructing opposite morphisms, functors, and natural transformations.

Unfortunately, because we do not have a definitional equality op (op X) = X, there are quite a few variations that are needed in practice.

source

theorem Quiver.Hom.op_inj {C : Type u₁} [Quiver C] {X : C} {Y : C} :

Function.Injective Quiver.Hom.op

source

theorem Quiver.Hom.unop_inj {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} :

Function.Injective Quiver.Hom.unop

source

@[simp]

theorem Quiver.Hom.unop_op {C : Type u₁} [Quiver C] {X : C} {Y : C} (f : X ⟶ Y) :

f.op.unop = f

source

@[simp]

theorem Quiver.Hom.unop_op' {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {x : Opposite.unop Y ⟶ Opposite.unop X} :

Quiver.Hom.unop (Opposite.op x) = x

source

@[simp]

theorem Quiver.Hom.op_unop {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) :

f.unop.op = f

source

@[simp]

theorem Quiver.Hom.unop_mk {C : Type u₁} [Quiver C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) :

Quiver.Hom.unop (Opposite.op f) = f

source

instance CategoryTheory.Category.opposite {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Category.{v₁, u₁} Cᵒᵖ

The opposite category.

See https://stacks.math.columbia.edu/tag/001M.

Equations

CategoryTheory.Category.opposite = CategoryTheory.Category.mk ⋯ ⋯ ⋯

source

theorem CategoryTheory.op_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z✝} {Z : Cᵒᵖ} (h : Opposite.op X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).op h = CategoryTheory.CategoryStruct.comp g.op (CategoryTheory.CategoryStruct.comp f.op h)

source

@[simp]

theorem CategoryTheory.op_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :

(CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op

source

@[simp]

theorem CategoryTheory.op_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :

(CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)

source

theorem CategoryTheory.unop_comp_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z✝} {Z : C} (h : Opposite.unop X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).unop h = CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.CategoryStruct.comp f.unop h)

source

@[simp]

theorem CategoryTheory.unop_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :

(CategoryTheory.CategoryStruct.comp f g).unop = CategoryTheory.CategoryStruct.comp g.unop f.unop

source

@[simp]

theorem CategoryTheory.unop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :

(CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop X)

source

@[simp]

theorem CategoryTheory.unop_id_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :

(CategoryTheory.CategoryStruct.id (Opposite.op X)).unop = CategoryTheory.CategoryStruct.id X

source

@[simp]

theorem CategoryTheory.op_id_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :

(CategoryTheory.CategoryStruct.id (Opposite.unop X)).op = CategoryTheory.CategoryStruct.id X

source

@[simp]

theorem CategoryTheory.unopUnop_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

∀ {X Y : Cᵒᵖᵒᵖ} (f : X ⟶ Y), (CategoryTheory.unopUnop C).map f = f.unop.unop

source

@[simp]

theorem CategoryTheory.unopUnop_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) :

(CategoryTheory.unopUnop C).obj X = Opposite.unop (Opposite.unop X)

source

def CategoryTheory.unopUnop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor Cᵒᵖᵒᵖ C

The functor from the double-opposite of a category to the underlying category.

Equations

CategoryTheory.unopUnop C = { obj := fun (X : Cᵒᵖᵒᵖ) => Opposite.unop (Opposite.unop X), map := fun {X Y : Cᵒᵖᵒᵖ} (f : X ⟶ Y) => f.unop.unop, map_id := ⋯, map_comp := ⋯ }

source

@[simp]

theorem CategoryTheory.opOp_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) :

(CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)

source

@[simp]

theorem CategoryTheory.opOp_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.opOp C).map f = f.op.op

source

def CategoryTheory.opOp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

CategoryTheory.Functor C Cᵒᵖᵒᵖ

The functor from a category to its double-opposite.

Equations

CategoryTheory.opOp C = { obj := fun (X : C) => Opposite.op (Opposite.op X), map := fun {X Y : C} (f : X ⟶ Y) => f.op.op, map_id := ⋯, map_comp := ⋯ }

source

@[simp]

theorem CategoryTheory.opOpEquivalence_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

(CategoryTheory.opOpEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.opOp C).comp (CategoryTheory.unopUnop C))

source

@[simp]

theorem CategoryTheory.opOpEquivalence_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

(CategoryTheory.opOpEquivalence C).functor = CategoryTheory.unopUnop C

source

@[simp]

theorem CategoryTheory.opOpEquivalence_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

(CategoryTheory.opOpEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ)

source

@[simp]

theorem CategoryTheory.opOpEquivalence_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

(CategoryTheory.opOpEquivalence C).inverse = CategoryTheory.opOp C

source

def CategoryTheory.opOpEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :

Cᵒᵖᵒᵖ ≌ C

The double opposite category is equivalent to the original.

Equations

One or more equations did not get rendered due to their size.

source

instance CategoryTheory.isIso_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

CategoryTheory.IsIso f.op

If f is an isomorphism, so is f.op

Equations

⋯ = ⋯

source

theorem CategoryTheory.isIso_of_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f.op] :

CategoryTheory.IsIso f

If f.op is an isomorphism f must be too. (This cannot be an instance as it would immediately loop!)

source

theorem CategoryTheory.isIso_op_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) :

CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f

source

theorem CategoryTheory.isIso_unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) :

CategoryTheory.IsIso f.unop ↔ CategoryTheory.IsIso f

source

instance CategoryTheory.isIso_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

CategoryTheory.IsIso f.unop

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.op_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

(CategoryTheory.inv f).op = CategoryTheory.inv f.op

source

@[simp]

theorem CategoryTheory.unop_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

(CategoryTheory.inv f).unop = CategoryTheory.inv f.unop

source

@[simp]

theorem CategoryTheory.Functor.op_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : Cᵒᵖ) :

F.op.obj X = Opposite.op (F.obj (Opposite.unop X))

source

@[simp]

theorem CategoryTheory.Functor.op_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), F.op.map f = (F.map f.unop).op

source

def CategoryTheory.Functor.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

CategoryTheory.Functor Cᵒᵖ Dᵒᵖ

The opposite of a functor, i.e. considering a functor F : C ⥤ D as a functor Cᵒᵖ ⥤ Dᵒᵖ. In informal mathematics no distinction is made between these.

Equations

F.op = { obj := fun (X : Cᵒᵖ) => Opposite.op (F.obj (Opposite.unop X)), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => (F.map f.unop).op, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.unop_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : C) :

F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))

source

@[simp]

theorem CategoryTheory.Functor.unop_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

∀ {X Y : C} (f : X ⟶ Y), F.unop.map f = (F.map f.op).unop

source

def CategoryTheory.Functor.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

CategoryTheory.Functor C D

Given a functor F : Cᵒᵖ ⥤ Dᵒᵖ we can take the "unopposite" functor F : C ⥤ D. In informal mathematics no distinction is made between these.

Equations

F.unop = { obj := fun (X : C) => Opposite.unop (F.obj (Opposite.op X)), map := fun {X Y : C} (f : X ⟶ Y) => (F.map f.op).unop, map_id := ⋯, map_comp := ⋯ }

source

@[simp]

theorem CategoryTheory.Functor.opUnopIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) :

F.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

@[simp]

theorem CategoryTheory.Functor.opUnopIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) :

F.opUnopIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

def CategoryTheory.Functor.opUnopIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

F.op.unop ≅ F

The isomorphism between F.op.unop and F.

Equations

F.opUnopIso = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.Iso.refl (F.op.unop.obj X)) ⋯

source

@[simp]

theorem CategoryTheory.Functor.unopOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) :

F.unopOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

@[simp]

theorem CategoryTheory.Functor.unopOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) :

F.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

def CategoryTheory.Functor.unopOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

F.unop.op ≅ F

The isomorphism between F.unop.op and F.

Equations

F.unopOpIso = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.Iso.refl (F.unop.op.obj X)) ⋯

source

@[simp]

theorem CategoryTheory.Functor.opHom_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : (CategoryTheory.Functor C D)ᵒᵖ) :

(CategoryTheory.Functor.opHom C D).obj F = (Opposite.unop F).op

source

@[simp]

theorem CategoryTheory.Functor.opHom_map_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :

∀ {X Y : (CategoryTheory.Functor C D)ᵒᵖ} (α : X ⟶ Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Functor.opHom C D).map α).app X_1 = (α.unop.app (Opposite.unop X_1)).op

source

def CategoryTheory.Functor.opHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :

CategoryTheory.Functor (CategoryTheory.Functor C D)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)

Taking the opposite of a functor is functorial.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Functor.opInv_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :

∀ {X Y : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X ⟶ Y), (CategoryTheory.Functor.opInv C D).map α = Quiver.Hom.op { app := fun (X_1 : C) => (α.app (Opposite.op X_1)).unop, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.Functor.opInv_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

(CategoryTheory.Functor.opInv C D).obj F = Opposite.op F.unop

source

def CategoryTheory.Functor.opInv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :

CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (CategoryTheory.Functor C D)ᵒᵖ

Take the "unopposite" of a functor is functorial.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Functor.leftOp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : Cᵒᵖ) :

F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))

source

@[simp]

theorem CategoryTheory.Functor.leftOp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), F.leftOp.map f = (F.map f.unop).unop

source

def CategoryTheory.Functor.leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :

CategoryTheory.Functor Cᵒᵖ D

Another variant of the opposite of functor, turning a functor C ⥤ Dᵒᵖ into a functor Cᵒᵖ ⥤ D. In informal mathematics no distinction is made.

Equations

F.leftOp = { obj := fun (X : Cᵒᵖ) => Opposite.unop (F.obj (Opposite.unop X)), map := fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => (F.map f.unop).unop, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.rightOp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : C) :

F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))

source

@[simp]

theorem CategoryTheory.Functor.rightOp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :

∀ {X Y : C} (f : X ⟶ Y), F.rightOp.map f = (F.map f.op).op

source

def CategoryTheory.Functor.rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :

CategoryTheory.Functor C Dᵒᵖ

Another variant of the opposite of functor, turning a functor Cᵒᵖ ⥤ D into a functor C ⥤ Dᵒᵖ. In informal mathematics no distinction is made.

Equations

F.rightOp = { obj := fun (X : C) => Opposite.op (F.obj (Opposite.op X)), map := fun {X Y : C} (f : X ⟶ Y) => (F.map f.op).op, map_id := ⋯, map_comp := ⋯ }

Instances For

source

theorem CategoryTheory.Functor.rightOp_map_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {X : C} {Y : C} (f : X ⟶ Y) :

(F.rightOp.map f).unop = F.map f.op

source

instance CategoryTheory.Functor.instFullOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Full] :

F.op.Full

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.instFaithfulOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [F.Faithful] :

F.op.Faithful

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.rightOp_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} [F.Faithful] :

F.rightOp.Faithful

If F is faithful then the right_op of F is also faithful.

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.leftOp_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} [F.Faithful] :

F.leftOp.Faithful

If F is faithful then the left_op of F is also faithful.

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.rightOp_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} [F.Full] :

F.rightOp.Full

Equations

⋯ = ⋯

source

instance CategoryTheory.Functor.leftOp_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} [F.Full] :

F.leftOp.Full

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) :

F.leftOpRightOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

@[simp]

theorem CategoryTheory.Functor.leftOpRightOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) :

F.leftOpRightOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

def CategoryTheory.Functor.leftOpRightOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) :

F.leftOp.rightOp ≅ F

The isomorphism between F.leftOp.rightOp and F.

Equations

F.leftOpRightOpIso = CategoryTheory.NatIso.ofComponents (fun (X : C) => CategoryTheory.Iso.refl (F.leftOp.rightOp.obj X)) ⋯

source

@[simp]

theorem CategoryTheory.Functor.rightOpLeftOpIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) :

F.rightOpLeftOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

@[simp]

theorem CategoryTheory.Functor.rightOpLeftOpIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) :

F.rightOpLeftOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

source

def CategoryTheory.Functor.rightOpLeftOpIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :

F.rightOp.leftOp ≅ F

The isomorphism between F.rightOp.leftOp and F.

Equations

F.rightOpLeftOpIso = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.Iso.refl (F.rightOp.leftOp.obj X)) ⋯

source

theorem CategoryTheory.Functor.rightOp_leftOp_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) :

F.rightOp.leftOp = F

Whenever possible, it is advisable to use the isomorphism rightOpLeftOpIso instead of this equality of functors.

source

@[simp]

theorem CategoryTheory.NatTrans.op_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) (X : Cᵒᵖ) :

(CategoryTheory.NatTrans.op α).app X = (α.app (Opposite.unop X)).op

source

def CategoryTheory.NatTrans.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) :

G.op ⟶ F.op

The opposite of a natural transformation.

Equations

CategoryTheory.NatTrans.op α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).op, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.op_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.op

source

@[simp]

theorem CategoryTheory.NatTrans.unop_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (X : C) :

(CategoryTheory.NatTrans.unop α).app X = (α.app (Opposite.op X)).unop

source

def CategoryTheory.NatTrans.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) :

G.unop ⟶ F.unop

The "unopposite" of a natural transformation.

Equations

CategoryTheory.NatTrans.unop α = { app := fun (X : C) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.unop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.unop

source

@[simp]

theorem CategoryTheory.NatTrans.removeOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ⟶ G.op) (X : C) :

(CategoryTheory.NatTrans.removeOp α).app X = (α.app (Opposite.op X)).unop

source

def CategoryTheory.NatTrans.removeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ⟶ G.op) :

G ⟶ F

Given a natural transformation α : F.op ⟶ G.op, we can take the "unopposite" of each component obtaining a natural transformation G ⟶ F.

Equations

CategoryTheory.NatTrans.removeOp α = { app := fun (X : C) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.removeOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :

CategoryTheory.NatTrans.removeOp (CategoryTheory.CategoryStruct.id F.op) = CategoryTheory.CategoryStruct.id F

source

@[simp]

theorem CategoryTheory.NatTrans.removeUnop_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F.unop ⟶ G.unop) (X : Cᵒᵖ) :

(CategoryTheory.NatTrans.removeUnop α).app X = (α.app (Opposite.unop X)).op

source

def CategoryTheory.NatTrans.removeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F.unop ⟶ G.unop) :

G ⟶ F

Given a natural transformation α : F.unop ⟶ G.unop, we can take the opposite of each component obtaining a natural transformation G ⟶ F.

Equations

CategoryTheory.NatTrans.removeUnop α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).op, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.removeUnop_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) :

CategoryTheory.NatTrans.removeUnop (CategoryTheory.CategoryStruct.id F.unop) = CategoryTheory.CategoryStruct.id F

source

@[simp]

theorem CategoryTheory.NatTrans.leftOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) :

(CategoryTheory.NatTrans.leftOp α).app X = (α.app (Opposite.unop X)).unop

source

def CategoryTheory.NatTrans.leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) :

G.leftOp ⟶ F.leftOp

Given a natural transformation α : F ⟶ G, for F G : C ⥤ Dᵒᵖ, taking unop of each component gives a natural transformation G.leftOp ⟶ F.leftOp.

Equations

CategoryTheory.NatTrans.leftOp α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).unop, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.leftOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} :

CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftOp

source

@[simp]

theorem CategoryTheory.NatTrans.leftOp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} {H : CategoryTheory.Functor C Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) :

CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp β) (CategoryTheory.NatTrans.leftOp α)

source

@[simp]

theorem CategoryTheory.NatTrans.removeLeftOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F.leftOp ⟶ G.leftOp) (X : C) :

(CategoryTheory.NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).op

source

def CategoryTheory.NatTrans.removeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (α : F.leftOp ⟶ G.leftOp) :

G ⟶ F

Given a natural transformation α : F.leftOp ⟶ G.leftOp, for F G : C ⥤ Dᵒᵖ, taking op of each component gives a natural transformation G ⟶ F.

Equations

CategoryTheory.NatTrans.removeLeftOp α = { app := fun (X : C) => (α.app (Opposite.op X)).op, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.removeLeftOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} :

CategoryTheory.NatTrans.removeLeftOp (CategoryTheory.CategoryStruct.id F.leftOp) = CategoryTheory.CategoryStruct.id F

source

@[simp]

theorem CategoryTheory.NatTrans.rightOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (X : C) :

(CategoryTheory.NatTrans.rightOp α).app X = (α.app (Opposite.op X)).op

source

def CategoryTheory.NatTrans.rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) :

G.rightOp ⟶ F.rightOp

Given a natural transformation α : F ⟶ G, for F G : Cᵒᵖ ⥤ D, taking op of each component gives a natural transformation G.rightOp ⟶ F.rightOp.

Equations

CategoryTheory.NatTrans.rightOp α = { app := fun (X : C) => (α.app (Opposite.op X)).op, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.rightOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} :

CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightOp

source

@[simp]

theorem CategoryTheory.NatTrans.rightOp_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} {H : CategoryTheory.Functor Cᵒᵖ D} (α : F ⟶ G) (β : G ⟶ H) :

CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp β) (CategoryTheory.NatTrans.rightOp α)

source

@[simp]

theorem CategoryTheory.NatTrans.removeRightOp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F.rightOp ⟶ G.rightOp) (X : Cᵒᵖ) :

(CategoryTheory.NatTrans.removeRightOp α).app X = (α.app (Opposite.unop X)).unop

source

def CategoryTheory.NatTrans.removeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (α : F.rightOp ⟶ G.rightOp) :

G ⟶ F

Given a natural transformation α : F.rightOp ⟶ G.rightOp, for F G : Cᵒᵖ ⥤ D, taking unop of each component gives a natural transformation G ⟶ F.

Equations

CategoryTheory.NatTrans.removeRightOp α = { app := fun (X : Cᵒᵖ) => (α.app (Opposite.unop X)).unop, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.NatTrans.removeRightOp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} :

CategoryTheory.NatTrans.removeRightOp (CategoryTheory.CategoryStruct.id F.rightOp) = CategoryTheory.CategoryStruct.id F

source

@[simp]

theorem CategoryTheory.Iso.op_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : X ≅ Y) :

α.op.inv = α.inv.op

source

@[simp]

theorem CategoryTheory.Iso.op_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : X ≅ Y) :

α.op.hom = α.hom.op

source

def CategoryTheory.Iso.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : X ≅ Y) :

Opposite.op Y ≅ Opposite.op X

The opposite isomorphism.

Equations

α.op = { hom := α.hom.op, inv := α.inv.op, hom_inv_id := ⋯, inv_hom_id := ⋯ }

source

@[simp]

theorem CategoryTheory.Iso.unop_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ≅ Y) :

f.unop.inv = f.inv.unop

source

@[simp]

theorem CategoryTheory.Iso.unop_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ≅ Y) :

f.unop.hom = f.hom.unop

source

def CategoryTheory.Iso.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ≅ Y) :

Opposite.unop Y ≅ Opposite.unop X

The isomorphism obtained from an isomorphism in the opposite category.

Equations

f.unop = { hom := f.hom.unop, inv := f.inv.unop, hom_inv_id := ⋯, inv_hom_id := ⋯ }

source

@[simp]

theorem CategoryTheory.Iso.unop_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ≅ Y) :

f.unop.op = f

source

@[simp]

theorem CategoryTheory.Iso.op_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ≅ Y) :

f.op.unop = f

source

@[simp]

theorem CategoryTheory.Iso.unop_hom_inv_id_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (G.obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (CategoryTheory.CategoryStruct.comp (e.inv.app X).unop h) = h

source

@[simp]

theorem CategoryTheory.Iso.unop_hom_inv_id_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) :

CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj X))

source

@[simp]

theorem CategoryTheory.Iso.unop_inv_hom_id_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) {Z : D} (h : Opposite.unop (F.obj X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (CategoryTheory.CategoryStruct.comp (e.hom.app X).unop h) = h

source

@[simp]

theorem CategoryTheory.Iso.unop_inv_hom_id_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C Dᵒᵖ} {G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) :

CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (F.obj X))

source

@[simp]

theorem CategoryTheory.NatIso.op_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) :

(CategoryTheory.NatIso.op α).inv = CategoryTheory.NatTrans.op α.inv

source

@[simp]

theorem CategoryTheory.NatIso.op_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) :

(CategoryTheory.NatIso.op α).hom = CategoryTheory.NatTrans.op α.hom

source

def CategoryTheory.NatIso.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) :

G.op ≅ F.op

The natural isomorphism between opposite functors G.op ≅ F.op induced by a natural isomorphism between the original functors F ≅ G.

Equations

CategoryTheory.NatIso.op α = { hom := CategoryTheory.NatTrans.op α.hom, inv := CategoryTheory.NatTrans.op α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

source

@[simp]

theorem CategoryTheory.NatIso.removeOp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) :

(CategoryTheory.NatIso.removeOp α).hom = CategoryTheory.NatTrans.removeOp α.hom

source

@[simp]

theorem CategoryTheory.NatIso.removeOp_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) :

(CategoryTheory.NatIso.removeOp α).inv = CategoryTheory.NatTrans.removeOp α.inv

source

def CategoryTheory.NatIso.removeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F.op ≅ G.op) :

G ≅ F

The natural isomorphism between functors G ≅ F induced by a natural isomorphism between the opposite functors F.op ≅ G.op.

Equations

CategoryTheory.NatIso.removeOp α = { hom := CategoryTheory.NatTrans.removeOp α.hom, inv := CategoryTheory.NatTrans.removeOp α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

source

@[simp]

theorem CategoryTheory.NatIso.unop_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) :

(CategoryTheory.NatIso.unop α).hom = CategoryTheory.NatTrans.unop α.hom

source

@[simp]

theorem CategoryTheory.NatIso.unop_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) :

(CategoryTheory.NatIso.unop α).inv = CategoryTheory.NatTrans.unop α.inv

source

def CategoryTheory.NatIso.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) :

G.unop ≅ F.unop

The natural isomorphism between functors G.unop ≅ F.unop induced by a natural isomorphism between the original functors F ≅ G.

Equations

CategoryTheory.NatIso.unop α = { hom := CategoryTheory.NatTrans.unop α.hom, inv := CategoryTheory.NatTrans.unop α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

source

@[simp]

theorem CategoryTheory.Equivalence.op_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm

source

@[simp]

theorem CategoryTheory.Equivalence.op_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

e.op.functor = e.functor.op

source

@[simp]

theorem CategoryTheory.Equivalence.op_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

e.op.inverse = e.inverse.op

source

@[simp]

theorem CategoryTheory.Equivalence.op_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm

source

def CategoryTheory.Equivalence.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) :

Cᵒᵖ ≌ Dᵒᵖ

An equivalence between categories gives an equivalence between the opposite categories.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Equivalence.unop_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :

e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm

source

@[simp]

theorem CategoryTheory.Equivalence.unop_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :

e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm

source

@[simp]

theorem CategoryTheory.Equivalence.unop_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :

e.unop.inverse = e.inverse.unop

source

@[simp]

theorem CategoryTheory.Equivalence.unop_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :

e.unop.functor = e.functor.unop

source

def CategoryTheory.Equivalence.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) :

C ≌ D

An equivalence between opposite categories gives an equivalence between the original categories.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.opEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A ⟶ B) :

(CategoryTheory.opEquiv A B) f = f.unop

source

@[simp]

theorem CategoryTheory.opEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : Opposite.unop B ⟶ Opposite.unop A) :

(CategoryTheory.opEquiv A B).symm g = g.op

source

def CategoryTheory.opEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) :

(A ⟶ B) ≃ (Opposite.unop B ⟶ Opposite.unop A)

The equivalence between arrows of the form A ⟶ B and B.unop ⟶ A.unop. Useful for building adjunctions. Note that this (definitionally) gives variants

def opEquiv' (A : C) (B : Cᵒᵖ) : (Opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
  opEquiv _ _

def opEquiv'' (A : Cᵒᵖ) (B : C) : (A ⟶ Opposite.op B) ≃ (B ⟶ A.unop) :=
  opEquiv _ _

def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
  opEquiv _ _

Equations

CategoryTheory.opEquiv A B = { toFun := fun (f : A ⟶ B) => f.unop, invFun := fun (g : Opposite.unop B ⟶ Opposite.unop A) => g.op, left_inv := ⋯, right_inv := ⋯ }

source

instance CategoryTheory.subsingleton_of_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) [Subsingleton (Opposite.unop B ⟶ Opposite.unop A)] :

Subsingleton (A ⟶ B)

Equations

⋯ = ⋯

source

instance CategoryTheory.decidableEqOfUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) [DecidableEq (Opposite.unop B ⟶ Opposite.unop A)] :

DecidableEq (A ⟶ B)

Equations

CategoryTheory.decidableEqOfUnop A B = (CategoryTheory.opEquiv A B).decidableEq

source

@[simp]

theorem CategoryTheory.isoOpEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (g : Opposite.unop B ≅ Opposite.unop A) :

(CategoryTheory.isoOpEquiv A B).symm g = g.op

source

@[simp]

theorem CategoryTheory.isoOpEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) (f : A ≅ B) :

(CategoryTheory.isoOpEquiv A B) f = f.unop

source

def CategoryTheory.isoOpEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (A : Cᵒᵖ) (B : Cᵒᵖ) :

(A ≅ B) ≃ (Opposite.unop B ≅ Opposite.unop A)

The equivalence between isomorphisms of the form A ≅ B and B.unop ≅ A.unop.

Note this is definitionally the same as the other three variants:

(Opposite.op A ≅ B) ≃ (B.unop ≅ A)
(A ≅ Opposite.op B) ≃ (B ≅ A.unop)
(Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)

Equations

CategoryTheory.isoOpEquiv A B = { toFun := fun (f : A ≅ B) => f.unop, invFun := fun (g : Opposite.unop B ≅ Opposite.unop A) => g.op, left_inv := ⋯, right_inv := ⋯ }