# Documentation

Mathlib.CategoryTheory.MorphismProperty

# Properties of morphisms #

We provide the basic framework for talking about properties of morphisms. The following meta-properties are defined

• RespectsIso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.
• StableUnderComposition: P is stable under composition if P f → P g → P (f ≫ g).
• StableUnderBaseChange: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.
• StableUnderCobaseChange: P is stable under cobase change if in all pushout squares, the right map satisfies P if the left map satisfies it.

A MorphismProperty C is a class of morphisms between objects in C.

Instances For
theorem CategoryTheory.MorphismProperty.top_apply {C : Type u} {X : C} {Y : C} (f : X Y) :
f

The morphism property in Cᵒᵖ associated to a morphism property in C

Instances For

The morphism property in C associated to a morphism property in Cᵒᵖ

Instances For
def CategoryTheory.MorphismProperty.inverseImage {C : Type u} {D : Type u_1} [] (F : ) :

The inverse image of a MorphismProperty D by a functor C ⥤ D

Instances For
def CategoryTheory.MorphismProperty.map {C : Type u} {D : Type u_1} [] (F : ) :

The image (up to isomorphisms) of a MorphismProperty C by a functor C ⥤ D

Instances For
theorem CategoryTheory.MorphismProperty.map_mem_map {C : Type u} {D : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) (hf : P X Y f) :
theorem CategoryTheory.MorphismProperty.monotone_map {C : Type u} {D : Type u_1} [] (F : ) (h : P Q) :

A morphism property RespectsIso if it still holds when composed with an isomorphism

Instances For

The closure by isomorphisms of a MorphismProperty

Instances For

A morphism property is StableUnderComposition if the composition of two such morphisms still falls in the class.

Instances For

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

Instances For

A morphism property is StableUnderBaseChange if the base change of such a morphism still falls in the class.

Instances For

A morphism property is StableUnderCobaseChange if the cobase change of such a morphism still falls in the class.

