mathlib docs: category_theory.opposites

@[instance]

def category_theory.has_hom.opposite {C : Type u₁} [category_theory.has_hom C] :

The hom types of the opposite of a category (or graph).

As with the objects, we'll make this irreducible below. Use f.op and f.unop to convert between morphisms of C and morphisms of Cᵒᵖ.

Equations

category_theory.has_hom.opposite = {hom := λ (X Y : Cᵒᵖ), opposite.unop Y ⟶ opposite.unop X}

source

def category_theory.has_hom.hom.op {C : Type u₁} [category_theory.has_hom C] {X Y : C} (f : X ⟶ Y) :

opposite.op Y ⟶ opposite.op X

Equations

f.op = f

source

def category_theory.has_hom.hom.unop {C : Type u₁} [category_theory.has_hom C] {X Y : Cᵒᵖ} (f : X ⟶ Y) :

opposite.unop Y ⟶ opposite.unop X

Equations

f.unop = f

source

theorem category_theory.has_hom.hom.op_inj {C : Type u₁} [category_theory.has_hom C] {X Y : C} :

function.injective category_theory.has_hom.hom.op

source

theorem category_theory.has_hom.hom.unop_inj {C : Type u₁} [category_theory.has_hom C] {X Y : Cᵒᵖ} :

function.injective category_theory.has_hom.hom.unop

source

@[simp]

theorem category_theory.has_hom.hom.unop_op {C : Type u₁} [category_theory.has_hom C] {X Y : C} {f : X ⟶ Y} :

f.op.unop = f

source

@[simp]

theorem category_theory.has_hom.hom.op_unop {C : Type u₁} [category_theory.has_hom C] {X Y : Cᵒᵖ} {f : X ⟶ Y} :

f.unop.op = f

source

@[instance]

def category_theory.category.opposite {C : Type u₁} [category_theory.category C] :

category_theory.category Cᵒᵖ

The opposite category.

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

Equations

