Rejectivity and opposite categories

Passing to the opposite category interchanges left and right rejectivity. The only bookkeeping subtlety is that Mathlib's full subcategory on the opposite object property is canonically equivalent, rather than definitionally equal, to the opposite of the original full subcategory.

def QuotientSubmoduleEquidistribution.CategoricalRejective.RightRejectiveData.ofLeftOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (data : LeftRejectiveData P) : RightRejectiveData P.op

Opposite categories turn left-rejective data into right-rejective data.

theorem QuotientSubmoduleEquidistribution.CategoricalRejective.isRightRejective_op_of_isLeftRejective {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (h : IsLeftRejective P) : IsRightRejective P.op

A left-rejective full subcategory becomes right rejective after passing to the opposite category.

def QuotientSubmoduleEquidistribution.CategoricalRejective.LeftRejectiveData.ofRightOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (data : RightRejectiveData P) : LeftRejectiveData P.op

Opposite categories turn right-rejective data into left-rejective data.

theorem QuotientSubmoduleEquidistribution.CategoricalRejective.isLeftRejective_op_of_isRightRejective {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (h : IsRightRejective P) : IsLeftRejective P.op

A right-rejective full subcategory becomes left rejective after passing to the opposite category.