Instances For
theorem CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso {C : Type u} (hP' : {X Y : C} → (e : X Y) → P X Y e.hom) :
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P X Z () P Y Z g
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P X Z () P X Y f
theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff {C : Type u} {f : } {g : } (e : f g) :
P (().obj f.left) (().obj f.right) f.hom P (().obj g.left) (().obj g.right) g.hom
theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff {C : Type u} {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} :
P W X f P Y Z g
theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso {C : Type u} (hP : (f g : ) → (f g) → P (().obj f.left) (().obj f.right) f.homP (().obj g.left) (().obj g.right) g.hom) :
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.mk {C : Type u} (hP₂ : (X Y S : C) → (f : X S) → (g : Y S) → P Y S gP () X CategoryTheory.Limits.pullback.fst) :
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst {C : Type u} {X : C} {Y : C} {S : C} (f : X S) (g : Y S) (H : P Y S g) :
P () X CategoryTheory.Limits.pullback.fst
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd {C : Type u} {X : C} {Y : C} {S : C} (f : X S) (g : Y S) (H : P X S f) :
P () Y CategoryTheory.Limits.pullback.snd
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj {C : Type u} {S : C} {S' : C} (f : S' S) (X : ) (H : P (().obj X.left) (().obj X.right) X.hom) :
P (().obj (().obj X).left) (().obj (().obj X).right) (().obj X).hom
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map {C : Type u} {S : C} {S' : C} (f : S' S) {X : } {Y : } (g : X Y) (H : P X.left Y.left g.left) :
P (().obj X).left (().obj Y).left (().map g).left
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map {C : Type u} {S : C} {X : C} {X' : C} {Y : C} {Y' : C} {f : X S} {g : Y S} {f' : X' S} {g' : Y' S} {i₁ : X X'} {i₂ : Y Y'} (h₁ : P X X' i₁) (h₂ : P Y Y' i₂) (e₁ : ) (e₂ : ) :
P () () (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ () (_ : ) (_ : ))
theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk {C : Type u} (hP₂ : (A B A' : C) → (f : A A') → (g : A B) → P A A' fP B () CategoryTheory.Limits.pushout.inr) :
theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl {C : Type u} {A : C} {B : C} {A' : C} (f : A A') (g : A B) (H : P A B g) :
P A' () CategoryTheory.Limits.pushout.inl
theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr {C : Type u} {A : C} {B : C} {A' : C} (f : A A') (g : A B) (H : P A A' f) :
P B () CategoryTheory.Limits.pushout.inr

If P : MorphismProperty C and F : C ⥤ D, then P.IsInvertedBy F means that all morphisms in P are mapped by F to isomorphisms in D.

Instances For
theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset {C : Type u} {D : Type u_1} [] (F : ) (h : P Q) :
theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [] [] [] (W : ) (F : ) (G : ) :
def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} {D : Type u_1} [] {F₁ : } {F₂ : } (app : (X : C) → F₁.obj X F₂.obj X) :

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.

Instances For
theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition {C : Type u} {D : Type u_1} [] {F₁ : } {F₂ : } (app : (X : C) → F₁.obj X F₂.obj X) :
theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse {C : Type u} {D : Type u_1} [] {F₁ : } {F₂ : } (app : (X : C) → F₁.obj X F₂.obj X) :

The MorphismProperty C satisfied by isomorphisms in C.

Instances For

The MorphismProperty C satisfied by monomorphisms in C.

Instances For

The MorphismProperty C satisfied by epimorphisms in C.

Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.isomorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.monomorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.epimorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
def CategoryTheory.MorphismProperty.FunctorsInverting {C : Type u} (D : Type u_2) [] :
Type (max (max (max u u_2) v) u_3)

The full subcategory of C ⥤ D consisting of functors inverting morphisms in W

Instances For
theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext {C : Type u} {D : Type u_1} [] (h : F₁.obj = F₂.obj) :
F₁ = F₂
theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext {C : Type u} {D : Type u_1} [] {α : F₁ F₂} {β : F₁ F₂} (h : α.app = β.app) :
α = β

A constructor for W.FunctorsInverting D

Instances For
theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso {C : Type u} {D : Type u_1} [] {F₁ : } {F₂ : } (e : F₁ F₂) :
@[simp]
@[simp]
theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [] [] [] (W : ) (F : ) (G : ) :
theorem CategoryTheory.MorphismProperty.map_subset_iff {C : Type u} {D : Type u_1} [] (F : ) :
(X Y : C) → (f : X Y) → P X Y fQ (F.obj X) (F.obj Y) (F.map f)
@[simp]
theorem CategoryTheory.MorphismProperty.map_isoClosure {C : Type u} {D : Type u_1} [] (F : ) :
@[simp]
theorem CategoryTheory.MorphismProperty.map_map {C : Type u} {D : Type u_1} [] (F : ) {E : Type u_2} [] (G : ) :
theorem CategoryTheory.MorphismProperty.IsInvertedBy.map_iff {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [] [] [] (W : ) (F : ) (G : ) :
theorem CategoryTheory.MorphismProperty.map_eq_of_iso {C : Type u} {D : Type u_1} [] {F : } {G : } (e : F G) :

For P : MorphismProperty C, P.diagonal is a morphism property that holds for f : X ⟶ Y whenever P holds for X ⟶ Y xₓ Y.

Instances For
theorem CategoryTheory.MorphismProperty.diagonal_iff {C : Type u} {X : C} {Y : C} {f : X Y} :

P.universally holds for a morphism f : X ⟶ Y iff P holds for all X ×[Y] Y' ⟶ Y'.

Instances For
theorem CategoryTheory.MorphismProperty.universally_mono {C : Type u} :
Monotone CategoryTheory.MorphismProperty.universally

Injectiveness (in a concrete category) as a MorphismProperty

Instances For

Surjectiveness (in a concrete category) as a MorphismProperty

Instances For

Bijectiveness (in a concrete category) as a MorphismProperty

Instances For
• id_mem' : ∀ (X : C),

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

Typeclass expressing that a morphism property contain identities.

Instances
• id_mem' : ∀ (X : C),
• stableUnderComposition :

compatibility of

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

Instances
theorem CategoryTheory.MorphismProperty.comp_mem {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hf : W X Y f) (hg : W Y Z g) :
W X Z ()