Documentation

GeometricallyP.Mathlib.CategoryTheory.ObjectProperty.Stability

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.instInheritedFromSourceIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
      P.InheritedFromSource (MorphismProperty.isomorphisms C)
      source
      instance CategoryTheory.ObjectProperty.instInheritedFromTargetIsomorphismsOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
      P.InheritedFromTarget (MorphismProperty.isomorphisms C)
      source
      instance CategoryTheory.ObjectProperty.instInheritedFromSourceMin {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
      instance CategoryTheory.ObjectProperty.instInheritedFromTargetMin {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.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