category_theory.category.opposite = {to_category_struct := {to_has_hom := category_theory.has_hom.opposite category_theory.category_struct.to_has_hom, id := λ (X : Cᵒᵖ), (𝟙 (opposite.unop X)).op, comp := λ (_x _x_1 _x_2 : Cᵒᵖ) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), (g.unop ≫ f.unop).op}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.op_comp {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :

(f ≫ g).op = g.op ≫ f.op

source

@[simp]

theorem category_theory.op_id {C : Type u₁} [category_theory.category C] {X : C} :

(𝟙 X).op = 𝟙 (opposite.op X)

source

@[simp]

theorem category_theory.unop_comp {C : Type u₁} [category_theory.category C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} :

(f ≫ g).unop = g.unop ≫ f.unop

source

@[simp]

theorem category_theory.unop_id {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} :

(𝟙 X).unop = 𝟙 (opposite.unop X)

source

@[simp]

theorem category_theory.unop_id_op {C : Type u₁} [category_theory.category C] {X : C} :

(𝟙 (opposite.op X)).unop = 𝟙 X

source

@[simp]

theorem category_theory.op_id_unop {C : Type u₁} [category_theory.category C] {X : Cᵒᵖ} :

(𝟙 (opposite.unop X)).op = 𝟙 X

source

def category_theory.op_op {C : Type u₁} [category_theory.category C] :

Cᵒᵖ ᵒᵖ ⥤ C

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

Equations

category_theory.op_op = {obj := λ (X : Cᵒᵖ ᵒᵖ), opposite.unop (opposite.unop X), map := λ (X Y : Cᵒᵖ ᵒᵖ) (f : X ⟶ Y), f.unop.unop, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.op_op_obj {C : Type u₁} [category_theory.category C] (X : Cᵒᵖ ᵒᵖ) :

category_theory.op_op.obj X = opposite.unop (opposite.unop X)

source

@[simp]

theorem category_theory.op_op_map {C : Type u₁} [category_theory.category C] (X Y : Cᵒᵖ ᵒᵖ) (f : X ⟶ Y) :

category_theory.op_op.map f = f.unop.unop

source

@[simp]

theorem category_theory.unop_unop_obj {C : Type u₁} [category_theory.category C] (X : C) :

category_theory.unop_unop.obj X = opposite.op (opposite.op X)

source

@[simp]

theorem category_theory.unop_unop_map {C : Type u₁} [category_theory.category C] (X Y : C) (f : X ⟶ Y) :

category_theory.unop_unop.map f = f.op.op

source

def category_theory.unop_unop {C : Type u₁} [category_theory.category C] :

C ⥤ Cᵒᵖ ᵒᵖ

The functor from a category to its double-opposite.

Equations

category_theory.unop_unop = {obj := λ (X : C), opposite.op (opposite.op X), map := λ (X Y : C) (f : X ⟶ Y), f.op.op, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.op_op_equivalence_counit_iso {C : Type u₁} [category_theory.category C] :

category_theory.op_op_equivalence.counit_iso = category_theory.iso.refl (category_theory.unop_unop ⋙ category_theory.op_op)

source

@[simp]

theorem category_theory.op_op_equivalence_functor {C : Type u₁} [category_theory.category C] :

category_theory.op_op_equivalence.functor = category_theory.op_op

source

def category_theory.op_op_equivalence {C : Type u₁} [category_theory.category C] :

Cᵒᵖ ᵒᵖ ≌ C

The double opposite category is equivalent to the original.

Equations

category_theory.op_op_equivalence = {functor := category_theory.op_op _inst_1, inverse := category_theory.unop_unop _inst_1, unit_iso := category_theory.iso.refl (𝟭 Cᵒᵖ ᵒᵖ), counit_iso := category_theory.iso.refl (category_theory.unop_unop ⋙ category_theory.op_op), functor_unit_iso_comp' := _}

source

@[simp]

theorem category_theory.op_op_equivalence_inverse {C : Type u₁} [category_theory.category C] :

category_theory.op_op_equivalence.inverse = category_theory.unop_unop

source

@[simp]

theorem category_theory.op_op_equivalence_unit_iso {C : Type u₁} [category_theory.category C] :

category_theory.op_op_equivalence.unit_iso = category_theory.iso.refl (𝟭 Cᵒᵖ ᵒᵖ)

source

def category_theory.is_iso_of_op {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso f.op] :

category_theory.is_iso f

Equations

category_theory.is_iso_of_op f = {inv := (category_theory.is_iso.inv f.op).unop, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.functor.op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X Y : Cᵒᵖ) (f : X ⟶ Y) :

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

source

def category_theory.functor.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Cᵒᵖ ⥤ Dᵒᵖ

Equations

F.op = {obj := λ (X : Cᵒᵖ), opposite.op (F.obj (opposite.unop X)), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), (F.map f.unop).op, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (X : Cᵒᵖ) :

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

source

def category_theory.functor.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :

C ⥤ D

Equations

F.unop = {obj := λ (X : C), opposite.unop (F.obj (opposite.op X)), map := λ (X Y : C) (f : X ⟶ Y), (F.map f.op).unop, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.unop_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X Y : C) (f : X ⟶ Y) :

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

source

@[simp]

theorem category_theory.functor.unop_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) (X : C) :

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

source

def category_theory.functor.op_unop_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

F.op.unop ≅ F

The isomorphism between F.op.unop and F.

Equations

F.op_unop_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl (F.op.unop.obj X)) _

source

def category_theory.functor.unop_op_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :

F.unop.op ≅ F

The isomorphism between F.unop.op and F.

Equations

F.unop_op_iso = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.iso.refl (F.unop.op.obj X)) _

source

def category_theory.functor.op_hom (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

(C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ

Equations

category_theory.functor.op_hom C D = {obj := λ (F : (C ⥤ D)ᵒᵖ), (opposite.unop F).op, map := λ (F G : (C ⥤ D)ᵒᵖ) (α : F ⟶ G), {app := λ (X : Cᵒᵖ), (α.unop.app (opposite.unop X)).op, naturality' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.op_hom_map_app (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : (C ⥤ D)ᵒᵖ) (α : F ⟶ G) (X : Cᵒᵖ) :

((category_theory.functor.op_hom C D).map α).app X = (α.unop.app (opposite.unop X)).op

source

@[simp]

theorem category_theory.functor.op_hom_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : (C ⥤ D)ᵒᵖ) :

(category_theory.functor.op_hom C D).obj F = (opposite.unop F).op

source

@[simp]

theorem category_theory.functor.op_inv_map (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F G : Cᵒᵖ ⥤ Dᵒᵖ) (α : F ⟶ G) :

(category_theory.functor.op_inv C D).map α = category_theory.has_hom.hom.op {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}

source

@[simp]

theorem category_theory.functor.op_inv_obj (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] (F : Cᵒᵖ ⥤ Dᵒᵖ) :

(category_theory.functor.op_inv C D).obj F = opposite.op F.unop

source

def category_theory.functor.op_inv (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :

(Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ

Equations

category_theory.functor.op_inv C D = {obj := λ (F : Cᵒᵖ ⥤ Dᵒᵖ), opposite.op F.unop, map := λ (F G : Cᵒᵖ ⥤ Dᵒᵖ) (α : F ⟶ G), category_theory.has_hom.hom.op {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.left_op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X Y : Cᵒᵖ) (f : X ⟶ Y) :

F.left_op.map f = (F.map f.unop).unop

source

def category_theory.functor.left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) :

Cᵒᵖ ⥤ D

Equations

F.left_op = {obj := λ (X : Cᵒᵖ), opposite.unop (F.obj (opposite.unop X)), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), (F.map f.unop).unop, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.left_op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ Dᵒᵖ) (X : Cᵒᵖ) :

F.left_op.obj X = opposite.unop (F.obj (opposite.unop X))

source

def category_theory.functor.right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) :

C ⥤ Dᵒᵖ

Equations

F.right_op = {obj := λ (X : C), opposite.op (F.obj (opposite.op X)), map := λ (X Y : C) (f : X ⟶ Y), (F.map f.op).op, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.functor.right_op_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X Y : C) (f : X ⟶ Y) :

F.right_op.map f = (F.map f.op).op

source

@[simp]

theorem category_theory.functor.right_op_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : Cᵒᵖ ⥤ D) (X : C) :

F.right_op.obj X = opposite.op (F.obj (opposite.op X))

source

@[instance]

def category_theory.functor.category_theory.full {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [category_theory.full F] :

category_theory.full F.op

Equations

category_theory.functor.category_theory.full = {preimage := λ (X Y : Cᵒᵖ) (f : F.op.obj X ⟶ F.op.obj Y), (F.preimage f.unop).op, witness' := _}

source

@[instance]

def category_theory.functor.category_theory.faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [category_theory.faithful F] :

category_theory.faithful F.op

source

@[instance]

def category_theory.functor.right_op_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : Cᵒᵖ ⥤ D} [category_theory.faithful F] :

category_theory.faithful F.right_op

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

source

@[instance]

def category_theory.functor.left_op_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ Dᵒᵖ} [category_theory.faithful F] :

category_theory.faithful F.left_op

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

source

@[simp]

theorem category_theory.nat_trans.op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) (X : Cᵒᵖ) :

(category_theory.nat_trans.op α).app X = (α.app (opposite.unop X)).op

source

def category_theory.nat_trans.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) :

G.op ⟶ F.op

Equations

category_theory.nat_trans.op α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).op, naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.op_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

