Properties of morphisms #

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

respects_iso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.
stable_under_composition: P is stable under composition if P f → P g → P (f ≫ g).
stable_under_base_change: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.

source

def category_theory.morphism_property (C : Type u) [category_theory.category C] :

Type (max u v)

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

Equations

category_theory.morphism_property C = Π ⦃X Y : C⦄, (X ⟶ Y) → Prop

Instances for category_theory.morphism_property

source

@[protected, instance]

def category_theory.morphism_property.complete_lattice (C : Type u) [category_theory.category C] :

complete_lattice (category_theory.morphism_property C)

source

@[protected, instance]

def category_theory.morphism_property.inhabited (C : Type u) [category_theory.category C] :

inhabited (category_theory.morphism_property C)

Equations

category_theory.morphism_property.inhabited C = {default := ⊤}

source

def category_theory.morphism_property.respects_iso {C : Type u} [category_theory.category C] (P : category_theory.morphism_property C) :

Prop

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

Equations

P.respects_iso = ((∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (e.hom ≫ f)) ∧ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (f ≫ e.hom))

source

def category_theory.morphism_property.stable_under_composition {C : Type u} [category_theory.category C] (P : category_theory.morphism_property C) :

Prop

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

Equations

P.stable_under_composition = ∀ ⦃X Y Z : C⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (f ≫ g)

source

def category_theory.morphism_property.stable_under_inverse {C : Type u} [category_theory.category C] (P : category_theory.morphism_property C) :

Prop

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

Equations

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

source

def category_theory.morphism_property.stable_under_base_change {C : Type u} [category_theory.category C] (P : category_theory.morphism_property C) :

Prop

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

Equations

P.stable_under_base_change = ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄, category_theory.is_pullback f' g' g f → P g → P g'

source

theorem category_theory.morphism_property.stable_under_composition.respects_iso {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.stable_under_composition) (hP' : ∀ {X Y : C} (e : X ≅ Y), P e.hom) :

P.respects_iso

source

theorem category_theory.morphism_property.respects_iso.cancel_left_is_iso {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.respects_iso) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso f] :

P (f ≫ g) ↔ P g

source

theorem category_theory.morphism_property.respects_iso.cancel_right_is_iso {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.respects_iso) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso g] :

P (f ≫ g) ↔ P f

source

theorem category_theory.morphism_property.respects_iso.arrow_iso_iff {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.respects_iso) {f g : category_theory.arrow C} (e : f ≅ g) :

P f.hom ↔ P g.hom

source

theorem category_theory.morphism_property.respects_iso.arrow_mk_iso_iff {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.respects_iso) {W X Y Z : C} {f : W ⟶ X} {g : Y ⟶ Z} (e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) :

P f ↔ P g

source

theorem category_theory.morphism_property.respects_iso.of_respects_arrow_iso {C : Type u} [category_theory.category C] (P : category_theory.morphism_property C) (hP : ∀ (f g : category_theory.arrow C), (f ≅ g) → P f.hom → P g.hom) :

P.respects_iso

source

theorem category_theory.morphism_property.stable_under_base_change.mk {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} [category_theory.limits.has_pullbacks C] (hP₁ : P.respects_iso) (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P category_theory.limits.pullback.fst) :

P.stable_under_base_change

source

theorem category_theory.morphism_property.stable_under_base_change.respects_iso {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) :

P.respects_iso

source

theorem category_theory.morphism_property.stable_under_base_change.fst {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [category_theory.limits.has_pullback f g] (H : P g) :

P category_theory.limits.pullback.fst

source

theorem category_theory.morphism_property.stable_under_base_change.snd {C : Type u} [category_theory.category C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [category_theory.limits.has_pullback f g] (H : P f) :

P category_theory.limits.pullback.snd

source

theorem category_theory.morphism_property.stable_under_base_change.base_change_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) {S S' : C} (f : S' ⟶ S) (X : category_theory.over S) (H : P X.hom) :

P ((category_theory.limits.base_change f).obj X).hom

source

theorem category_theory.morphism_property.stable_under_base_change.base_change_map {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) {S S' : C} (f : S' ⟶ S) {X Y : category_theory.over S} (g : X ⟶ Y) (H : P g.left) :

P ((category_theory.limits.base_change f).map g).left

source

theorem category_theory.morphism_property.stable_under_base_change.pullback_map {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {P : category_theory.morphism_property C} (hP : P.stable_under_base_change) (hP' : P.stable_under_composition) {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = i₁ ≫ f') (e₂ : g = i₂ ≫ g') :

P (category_theory.limits.pullback.map f g f' g' i₁ i₂ (𝟙 S) _ _)

source

def category_theory.morphism_property.is_inverted_by {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] (P : category_theory.morphism_property C) (F : C ⥤ D) :

Prop

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

Equations

P.is_inverted_by F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → category_theory.is_iso (F.map f)

source

@[simp]

def category_theory.morphism_property.naturality_property {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F₁ F₂ : C ⥤ D} (app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :

category_theory.morphism_property 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

category_theory.morphism_property.naturality_property app = λ (X Y : C) (f : X ⟶ Y), F₁.map f ≫ app Y = app X ≫ F₂.map f

source

theorem category_theory.morphism_property.naturality_property.is_stable_under_composition {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F₁ F₂ : C ⥤ D} (app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :

(category_theory.morphism_property.naturality_property app).stable_under_composition

source

theorem category_theory.morphism_property.naturality_property.is_stable_under_inverse {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F₁ F₂ : C ⥤ D} (app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :

(category_theory.morphism_property.naturality_property app).stable_under_inverse