Documentation

Mathlib.CategoryTheory.ObjectProperty.EpiMono

Properties of objects that are closed under subobjects and quotients #

Given a category C and P : ObjectProperty C, we define type classes P.IsClosedUnderSubobjects and P.IsClosedUnderQuotients expressing that P is closed under subobjects (resp. quotients).

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

Given P : ObjectProperty C, we say that P is closed under subobjects, if for any monomorphism X ⟶ Y, P Y implies P X.

  • prop_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (hY : P Y) : P X
Instances
    source
    theorem CategoryTheory.ObjectProperty.prop_of_mono {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] {X Y : C} (f : X ⟶ Y) [Mono f] (hY : P Y) :
    P X
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] :
    P.IsClosedUnderIsomorphisms
    source
    theorem CategoryTheory.ObjectProperty.prop_X₁_of_shortExact {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (hS : S.ShortExact) (h₂ : P S.X₂) :
    P S.X₁
    source
    instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] (F : Functor D C) [F.PreservesMonomorphisms] :
    (P.inverseImage F).IsClosedUnderSubobjects
    source
    class CategoryTheory.ObjectProperty.IsClosedUnderQuotients {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) :
    Prop

    Given P : ObjectProperty C, we say that P is closed under quotients, if for any epimorphism X ⟶ Y, P X implies P Y.

    • prop_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (hX : P X) : P Y
    Instances
      source
      theorem CategoryTheory.ObjectProperty.prop_of_epi {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] {X Y : C} (f : X ⟶ Y) [Epi f] (hX : P X) :
      P Y
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] :
      P.IsClosedUnderIsomorphisms
      source
      theorem CategoryTheory.ObjectProperty.prop_X₃_of_shortExact {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (hS : S.ShortExact) (h₂ : P S.X₂) :
      P S.X₃
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (P : ObjectProperty C) [P.IsClosedUnderQuotients] (F : Functor D C) [F.PreservesEpimorphisms] :
      (P.inverseImage F).IsClosedUnderQuotients
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsTop {C : Type u} [Category.{v, u} C] :
      ⊤.IsClosedUnderSubobjects
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsTop {C : Type u} [Category.{v, u} C] :
      ⊤.IsClosedUnderQuotients
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
      IsClosedUnderSubobjects Limits.IsZero
      source
      instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :
      IsClosedUnderQuotients Limits.IsZero