category_theory.nat_trans.op (𝟙 F) = 𝟙 F.op

source

def category_theory.nat_trans.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ⟶ G.op) :

G ⟶ F

Equations

category_theory.nat_trans.unop α = {app := λ (X : C), (α.app (opposite.op X)).unop, naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.unop_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ⟶ G.op) (X : C) :

(category_theory.nat_trans.unop α).app X = (α.app (opposite.op X)).unop

source

@[simp]

theorem category_theory.nat_trans.unop_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

category_theory.nat_trans.unop (𝟙 F.op) = 𝟙 F

source

def category_theory.nat_trans.left_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F ⟶ G) :

G.left_op ⟶ F.left_op

Equations

category_theory.nat_trans.left_op α = {app := λ (X : Cᵒᵖ), (α.app (opposite.unop X)).unop, naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.left_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F ⟶ G) (X : Cᵒᵖ) :

(category_theory.nat_trans.left_op α).app X = (α.app (opposite.unop X)).unop

source

def category_theory.nat_trans.right_op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F.left_op ⟶ G.left_op) :

G ⟶ F

Equations

category_theory.nat_trans.right_op α = {app := λ (X : C), (α.app (opposite.op X)).op, naturality' := _}

source

@[simp]

theorem category_theory.nat_trans.right_op_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ Dᵒᵖ} (α : F.left_op ⟶ G.left_op) (X : C) :

