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} [Category.{v, u} C] (W : MorphismProperty C) : Prop

Typeclass expressing that a morphism property contain identities.

• id_mem (X : C) : W (CategoryStruct.id X)

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

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

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

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

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

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

theorem CategoryTheory.MorphismProperty.ContainsIdentities.eqToHom {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.ContainsIdentities] {x y : C} (h : x = y) : W (CategoryTheory.eqToHom h)

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

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

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

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

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

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

class CategoryTheory.MorphismProperty.IsStableUnderComposition {C : Type u} [Category.{v, u} C] (P : 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 (CategoryStruct.comp f g)

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

@[instance 900]

instance CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderComposition] : W.Respects W

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

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

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

def CategoryTheory.MorphismProperty.StableUnderInverse {C : Type u} [Category.{v, u} C] (P : 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} [Category.{v, u} C] {P : MorphismProperty C} (h : P.StableUnderInverse) : P.op.StableUnderInverse

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

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

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

def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F₁ F₂ : Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : 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} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F₁ F₂ : Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : (naturalityProperty app).IsStableUnderComposition

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

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

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

• id_mem (X : C) : W (CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W g → W (CategoryStruct.comp f g)

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

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

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

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

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

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

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

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

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

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

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

inductive CategoryTheory.MorphismProperty.multiplicativeClosure {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : MorphismProperty C

Given a morphism property W, the multiplicativeClosure W is the smallest multiplicative property greater than or equal to W.

• of {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {x y : C} (f : x ⟶ y) (hf : W f) : W.multiplicativeClosure f
• id {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} (x : C) : W.multiplicativeClosure (CategoryStruct.id x)
• comp_of {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W.multiplicativeClosure f) (hg : W g) : W.multiplicativeClosure (CategoryStruct.comp f g)

inductive CategoryTheory.MorphismProperty.multiplicativeClosure' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : MorphismProperty C

A variant of multiplicativeClosure in which compositions are taken on the left rather than on the right. It is not intended to be used directly, and one should rather access this via multiplicativeClosure_eq_multiplicativeClosure' in cases where the inductive principle of this variant is needed.

• of {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {x y : C} (f : x ⟶ y) (hf : W f) : W.multiplicativeClosure' f
• id {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} (x : C) : W.multiplicativeClosure' (CategoryStruct.id x)
• of_comp {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : W f) (hg : W.multiplicativeClosure' g) : W.multiplicativeClosure' (CategoryStruct.comp f g)

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

multiplicativeClosure W is multiplicative.

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

multiplicativeClosure' W is multiplicative.

theorem CategoryTheory.MorphismProperty.le_multiplicativeClosure {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W ≤ W.multiplicativeClosure

The multiplicative closure is greater than or equal to the original property.

@[simp]

theorem CategoryTheory.MorphismProperty.multiplicativeClosure_eq_self {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsMultiplicative] : W.multiplicativeClosure = W

The multiplicative closure of a multiplicative property is equal to itself.

theorem CategoryTheory.MorphismProperty.multiplicativeClosure_eq_self_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W.multiplicativeClosure = W ↔ W.IsMultiplicative

@[simp]

theorem CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff {C : Type u} [Category.{v, u} C] (W W' : MorphismProperty C) [W'.IsMultiplicative] : W.multiplicativeClosure ≤ W' ↔ W ≤ W'

The multiplicative closure of W is the smallest multiplicative property greater than or equal to W.

theorem CategoryTheory.MorphismProperty.multiplicativeClosure_monotone {C : Type u} [Category.{v, u} C] : Monotone multiplicativeClosure

theorem CategoryTheory.MorphismProperty.multiplicativeClosure_eq_multiplicativeClosure' {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W.multiplicativeClosure = W.multiplicativeClosure'

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

A class of morphisms W has the of-postcomp property wrt. W' if whenever g is in W' and f ≫ g is in W, also f is in W.

• of_postcomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W' g → W (CategoryStruct.comp f g) → W f

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

A class of morphisms W has the of-precomp property wrt. W' if whenever f is in W' and f ≫ g is in W, also g is in W.

• of_precomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W' f → W (CategoryStruct.comp f g) → W g

class CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) extends W.IsStableUnderComposition, W.HasOfPostcompProperty W, W.HasOfPrecompProperty W : 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 (CategoryStruct.comp f g)
• of_postcomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W g → W (CategoryStruct.comp f g) → W f
• of_precomp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : W f → W (CategoryStruct.comp f g) → W g

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

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

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

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

theorem CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} (Q : MorphismProperty C) [W.HasOfPostcompProperty Q] (hle : W' ≤ Q) : W.HasOfPostcompProperty W'

theorem CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} (Q : MorphismProperty C) [W.HasOfPrecompProperty Q] (hle : W' ≤ Q) : W.HasOfPrecompProperty W'

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

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