Properties of morphisms

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

• RespectsIso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.

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

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

Equations

• CategoryTheory.MorphismProperty C = (⦃X Y : C⦄ → (X ⟶ Y) → Prop)

instance CategoryTheory.instCompleteBooleanAlgebraMorphismProperty (C : Type u) [CategoryTheory.Category.{v, u} C] : CompleteBooleanAlgebra (CategoryTheory.MorphismProperty C)

Equations

• CategoryTheory.instCompleteBooleanAlgebraMorphismProperty C = let __spread.0 := inferInstanceAs (CompleteBooleanAlgebra (⦃X Y : C⦄ → (X ⟶ Y) → Prop)); CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem CategoryTheory.MorphismProperty.le_def (C : Type u) [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} : P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f

instance CategoryTheory.instInhabitedMorphismProperty (C : Type u) [CategoryTheory.Category.{v, u} C] : Inhabited (CategoryTheory.MorphismProperty C)

Equations

• CategoryTheory.instInhabitedMorphismProperty C = { default := ⊤ }

theorem CategoryTheory.MorphismProperty.top_eq (C : Type u) [CategoryTheory.Category.{v, u} C] : ⊤ = fun (x x_1 : C) (x : x ⟶ x_1) => True

theorem CategoryTheory.MorphismProperty.ext {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (W' : CategoryTheory.MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) : W = W'

@[simp]

theorem CategoryTheory.MorphismProperty.top_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : ⊤ f

def CategoryTheory.MorphismProperty.op {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty Cᵒᵖ

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

Equations

• CategoryTheory.MorphismProperty.op P f = P f.unop

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

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

Equations

• CategoryTheory.MorphismProperty.unop P f = P f.op

theorem CategoryTheory.MorphismProperty.unop_op {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.unop (CategoryTheory.MorphismProperty.op P) = P

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

def CategoryTheory.MorphismProperty.inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty C

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

Equations

• CategoryTheory.MorphismProperty.inverseImage P F f = P (F.map f)

@[simp]

theorem CategoryTheory.MorphismProperty.inverseImage_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.inverseImage P F f ↔ P (F.map f)

def CategoryTheory.MorphismProperty.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty D

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

Equations

• CategoryTheory.MorphismProperty.map P F f = ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : P f'), Nonempty (CategoryTheory.Arrow.mk (F.map f') ≅ CategoryTheory.Arrow.mk f)

theorem CategoryTheory.MorphismProperty.map_mem_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) (hf : P f) : CategoryTheory.MorphismProperty.map P F (F.map f)

theorem CategoryTheory.MorphismProperty.monotone_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : Monotone fun (x : CategoryTheory.MorphismProperty C) => CategoryTheory.MorphismProperty.map x F

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

The closure by isomorphisms of a MorphismProperty

Equations

• CategoryTheory.MorphismProperty.isoClosure P f = ∃ (Y₁ : C) (Y₂ : C) (f' : Y₁ ⟶ Y₂) (_ : P f'), Nonempty (CategoryTheory.Arrow.mk f' ≅ CategoryTheory.Arrow.mk f)

theorem CategoryTheory.MorphismProperty.le_isoClosure {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P ≤ CategoryTheory.MorphismProperty.isoClosure P

theorem CategoryTheory.MorphismProperty.isoClosure_respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.isoClosure P)

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

theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : P (CategoryTheory.CategoryStruct.comp f g) ↔ P g

theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : P (CategoryTheory.CategoryStruct.comp f g) ↔ P f

theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) {f : CategoryTheory.Arrow C} {g : CategoryTheory.Arrow C} (e : f ≅ g) : P f.hom ↔ P g.hom

theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) {W : C} {X : C} {Y : C} {Z : C} {f : W ⟶ X} {g : Y ⟶ Z} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : P f ↔ P g

theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (hP : ∀ (f g : CategoryTheory.Arrow C), (f ≅ g) → P f.hom → P g.hom) : CategoryTheory.MorphismProperty.RespectsIso P

theorem CategoryTheory.MorphismProperty.isoClosure_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} : CategoryTheory.MorphismProperty.isoClosure P = P ↔ CategoryTheory.MorphismProperty.RespectsIso P

theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) : CategoryTheory.MorphismProperty.isoClosure P = P

@[simp]

theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.isoClosure (CategoryTheory.MorphismProperty.isoClosure P) = CategoryTheory.MorphismProperty.isoClosure P

theorem CategoryTheory.MorphismProperty.isoClosure_le_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (hQ : CategoryTheory.MorphismProperty.RespectsIso Q) : CategoryTheory.MorphismProperty.isoClosure P ≤ Q ↔ P ≤ Q

theorem CategoryTheory.MorphismProperty.map_respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.map P F)

theorem CategoryTheory.MorphismProperty.map_le_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {P : CategoryTheory.MorphismProperty C} {F : CategoryTheory.Functor C D} {Q : CategoryTheory.MorphismProperty D} (hQ : CategoryTheory.MorphismProperty.RespectsIso Q) : CategoryTheory.MorphismProperty.map P F ≤ Q ↔ P ≤ CategoryTheory.MorphismProperty.inverseImage Q F

@[simp]

