Morphism properties from object properties

Given two object properties P and Q, we introduce a morphism property ofObjectProperty P Q, given by all morphisms whose source satisfies P and target satisfies Q.

def CategoryTheory.MorphismProperty.ofObjectProperty {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) : MorphismProperty C

Given two object properties P and Q, the property of morphisms whose source satisfies P and target satisfies Q.

Equations

• CategoryTheory.MorphismProperty.ofObjectProperty P Q x✝ = (P X ∧ Q Y)

theorem CategoryTheory.MorphismProperty.ofObjectProperty_iff {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {X Y : C} (f : X ⟶ Y) : ofObjectProperty P Q f ↔ P X ∧ Q Y

theorem CategoryTheory.MorphismProperty.monotone_ofObjectProperty_left {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} (Q : ObjectProperty C) {P' : ObjectProperty C} (h : P ≤ P') : ofObjectProperty P Q ≤ ofObjectProperty P' Q

theorem CategoryTheory.MorphismProperty.monotone_ofObjectProperty_right {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {Q Q' : ObjectProperty C} (h : Q ≤ Q') : ofObjectProperty P Q ≤ ofObjectProperty P Q'

theorem CategoryTheory.MorphismProperty.ofObjectProperty_inverseImage {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor D C) : ofObjectProperty (P.inverseImage F) (Q.inverseImage F) = (ofObjectProperty P Q).inverseImage F

theorem CategoryTheory.MorphismProperty.ofObjectProperty_map_le {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : (ofObjectProperty P Q).map F ≤ ofObjectProperty (P.map F) (Q.map F)

instance CategoryTheory.MorphismProperty.instRespectsLeftOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : (ofObjectProperty P Q).RespectsLeft (isomorphisms C)

instance CategoryTheory.MorphismProperty.instRespectsRightOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) [Q.IsClosedUnderIsomorphisms] : (ofObjectProperty P Q).RespectsRight (isomorphisms C)