Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms structure

Full source

/-- A predicate `C → Prop` on the objects of a category is closed under isomorphisms
if whenever `P X`, then all the objects `Y` that are isomorphic to `X` also satisfy `P Y`. -/
class IsClosedUnderIsomorphisms : Prop where
  of_iso {X Y : C} (_ : X ≅ Y) (_ : P X) : P Y

Property Closed Under Isomorphisms

Informal description

A property $ P $ of objects in a category $ C $ is said to be *closed under isomorphisms* if whenever an object $ X $ satisfies $ P(X) $, then any object $ Y $ isomorphic to $ X $ also satisfies $ P(Y) $.

CategoryTheory.ObjectProperty.prop_of_iso theorem

[IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y

Full source

lemma prop_of_iso [IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y :=
  IsClosedUnderIsomorphisms.of_iso e hX

Isomorphism Invariance of Object Properties

Informal description

Let $ \mathcal{C} $ be a category and $ P $ be a property of objects in $ \mathcal{C} $ that is closed under isomorphisms. For any objects $ X $ and $ Y $ in $ \mathcal{C} $ with an isomorphism $ e : X \cong Y $, if $ X $ satisfies $ P $, then $ Y $ also satisfies $ P $.

CategoryTheory.ObjectProperty.prop_iff_of_iso theorem

[IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) : P X ↔ P Y

Full source

lemma prop_iff_of_iso [IsClosedUnderIsomorphisms P] {X Y : C} (e : X ≅ Y) : P X ↔ P Y :=
  ⟨prop_of_iso P e, prop_of_iso P e.symm⟩

Equivalence of Object Properties Under Isomorphism

Informal description

Let $\mathcal{C}$ be a category and $P$ be a property of objects in $\mathcal{C}$ that is closed under isomorphisms. For any objects $X$ and $Y$ in $\mathcal{C}$ with an isomorphism $e : X \cong Y$, the property $P$ holds for $X$ if and only if it holds for $Y$. In other words, $P(X) \leftrightarrow P(Y)$.

CategoryTheory.ObjectProperty.prop_of_isIso theorem

[IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) : P Y

Full source

lemma prop_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) :
    P Y :=
  prop_of_iso P (asIso f) hX

Isomorphism Invariance of Object Properties via Isomorphism Morphism

Informal description

Let $\mathcal{C}$ be a category and $P$ be a property of objects in $\mathcal{C}$ that is closed under isomorphisms. For any objects $X$ and $Y$ in $\mathcal{C}$ and any isomorphism $f : X \to Y$, if $X$ satisfies $P$, then $Y$ also satisfies $P$.

CategoryTheory.ObjectProperty.prop_iff_of_isIso theorem

[IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y

Full source

lemma prop_iff_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [IsIso f] : P X ↔ P Y :=
  prop_iff_of_iso P (asIso f)

Equivalence of Object Properties Under Isomorphism

Informal description

Let $\mathcal{C}$ be a category and $P$ be a property of objects in $\mathcal{C}$ that is closed under isomorphisms. For any objects $X$ and $Y$ in $\mathcal{C}$ and an isomorphism $f : X \to Y$, the property $P$ holds for $X$ if and only if it holds for $Y$, i.e., $P(X) \leftrightarrow P(Y)$.

CategoryTheory.ObjectProperty.isoClosure definition

: ObjectProperty C

Full source

/-- The closure by isomorphisms of a predicate on objects in a category. -/
def isoClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y)

Closure under isomorphisms of an object property

Informal description

The closure under isomorphisms of a predicate $P$ on objects in a category $\mathcal{C}$ is defined as the property that an object $X$ satisfies if there exists an object $Y$ satisfying $P$ and an isomorphism between $X$ and $Y$. In other words, $X$ is in the closure if it is isomorphic to some object that satisfies $P$.

CategoryTheory.ObjectProperty.prop_isoClosure_iff theorem

(X : C) : isoClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y)

Full source

lemma prop_isoClosure_iff (X : C) :
    isoClosureisoClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y) := by rfl

Characterization of Isomorphism Closure Property: $\text{isoClosure}(P)(X) \leftrightarrow \exists Y, P(Y) \land X \cong Y$

Informal description

For an object $X$ in a category $\mathcal{C}$, the property $\text{isoClosure}(P)(X)$ holds if and only if there exists an object $Y$ in $\mathcal{C}$ such that $P(Y)$ holds and there is an isomorphism between $X$ and $Y$.

CategoryTheory.ObjectProperty.prop_isoClosure theorem

