Documentation

Mathlib.CategoryTheory.ObjectProperty.Retract

Properties of objects which are stable under retracts #

Given a category C and P : ObjectProperty C (i.e. P : C → Prop), this file introduces the type class P.IsStableUnderRetracts.

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

A predicate C → Prop on the objects of a category is stable under retracts if whenever P Y, then all the objects X that are retracts of X also satisfy P X.

  • of_retract {X Y : C} : ∀ (x : Retract X Y), P Y → P X
Instances
    source
    theorem CategoryTheory.ObjectProperty.prop_of_retract {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] {X Y : C} (h : Retract X Y) (hY : P Y) :
    P X
    source
    def CategoryTheory.ObjectProperty.retractClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) :
    ObjectProperty C

    The closure by retracts of a predicate on objects in a category.

    Equations
    Instances For
      source
      theorem CategoryTheory.ObjectProperty.prop_retractClosure_iff {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (X : C) :
      P.retractClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (Retract X Y)
      source
      theorem CategoryTheory.ObjectProperty.prop_retractClosure {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {X Y : C} (h : P Y) (r : Retract X Y) :
      P.retractClosure X
      source
      theorem CategoryTheory.ObjectProperty.le_retractClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) :
      P ≤ P.retractClosure
      source
      theorem CategoryTheory.ObjectProperty.monotone_retractClosure {C : Type u_1} [Category.{u_2, u_1} C] {P Q : ObjectProperty C} (h : P ≤ Q) :
      P.retractClosure ≤ Q.retractClosure
      source
      theorem CategoryTheory.ObjectProperty.retractClosure_eq_self {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] :
      P.retractClosure = P
      source
      theorem CategoryTheory.ObjectProperty.retractClosure_le_iff {C : Type u_1} [Category.{u_2, u_1} C] (P Q : ObjectProperty C) [Q.IsStableUnderRetracts] :
      P.retractClosure ≤ Q ↔ P ≤ Q
      source
      instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsRetractClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) :
      P.retractClosure.IsStableUnderRetracts