Documentation

Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Properties of objects which are closed under isomorphisms #

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

source
class CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
Prop

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.

  • of_iso {X Y : C} : ∀ (x : X ≅ Y), P X → P Y
Instances
    source
    @[deprecated CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms (since := "2025-02-25")]
    def CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
    Prop

    Alias of CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.

    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.

    Equations
      Instances For
        source
        theorem CategoryTheory.ObjectProperty.prop_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) :
        P Y
        source
        theorem CategoryTheory.ObjectProperty.prop_iff_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) :
        P X ↔ P Y
        source
        theorem CategoryTheory.ObjectProperty.prop_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) :
        P Y
        source
        theorem CategoryTheory.ObjectProperty.prop_iff_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] :
        P X ↔ P Y
        source
        def CategoryTheory.ObjectProperty.isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
        ObjectProperty C

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

        Equations
          Instances For
            source
            theorem CategoryTheory.ObjectProperty.prop_isoClosure_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) :
            P.isoClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)
            source
            theorem CategoryTheory.ObjectProperty.prop_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] :
            P.isoClosure Y
            source
            theorem CategoryTheory.ObjectProperty.le_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
            P ≤ P.isoClosure
            source
            theorem CategoryTheory.ObjectProperty.monotone_isoClosure {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} (h : P ≤ Q) :
            P.isoClosure ≤ Q.isoClosure
            source
            theorem CategoryTheory.ObjectProperty.isoClosure_eq_self {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
            P.isoClosure = P
            source
            theorem CategoryTheory.ObjectProperty.isoClosure_le_iff {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [Q.IsClosedUnderIsomorphisms] :
            P.isoClosure ≤ Q ↔ P ≤ Q
            source
            instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
            P.isoClosure.IsClosedUnderIsomorphisms
            source
            instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMap {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor C D) :
            (P.map F).IsClosedUnderIsomorphisms
            source
            instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInverseImage {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) (F : Functor D C) [P.IsClosedUnderIsomorphisms] :
            (P.inverseImage F).IsClosedUnderIsomorphisms
            source
            @[deprecated CategoryTheory.ObjectProperty.prop_of_iso (since := "2025-02-25")]
            theorem CategoryTheory.mem_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) :
            P Y

            Alias of CategoryTheory.ObjectProperty.prop_of_iso.

            source
            @[deprecated CategoryTheory.ObjectProperty.prop_iff_of_iso (since := "2025-02-25")]
            theorem CategoryTheory.mem_iff_of_iso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) :
            P X ↔ P Y

            Alias of CategoryTheory.ObjectProperty.prop_iff_of_iso.

            source
            @[deprecated CategoryTheory.ObjectProperty.prop_of_isIso (since := "2025-02-25")]
            theorem CategoryTheory.mem_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] (hX : P X) :
            P Y

            Alias of CategoryTheory.ObjectProperty.prop_of_isIso.

            source
            @[deprecated CategoryTheory.ObjectProperty.prop_iff_of_isIso (since := "2025-02-25")]
            theorem CategoryTheory.mem_iff_of_isIso {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [IsIso f] :
            P X ↔ P Y

            Alias of CategoryTheory.ObjectProperty.prop_iff_of_isIso.

            source
            @[deprecated CategoryTheory.ObjectProperty.isoClosure (since := "2025-02-25")]
            def CategoryTheory.isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
            ObjectProperty C

            Alias of CategoryTheory.ObjectProperty.isoClosure.

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

            Equations
              Instances For
                source
                @[deprecated CategoryTheory.ObjectProperty.prop_isoClosure_iff (since := "2025-02-25")]
                theorem CategoryTheory.mem_isoClosure_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (X : C) :
                P.isoClosure X ↔ ∃ (Y : C), ∃ (x : P Y), Nonempty (X ≅ Y)

                Alias of CategoryTheory.ObjectProperty.prop_isoClosure_iff.

                source
                @[deprecated CategoryTheory.ObjectProperty.prop_isoClosure (since := "2025-02-25")]
                theorem CategoryTheory.mem_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] :
                P.isoClosure Y

                Alias of CategoryTheory.ObjectProperty.prop_isoClosure.