{X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y

Full source

lemma prop_isoClosure {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y :=
  ⟨X, h, ⟨(asIso e).symm⟩⟩

Isomorphism Closure Preserves Property Under Isomorphism

Informal description

Given objects $X$ and $Y$ in a category $\mathcal{C}$, if $X$ satisfies property $P$ and there exists an isomorphism $e : X \to Y$, then $Y$ satisfies the isomorphism closure of $P$.

CategoryTheory.ObjectProperty.le_isoClosure theorem

: P ≤ isoClosure P

Full source

lemma le_isoClosure : P ≤ isoClosure P :=
  fun X hX => ⟨X, hX, ⟨Iso.refl X⟩⟩

Inclusion of Property in its Isomorphism Closure

Informal description

For any object property $P$ in a category $\mathcal{C}$, the property $P$ implies its isomorphism closure, i.e., $P \leq \text{isoClosure}(P)$. This means that if an object $X$ satisfies $P$, then $X$ is in the isomorphism closure of $P$.

CategoryTheory.ObjectProperty.monotone_isoClosure theorem

(h : P ≤ Q) : isoClosure P ≤ isoClosure Q

Full source

lemma monotone_isoClosure (h : P ≤ Q) : isoClosure P ≤ isoClosure Q := by
  rintro X ⟨X', hX', ⟨e⟩⟩
  exact ⟨X', h _ hX', ⟨e⟩⟩

Monotonicity of Isomorphism Closure for Object Properties

Informal description

For any two object properties $P$ and $Q$ in a category $\mathcal{C}$, if $P$ implies $Q$ (i.e., $P \leq Q$), then the isomorphism closure of $P$ implies the isomorphism closure of $Q$ (i.e., $\text{isoClosure}(P) \leq \text{isoClosure}(Q)$).

CategoryTheory.ObjectProperty.isoClosure_eq_self theorem

[IsClosedUnderIsomorphisms P] : isoClosure P = P

Full source

lemma isoClosure_eq_self [IsClosedUnderIsomorphisms P] : isoClosure P = P := by
  apply le_antisymm
  · intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_iso P e.symm hY
  · exact le_isoClosure P

Isomorphism Closure Equals Property for Closed Properties

Informal description

For any property $P$ of objects in a category $\mathcal{C}$ that is closed under isomorphisms, the isomorphism closure of $P$ is equal to $P$ itself, i.e., $\text{isoClosure}(P) = P$.

CategoryTheory.ObjectProperty.isoClosure_le_iff theorem

[IsClosedUnderIsomorphisms Q] : isoClosure P ≤ Q ↔ P ≤ Q

Full source

lemma isoClosure_le_iff [IsClosedUnderIsomorphisms Q] : isoClosureisoClosure P ≤ Q ↔ P ≤ Q :=
  ⟨(le_isoClosure P).trans,
    fun h => (monotone_isoClosure h).trans (by rw [isoClosure_eq_self])⟩

Isomorphism Closure Implication Criterion for Closed Properties

Informal description

For any property $Q$ of objects in a category $\mathcal{C}$ that is closed under isomorphisms, the isomorphism closure of $P$ implies $Q$ if and only if $P$ implies $Q$. In other words, $\text{isoClosure}(P) \leq Q \leftrightarrow P \leq Q$.

CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsoClosure instance

: IsClosedUnderIsomorphisms (isoClosure P)

Full source

instance : IsClosedUnderIsomorphisms (isoClosure P) where
  of_iso := by
    rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
    exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩

Closure Under Isomorphisms is Closed Under Isomorphisms

Informal description

For any category $\mathcal{C}$ and property $P$ on its objects, the closure of $P$ under isomorphisms is itself closed under isomorphisms. That is, if an object $X$ is in the closure of $P$ (meaning $X$ is isomorphic to some object satisfying $P$), then any object isomorphic to $X$ is also in the closure of $P$.

CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMap instance

(F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F)

Full source

instance (F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F) where
  of_iso := by
    rintro _ _ e ⟨X, hX, ⟨e'⟩⟩
    exact ⟨X, hX, ⟨e' ≪≫ e⟩⟩

Functor-Image Property is Closed Under Isomorphisms

Informal description

For any functor $F \colon C \to D$ between categories, the property $P \circ F$ on objects of $D$ is closed under isomorphisms. That is, if an object $Y$ in $D$ satisfies $P(F(Y))$, then any object isomorphic to $Y$ also satisfies $P(F(Y'))$.

CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInverseImage instance

(F : D ⥤ C) [P.IsClosedUnderIsomorphisms] : IsClosedUnderIsomorphisms (P.inverseImage F)

Full source

instance (F : D ⥤ C) [P.IsClosedUnderIsomorphisms] :
    IsClosedUnderIsomorphisms (P.inverseImage F) where
  of_iso e hX := P.prop_of_iso (F.mapIso e) hX

Inverse Image of Isomorphism-Closed Property is Closed Under Isomorphisms

Informal description

For any functor $F \colon D \to C$ between categories and any property $P$ of objects in $C$ that is closed under isomorphisms, the inverse image property $P \circ F$ on objects of $D$ is also closed under isomorphisms. That is, if an object $Y$ in $D$ satisfies $P(F(Y))$, then any object isomorphic to $Y$ also satisfies $P(F(Y'))$.