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.

class CategoryTheory.ObjectProperty.IsStableUnderRetracts {C : Type u} [Category.{v, u} 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 Y also satisfy P X.

• of_retract {X Y : C} : ∀ (x : Retract X Y), P Y → P X

theorem CategoryTheory.ObjectProperty.prop_of_retract {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] {X Y : C} (h : Retract X Y) (hY : P Y) : P X

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsBot {C : Type u} [Category.{v, u} C] : ⊥.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsTop {C : Type u} [Category.{v, u} C] : ⊤.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.IsStableUnderRetracts.instIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] : P.IsClosedUnderIsomorphisms

@[instance 100]

instance CategoryTheory.ObjectProperty.IsStableUnderRetracts.instContainsZeroOfHasZeroObjectOfNonempty {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroObject C] [P.Nonempty] : P.ContainsZero

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_left {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {X Y : C} (c : Limits.BinaryBicone X Y) (h : P c.pt) : P X

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_binaryBicone_right {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {X Y : C} (c : Limits.BinaryBicone X Y) (h : P c.pt) : P Y

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biprod_left {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] (h : P (X ⊞ Y)) : P X

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biprod_right {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {X Y : C} [Limits.HasBinaryBiproduct X Y] (h : P (X ⊞ Y)) : P Y

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_bicone {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {J : Type u_1} (F : J → C) (c : Limits.Bicone F) (h : P c.pt) (j : J) : P (F j)

theorem CategoryTheory.ObjectProperty.IsStableUnderRetracts.of_biproduct {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] [Limits.HasZeroMorphisms C] {J : Type u_1} (F : J → C) [Limits.HasBiproduct F] (h : P (⨁ F)) (j : J) : P (F j)

def CategoryTheory.ObjectProperty.retractClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : ObjectProperty C

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

Equations

• P.retractClosure X = ∃ (Y : C) (_ : P Y), Nonempty (CategoryTheory.Retract X Y)

theorem CategoryTheory.ObjectProperty.prop_retractClosure_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) : P.retractClosure X ↔ ∃ (Y : C) (_ : P Y), Nonempty (Retract X Y)

theorem CategoryTheory.ObjectProperty.prop_retractClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : C} (h : P Y) (r : Retract X Y) : P.retractClosure X

theorem CategoryTheory.ObjectProperty.le_retractClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P ≤ P.retractClosure

instance CategoryTheory.ObjectProperty.instNonemptyRetractClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.Nonempty] : P.retractClosure.Nonempty

theorem CategoryTheory.ObjectProperty.monotone_retractClosure {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) : P.retractClosure ≤ Q.retractClosure

theorem CategoryTheory.ObjectProperty.retractClosure_eq_self {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] : P.retractClosure = P

@[simp]

theorem CategoryTheory.ObjectProperty.retractClosure_bot {C : Type u} [Category.{v, u} C] : ⊥.retractClosure = ⊥

@[simp]

theorem CategoryTheory.ObjectProperty.retractClosure_top {C : Type u} [Category.{v, u} C] : ⊤.retractClosure = ⊤

theorem CategoryTheory.ObjectProperty.retractClosure_le_iff {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [Q.IsStableUnderRetracts] : P.retractClosure ≤ Q ↔ P ≤ Q

theorem CategoryTheory.ObjectProperty.retractClosure_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.isoClosure.retractClosure = P.retractClosure

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsRetractClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.retractClosure.IsStableUnderRetracts

@[simp]

theorem CategoryTheory.ObjectProperty.retractClosure_retractClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : P.retractClosure.retractClosure = P.retractClosure

instance CategoryTheory.ObjectProperty.instEssentiallySmallRetractClosureOfLocallySmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] : ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure