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)
:
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
Instances
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
theorem
CategoryTheory.ObjectProperty.IsStableUnderRetracts.containsZero
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.IsStableUnderRetracts]
[Limits.HasZeroObject C]
{X : C}
(h : P X)
:
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)
:
The closure by retracts of a predicate on objects in a category.
Instances For
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)
:
theorem
CategoryTheory.ObjectProperty.monotone_retractClosure
{C : Type u}
[Category.{v, u} C]
{P Q : ObjectProperty C}
(h : P ≤ Q)
:
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)
:
instance
CategoryTheory.ObjectProperty.instIsStableUnderRetractsRetractClosure
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
: