Compatibilities of properties of morphisms with respect to composition

Given P : MorphismProperty C, we define the predicate P.IsStableUnderComposition which means that P f → P g → P (f ≫ g). We also introduce the type classes W.ContainsIdentities, W.IsMultiplicative, and W.HasTwoOutOfThreeProperty.

class CategoryTheory.MorphismProperty.ContainsIdentities {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) : Prop

Typeclass expressing that a morphism property contain identities.

• id_mem : ∀ (X : C), W (CategoryTheory.CategoryStruct.id X)

  for all X : C, the identity of X satisfies the morphism property

theorem CategoryTheory.MorphismProperty.ContainsIdentities.id_mem {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} [self : W.ContainsIdentities] (X : C), W (CategoryTheory.CategoryStruct.id X)

for all X : C, the identity of X satisfies the morphism property

theorem CategoryTheory.MorphismProperty.id_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] (X : C) : W (CategoryTheory.CategoryStruct.id X)

instance CategoryTheory.MorphismProperty.ContainsIdentities.op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] : W.op.ContainsIdentities

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.ContainsIdentities.unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [W.ContainsIdentities] : W.unop.ContainsIdentities

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.op.ContainsIdentities] : W.ContainsIdentities

theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [W.unop.ContainsIdentities] : W.ContainsIdentities

instance CategoryTheory.MorphismProperty.ContainsIdentities.inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.MorphismProperty D} [P.ContainsIdentities] (F : CategoryTheory.Functor C D) : (P.inverseImage F).ContainsIdentities

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.ContainsIdentities.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.ContainsIdentities] [Q.ContainsIdentities] : (P ⊓ Q).ContainsIdentities

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.Prod.containsIdentities {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_3, u_1} C₁] [CategoryTheory.Category.{u_4, u_2} C₂] (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities] : (W₁.prod W₂).ContainsIdentities

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.Pi.containsIdentities {J : Type w} {C : J → Type u} [(j : J) → CategoryTheory.Category.{v, u} (C j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities] : (CategoryTheory.MorphismProperty.pi W).ContainsIdentities

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : P f

theorem CategoryTheory.MorphismProperty.isomorphisms_le_of_containsIdentities {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] : CategoryTheory.MorphismProperty.isomorphisms C ≤ P

class CategoryTheory.MorphismProperty.IsStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : Prop

A morphism property satisfies IsStableUnderComposition if the composition of two such morphisms still falls in the class.

• comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (CategoryTheory.CategoryStruct.comp f g)

theorem CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.IsStableUnderComposition] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (CategoryTheory.CategoryStruct.comp f g)

theorem CategoryTheory.MorphismProperty.comp_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsStableUnderComposition] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) : W (CategoryTheory.CategoryStruct.comp f g)

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] : P.op.IsStableUnderComposition

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] : P.unop.IsStableUnderComposition

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] [Q.IsStableUnderComposition] : (P ⊓ Q).IsStableUnderComposition

Equations

• ⋯ = ⋯

def CategoryTheory.MorphismProperty.StableUnderInverse {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : Prop

A morphism property is StableUnderInverse if the inverse of a morphism satisfying the property still falls in the class.

Equations

• P.StableUnderInverse = ∀ ⦃X Y : C⦄ (e : X ≅ Y), P e.hom → P e.inv

theorem CategoryTheory.MorphismProperty.StableUnderInverse.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (h : P.StableUnderInverse) : P.op.StableUnderInverse

theorem CategoryTheory.MorphismProperty.StableUnderInverse.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} (h : P.StableUnderInverse) : P.unop.StableUnderInverse

theorem CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] (hP : CategoryTheory.MorphismProperty.isomorphisms C ≤ P) : P.RespectsIso

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.MorphismProperty D} [P.IsStableUnderComposition] (F : CategoryTheory.Functor C D) : (P.inverseImage F).IsStableUnderComposition

Equations

• ⋯ = ⋯

def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : CategoryTheory.MorphismProperty C

Given app : Π X, F₁.obj X ⟶ F₂.obj X where F₁ and F₂ are two functors, this is the morphism_property C satisfied by the morphisms in C with respect to whom app is natural.

Equations

• CategoryTheory.MorphismProperty.naturalityProperty app f = (CategoryTheory.CategoryStruct.comp (F₁.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (F₂.map f))

instance CategoryTheory.MorphismProperty.naturalityProperty.isStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : (CategoryTheory.MorphismProperty.naturalityProperty app).IsStableUnderComposition

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : (CategoryTheory.MorphismProperty.naturalityProperty app).StableUnderInverse

class CategoryTheory.MorphismProperty.IsMultiplicative {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) extends CategoryTheory.MorphismProperty.ContainsIdentities , CategoryTheory.MorphismProperty.IsStableUnderComposition : Prop

A morphism property is multiplicative if it contains identities and is stable by composition.

instance CategoryTheory.MorphismProperty.IsMultiplicative.op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsMultiplicative] : W.op.IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [W.IsMultiplicative] : W.unop.IsMultiplicative

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.op.IsMultiplicative] : W.IsMultiplicative

theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [W.unop.IsMultiplicative] : W.IsMultiplicative

instance CategoryTheory.MorphismProperty.IsMultiplicative.instTop {C : Type u} [CategoryTheory.Category.{v, u} C] : ⊤.IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.instIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.isomorphisms C).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.instMonomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.monomorphisms C).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.instEpimorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.epimorphisms C).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.MorphismProperty D} [P.IsMultiplicative] (F : CategoryTheory.Functor C D) : (P.inverseImage F).IsMultiplicative

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.IsMultiplicative.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.IsMultiplicative] [Q.IsMultiplicative] : (P ⊓ Q).IsMultiplicative

Equations

• ⋯ = ⋯

class CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) extends CategoryTheory.MorphismProperty.IsStableUnderComposition : Prop

A class of morphisms W has the two-out-of-three property if whenever two out of three maps in f, g, f ≫ g are in W, then the third map is also in W.

• comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
• of_postcomp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W g → W (CategoryTheory.CategoryStruct.comp f g) → W f
• of_precomp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W (CategoryTheory.CategoryStruct.comp f g) → W g

theorem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.of_postcomp {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} [self : W.HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W g → W (CategoryTheory.CategoryStruct.comp f g) → W f

theorem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.of_precomp {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} [self : W.HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W (CategoryTheory.CategoryStruct.comp f g) → W g

theorem CategoryTheory.MorphismProperty.of_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W g) (hfg : W (CategoryTheory.CategoryStruct.comp f g)) : W f

theorem CategoryTheory.MorphismProperty.of_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hfg : W (CategoryTheory.CategoryStruct.comp f g)) : W g

theorem CategoryTheory.MorphismProperty.postcomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W g) : W (CategoryTheory.CategoryStruct.comp f g) ↔ W f

theorem CategoryTheory.MorphismProperty.precomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) : W (CategoryTheory.CategoryStruct.comp f g) ↔ W g

instance CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.MorphismProperty.isomorphisms C).HasTwoOutOfThreeProperty

Equations

• ⋯ = ⋯

instance CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty D) [W.HasTwoOutOfThreeProperty] : (W.inverseImage F).HasTwoOutOfThreeProperty

Equations

• ⋯ = ⋯