The opposite of a property of objects

def CategoryTheory.ObjectProperty.op {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ObjectProperty Cᵒᵖ

The property of objects of Cᵒᵖ corresponding to P : ObjectProperty C.

Equations

• P.op X = P (Opposite.unop X)

def CategoryTheory.ObjectProperty.unop {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) : ObjectProperty C

The property of objects of C corresponding to P : ObjectProperty Cᵒᵖ.

Equations

• P.unop X = P (Opposite.op X)

@[simp]

theorem CategoryTheory.ObjectProperty.op_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : Cᵒᵖ) : P.op X ↔ P (Opposite.unop X)

@[simp]

theorem CategoryTheory.ObjectProperty.unop_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) (X : C) : P.unop X ↔ P (Opposite.op X)

@[simp]

theorem CategoryTheory.ObjectProperty.op_unop {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) : P.unop.op = P

@[simp]

theorem CategoryTheory.ObjectProperty.unop_op {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.op.unop = P

theorem CategoryTheory.ObjectProperty.op_injective {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P.op = Q.op) : P = Q

theorem CategoryTheory.ObjectProperty.unop_injective {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty Cᵒᵖ} (h : P.unop = Q.unop) : P = Q

theorem CategoryTheory.ObjectProperty.op_injective_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} : P.op = Q.op ↔ P = Q

theorem CategoryTheory.ObjectProperty.unop_injective_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty Cᵒᵖ} : P.unop = Q.unop ↔ P = Q

theorem CategoryTheory.ObjectProperty.op_monotone {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.op ≤ Q.op

theorem CategoryTheory.ObjectProperty.unop_monotone {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty Cᵒᵖ} (h : P ≤ Q) : P.unop ≤ Q.unop

@[simp]

theorem CategoryTheory.ObjectProperty.op_monotone_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} : P.op ≤ Q.op ↔ P ≤ Q

@[simp]

theorem CategoryTheory.ObjectProperty.unop_monotone_iff {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty Cᵒᵖ} : P.unop ≤ Q.unop ↔ P ≤ Q

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsOppositeOp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.op.IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsUnopOfOpposite {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] : P.unop.IsClosedUnderIsomorphisms

theorem CategoryTheory.ObjectProperty.op_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.isoClosure.op = P.op.isoClosure

theorem CategoryTheory.ObjectProperty.unop_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure

def CategoryTheory.ObjectProperty.subtypeOpEquiv {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Subtype P.op ≃ Subtype P

The bijection Subtype P.op ≃ Subtype P for P : ObjectProperty C.

Equations

• P.subtypeOpEquiv = { toFun := fun (x : Subtype P.op) => ⟨Opposite.unop ↑x, ⋯⟩, invFun := fun (x : Subtype P) => ⟨Opposite.op ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.ObjectProperty.op_ofObj {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ι → C) : (ofObj X).op = ofObj fun (i : ι) => Opposite.op (X i)

@[simp]

theorem CategoryTheory.ObjectProperty.unop_ofObj {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ι → Cᵒᵖ) : (ofObj X).unop = ofObj fun (i : ι) => Opposite.unop (X i)

@[simp]

theorem CategoryTheory.ObjectProperty.op_singleton {C : Type u} [Category.{v, u} C] (X : C) : (singleton X).op = singleton (Opposite.op X)

@[simp]

theorem CategoryTheory.ObjectProperty.unop_singleton {C : Type u} [Category.{v, u} C] (X : Cᵒᵖ) : (singleton X).unop = singleton (Opposite.unop X)