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.

source

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

Instances

source

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)

source

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

W.op.ContainsIdentities

Equations

⋯ = ⋯

source

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

W.unop.ContainsIdentities

Equations

⋯ = ⋯

source

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

W.ContainsIdentities

source

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

W.ContainsIdentities

source

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

⋯ = ⋯

source

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

(P ⊓ Q).ContainsIdentities

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

P f

source

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

source

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)

Instances

source

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

W (CategoryTheory.CategoryStruct.comp f g)

source

@[instance 900]

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

W.Respects W

Equations

⋯ = ⋯

source

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

P.op.IsStableUnderComposition

Equations

⋯ = ⋯

source

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

P.unop.IsStableUnderComposition

Equations

⋯ = ⋯

source

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

(P ⊓ Q).IsStableUnderComposition

Equations

⋯ = ⋯

source

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

Instances For

source

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

P.op.StableUnderInverse

source

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

P.unop.StableUnderInverse

source

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

source

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

⋯ = ⋯

source

def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F₁ 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))

Instances For

source

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

(CategoryTheory.MorphismProperty.naturalityProperty app).IsStableUnderComposition

Equations

⋯ = ⋯

source

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

(CategoryTheory.MorphismProperty.naturalityProperty app).StableUnderInverse

source

class CategoryTheory.MorphismProperty.IsMultiplicative {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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 (CategoryTheory.CategoryStruct.id X)
comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)

Instances

source

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

W.op.IsMultiplicative

Equations

⋯ = ⋯

source

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

W.unop.IsMultiplicative

Equations

⋯ = ⋯

source

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

W.IsMultiplicative

source

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

W.IsMultiplicative

source

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

⊤.IsMultiplicative

Equations

⋯ = ⋯

source

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

(CategoryTheory.MorphismProperty.isomorphisms C).IsMultiplicative

Equations

⋯ = ⋯

source

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

(CategoryTheory.MorphismProperty.monomorphisms C).IsMultiplicative

Equations

⋯ = ⋯

source

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

(CategoryTheory.MorphismProperty.epimorphisms C).IsMultiplicative

Equations

⋯ = ⋯

source

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

⋯ = ⋯

source

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

(P ⊓ Q).IsMultiplicative

Equations

⋯ = ⋯

source

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

Instances

source

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

Instances

source

class CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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 (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

Instances

source

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

W f

source

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

W g

source

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

W (CategoryTheory.CategoryStruct.comp f g) ↔ W f

source

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

W (CategoryTheory.CategoryStruct.comp f g) ↔ W g

source

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

(CategoryTheory.MorphismProperty.isomorphisms C).HasTwoOutOfThreeProperty

Equations

⋯ = ⋯

source

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

⋯ = ⋯

Documentation

Mathlib.CategoryTheory.MorphismProperty.Composition

Compatibilities of properties of morphisms with respect to composition #