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).

We also relate these two classes to their analogues in the opposite category: P.op is closed under quotients iff P is closed under subobjects, and dually.

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

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

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

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

P.IsClosedUnderIsomorphisms

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₁

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsISup {C : Type u} [Category.{v, u} C] {ι : Type u_1} (P : ι → ObjectProperty C) [∀ (i : ι), (P i).IsClosedUnderSubobjects] :

(⨆ (i : ι), P i).IsClosedUnderSubobjects

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

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

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] :

P.IsClosedUnderIsomorphisms

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₃

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsISup {C : Type u} [Category.{v, u} C] {ι : Type u_1} (P : ι → ObjectProperty C) [∀ (i : ι), (P i).IsClosedUnderQuotients] :

(⨆ (i : ι), P i).IsClosedUnderQuotients

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsTop {C : Type u} [Category.{v, u} C] :

⊤.IsClosedUnderSubobjects

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsTop {C : Type u} [Category.{v, u} C] :

⊤.IsClosedUnderQuotients

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :

IsClosedUnderSubobjects Limits.IsZero

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] :

IsClosedUnderQuotients Limits.IsZero

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

P.op.IsClosedUnderQuotients ↔ P.IsClosedUnderSubobjects

A property of objects P.op is closed under quotients iff P is closed under subobjects, since epimorphisms in Cᵒᵖ correspond to monomorphisms in C.

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

P.op.IsClosedUnderSubobjects ↔ P.IsClosedUnderQuotients

A property of objects P.op is closed under subobjects iff P is closed under quotients, since monomorphisms in Cᵒᵖ correspond to epimorphisms in C.

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsOppositeOpOfIsClosedUnderSubobjects {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] :

P.op.IsClosedUnderQuotients

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsOppositeOpOfIsClosedUnderQuotients {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] :

P.op.IsClosedUnderSubobjects

theorem CategoryTheory.ObjectProperty.isClosedUnderQuotients_unop_iff {C : Type u} [Category.{v, u} C] (Q : ObjectProperty Cᵒᵖ) :

Q.unop.IsClosedUnderQuotients ↔ Q.IsClosedUnderSubobjects

A property of objects Q.unop is closed under quotients iff Q is closed under subobjects.

theorem CategoryTheory.ObjectProperty.isClosedUnderSubobjects_unop_iff {C : Type u} [Category.{v, u} C] (Q : ObjectProperty Cᵒᵖ) :

Q.unop.IsClosedUnderSubobjects ↔ Q.IsClosedUnderQuotients

A property of objects Q.unop is closed under subobjects iff Q is closed under quotients.

instance CategoryTheory.ObjectProperty.instIsClosedUnderQuotientsUnopOfIsClosedUnderSubobjectsOpposite {C : Type u} [Category.{v, u} C] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderSubobjects] :

Q.unop.IsClosedUnderQuotients

instance CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsUnopOfIsClosedUnderQuotientsOpposite {C : Type u} [Category.{v, u} C] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderQuotients] :

Q.unop.IsClosedUnderSubobjects