(category_theory.nat_trans.right_op α).app X = (α.app (opposite.op X)).op

source

def category_theory.iso.op {C : Type u₁} [category_theory.category C] {X Y : C} (α : X ≅ Y) :

opposite.op Y ≅ opposite.op X

Equations

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

source

@[simp]

theorem category_theory.iso.op_hom {C : Type u₁} [category_theory.category C] {X Y : C} {α : X ≅ Y} :

α.op.hom = α.hom.op

source

@[simp]

theorem category_theory.iso.op_inv {C : Type u₁} [category_theory.category C] {X Y : C} {α : X ≅ Y} :

α.op.inv = α.inv.op

source

def category_theory.nat_iso.op {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : 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

category_theory.nat_iso.op α = {hom := category_theory.nat_trans.op α.hom, inv := category_theory.nat_trans.op α.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.nat_iso.op_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) :

(category_theory.nat_iso.op α).hom = category_theory.nat_trans.op α.hom

source

@[simp]

theorem category_theory.nat_iso.op_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F ≅ G) :

(category_theory.nat_iso.op α).inv = category_theory.nat_trans.op α.inv

source

def category_theory.nat_iso.unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : 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

category_theory.nat_iso.unop α = {hom := category_theory.nat_trans.unop α.hom, inv := category_theory.nat_trans.unop α.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.nat_iso.unop_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ≅ G.op) :

(category_theory.nat_iso.unop α).hom = category_theory.nat_trans.unop α.hom

source

@[simp]

theorem category_theory.nat_iso.unop_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ D} (α : F.op ≅ G.op) :

(category_theory.nat_iso.unop α).inv = category_theory.nat_trans.unop α.inv

source

def category_theory.op_equiv {C : Type u₁} [category_theory.category C] (A 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 op_equiv' (A : C) (B : Cᵒᵖ) : (opposite.op A ⟶ B) ≃ (B.unop ⟶ A) :=
op_equiv _ _

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

def op_equiv''' (A B : C) : (opposite.op A ⟶ opposite.op B) ≃ (B ⟶ A) :=
op_equiv _ _

Equations

category_theory.op_equiv A B = {to_fun := λ (f : A ⟶ B), f.unop, inv_fun := λ (g : opposite.unop B ⟶ opposite.unop A), g.op, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.op_equiv_apply {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) (f : A ⟶ B) :

⇑(category_theory.op_equiv A B) f = f.unop

source

@[simp]

theorem category_theory.op_equiv_symm_apply {C : Type u₁} [category_theory.category C] (A B : Cᵒᵖ) (f : opposite.unop B ⟶ opposite.unop A) :

⇑((category_theory.op_equiv A B).symm) f = f.op

source

def category_theory.op_hom_of_le {α : Type v} [preorder α] {U V : αᵒᵖ} (h : opposite.unop V ≤ opposite.unop U) :

U ⟶ V

Construct a morphism in the opposite of a preorder category from an inequality.

Equations

category_theory.op_hom_of_le h = (category_theory.hom_of_le h).op

source

theorem category_theory.le_of_op_hom {α : Type v} [preorder α] {U V : αᵒᵖ} (h : U ⟶ V) :

opposite.unop V ≤ opposite.unop U