Documentation

Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom

Object properties transported along morphisms #

In this file we define the predicates InheritedFromSource and InheritedFromTarget for an object property P along a morphism property Q. P is inherited from the source (resp. target) along Q if for every morphism f : X ⟶ Y with Q f, P X implies P Y (resp. P Y implies P X).

source
class CategoryTheory.ObjectProperty.InheritedFromSource {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) :
Prop

A property of objects P is inherited from the source of morphisms satisfying Q if whenever P holds for X and f : X ⟶ Y is a Q-morphism, then P holds for Y.

  • of_hom_of_source {X Y : C} (f : X ⟶ Y) (hf : Q f) : P X → P Y
Instances
    source
    class CategoryTheory.ObjectProperty.InheritedFromTarget {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) :
    Prop

    A property of objects P is inherited from the target of morphisms satisfying Q if whenever P holds for Y and f : X ⟶ Y is a Q-morphism, then P holds for X.

    • of_hom_of_target {X Y : C} (f : X ⟶ Y) (hf : Q f) : P Y → P X
    Instances
      source
      instance CategoryTheory.ObjectProperty.InheritedFromSource.instIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
      P.InheritedFromSource (MorphismProperty.isomorphisms C)
      source
      instance CategoryTheory.ObjectProperty.InheritedFromSource.op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromSource Q] :
      P.op.InheritedFromTarget Q.op
      source
      instance CategoryTheory.ObjectProperty.InheritedFromSource.instMin {C : Type u_1} [Category.{u_2, u_1} C] (P P' : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromSource Q] [P'.InheritedFromSource Q] :
      (P ⊓ P').InheritedFromSource Q
      source
      theorem CategoryTheory.ObjectProperty.InheritedFromSource.of_le {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q Q' : MorphismProperty C) (hQ : Q ≤ Q') [P.InheritedFromSource Q'] :
      P.InheritedFromSource Q
      source
      instance CategoryTheory.ObjectProperty.InheritedFromTarget.instIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
      P.InheritedFromTarget (MorphismProperty.isomorphisms C)
      source
      instance CategoryTheory.ObjectProperty.InheritedFromTarget.op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromTarget Q] :
      P.op.InheritedFromSource Q.op
      source
      instance CategoryTheory.ObjectProperty.InheritedFromTarget.instMin {C : Type u_1} [Category.{u_2, u_1} C] (P P' : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromTarget Q] [P'.InheritedFromTarget Q] :
      (P ⊓ P').InheritedFromTarget Q
      source
      theorem CategoryTheory.ObjectProperty.InheritedFromTarget.of_le {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q Q' : MorphismProperty C) (hQ : Q ≤ Q') [P.InheritedFromTarget Q'] :
      P.InheritedFromTarget Q
      source
      theorem CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_inheritedFromSource {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromSource Q] [Q.RespectsIso] [Q.ContainsIdentities] :
      P.IsClosedUnderIsomorphisms
      source
      theorem CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_inheritedFromTarget {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (Q : MorphismProperty C) [P.InheritedFromTarget Q] [Q.RespectsIso] [Q.ContainsIdentities] :
      P.IsClosedUnderIsomorphisms