The opposite of a property of objects

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

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

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

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

@[simp]

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

@[simp]

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

instance CategoryTheory.ObjectProperty.instNonemptyOppositeOp {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty C) [P.Nonempty] : P.op.Nonempty

instance CategoryTheory.ObjectProperty.instNonemptyUnopOfOpposite {C : Type u} [CategoryStruct.{v, u} C] (P : ObjectProperty Cᵒᵖ) [P.Nonempty] : P.unop.Nonempty

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.ObjectProperty.op_ofObj {C : Type u} [CategoryStruct.{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} [CategoryStruct.{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} [CategoryStruct.{v, u} C] (X : C) : (singleton X).op = singleton (Opposite.op X)

@[simp]

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

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.opEquivalence {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ

Given P : ObjectProperty C, this is the equivalence between P.op.FullSubcategory and P.FullSubcategoryᵒᵖ.

@[simp]

theorem CategoryTheory.ObjectProperty.opEquivalence_inverse {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.opEquivalence.inverse = P.op.lift P.ι.op ⋯

@[simp]

theorem CategoryTheory.ObjectProperty.opEquivalence_functor {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.opEquivalence.functor = (P.lift P.op.ι.leftOp ⋯).rightOp

@[simp]

theorem CategoryTheory.ObjectProperty.opEquivalence_unitIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.opEquivalence.unitIso = Iso.refl (Functor.id P.op.FullSubcategory)

@[simp]

theorem CategoryTheory.ObjectProperty.opEquivalence_counitIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.opEquivalence.counitIso = Iso.refl ((P.op.lift P.ι.op ⋯).comp (P.lift P.op.ι.leftOp ⋯).rightOp)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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