theorem CategoryTheory.MorphismProperty.map_isoClosure {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.map (CategoryTheory.MorphismProperty.isoClosure P) F = CategoryTheory.MorphismProperty.map P F

theorem CategoryTheory.MorphismProperty.map_id_eq_isoClosure {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.map P (CategoryTheory.Functor.id C) = CategoryTheory.MorphismProperty.isoClosure P

theorem CategoryTheory.MorphismProperty.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (hP : CategoryTheory.MorphismProperty.RespectsIso P) : CategoryTheory.MorphismProperty.map P (CategoryTheory.Functor.id C) = P

@[simp]

theorem CategoryTheory.MorphismProperty.map_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] (G : CategoryTheory.Functor D E) : CategoryTheory.MorphismProperty.map (CategoryTheory.MorphismProperty.map P F) G = CategoryTheory.MorphismProperty.map P (CategoryTheory.Functor.comp F G)

theorem CategoryTheory.MorphismProperty.RespectsIso.inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {P : CategoryTheory.MorphismProperty D} (h : CategoryTheory.MorphismProperty.RespectsIso P) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.inverseImage P F)

theorem CategoryTheory.MorphismProperty.map_eq_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (e : F ≅ G) : CategoryTheory.MorphismProperty.map P F = CategoryTheory.MorphismProperty.map P G

theorem CategoryTheory.MorphismProperty.map_inverseImage_le {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.map (CategoryTheory.MorphismProperty.inverseImage P F) F ≤ CategoryTheory.MorphismProperty.isoClosure P

theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D) (hP : CategoryTheory.MorphismProperty.RespectsIso P) (E : C ≌ D) : CategoryTheory.MorphismProperty.inverseImage P E.functor = CategoryTheory.MorphismProperty.map P E.inverse

theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (Q : CategoryTheory.MorphismProperty C) (hQ : CategoryTheory.MorphismProperty.RespectsIso Q) (E : C ≌ D) : CategoryTheory.MorphismProperty.inverseImage Q E.inverse = CategoryTheory.MorphismProperty.map Q E.functor

theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D) (hP : CategoryTheory.MorphismProperty.RespectsIso P) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsEquivalence F] : CategoryTheory.MorphismProperty.map (CategoryTheory.MorphismProperty.inverseImage P F) F = P

theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (hP : CategoryTheory.MorphismProperty.RespectsIso P) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.IsEquivalence F] : CategoryTheory.MorphismProperty.inverseImage (CategoryTheory.MorphismProperty.map P F) F = P

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

The MorphismProperty C satisfied by isomorphisms in C.

Equations

• CategoryTheory.MorphismProperty.isomorphisms C f = CategoryTheory.IsIso f

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

The MorphismProperty C satisfied by monomorphisms in C.

Equations

• CategoryTheory.MorphismProperty.monomorphisms C f = CategoryTheory.Mono f

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

The MorphismProperty C satisfied by epimorphisms in C.

Equations

• CategoryTheory.MorphismProperty.epimorphisms C f = CategoryTheory.Epi f

@[simp]

theorem CategoryTheory.MorphismProperty.isomorphisms.iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.isomorphisms C f ↔ CategoryTheory.IsIso f

@[simp]

theorem CategoryTheory.MorphismProperty.monomorphisms.iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.monomorphisms C f ↔ CategoryTheory.Mono f

@[simp]

theorem CategoryTheory.MorphismProperty.epimorphisms.iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.MorphismProperty.epimorphisms C f ↔ CategoryTheory.Epi f

theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsIso f] : CategoryTheory.MorphismProperty.isomorphisms C f

theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [hf : CategoryTheory.Mono f] : CategoryTheory.MorphismProperty.monomorphisms C f

theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X ⟶ Y) [hf : CategoryTheory.Epi f] : CategoryTheory.MorphismProperty.epimorphisms C f

theorem CategoryTheory.MorphismProperty.RespectsIso.monomorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.monomorphisms C)

theorem CategoryTheory.MorphismProperty.RespectsIso.epimorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.epimorphisms C)

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

def CategoryTheory.MorphismProperty.prod {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_4, u_2} C₁] [CategoryTheory.Category.{u_5, u_3} C₂] (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) : CategoryTheory.MorphismProperty (C₁ × C₂)

If W₁ and W₂ are morphism properties on two categories C₁ and C₂, this is the induced morphism property on C₁ × C₂.

Equations

• CategoryTheory.MorphismProperty.prod W₁ W₂ f = (W₁ f.1 ∧ W₂ f.2)

def CategoryTheory.MorphismProperty.pi {J : Type w} {C : J → Type u} [(j : J) → CategoryTheory.Category.{v, u} (C j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) : CategoryTheory.MorphismProperty ((j : J) → C j)

If W j are morphism properties on categories C j for all j, this is the induced morphism property on the category ∀ j, C j.

Equations

• CategoryTheory.MorphismProperty.pi W f = ∀ (j : J), W j (f j)

def CategoryTheory.MorphismProperty.functorCategory {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_2) [CategoryTheory.Category.{u_3, u_2} J] : CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)

The morphism property on J ⥤ C which is defined objectwise from W : MorphismProperty C.

Equations

• CategoryTheory.MorphismProperty.functorCategory W J f = ∀ (j : J), W (f.app j)

theorem CategoryTheory.NatTrans.isIso_app_iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) {X : C} {Y : C} (e : X ≅ Y) : CategoryTheory.IsIso (α.app X) ↔ CategoryTheory.IsIso (α.app Y)