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

• P.op 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

• P.unop f = P f.op

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

theorem CategoryTheory.MorphismProperty.op_unop {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty Cᵒᵖ) : P.unop.op = 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

• P.inverseImage 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) : P.inverseImage 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

• P.map 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) : P.map 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) => x.map 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 : P.RespectsIso) : P.op.RespectsIso

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

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

• P.isoClosure 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 ≤ P.isoClosure

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

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 : P.RespectsIso) {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 : P.RespectsIso) {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 : P.RespectsIso) {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 : P.RespectsIso) {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) : P.RespectsIso

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

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

@[simp]

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

theorem CategoryTheory.MorphismProperty.isoClosure_le_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (hQ : Q.RespectsIso) : P.isoClosure ≤ 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) : (P.map F).RespectsIso

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 : Q.RespectsIso) : P.map F ≤ Q ↔ P ≤ Q.inverseImage 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) : P.isoClosure.map F = P.map F

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

theorem CategoryTheory.MorphismProperty.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (hP : P.RespectsIso) : P.map (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) : (P.map F).map G = P.map (F.comp 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 : P.RespectsIso) (F : CategoryTheory.Functor C D) : (P.inverseImage F).RespectsIso

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) : P.map F = P.map 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) : (P.inverseImage F).map F ≤ P.isoClosure

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 : P.RespectsIso) (E : C ≌ D) : P.inverseImage E.functor = P.map 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 : Q.RespectsIso) (E : C ≌ D) : Q.inverseImage E.inverse = Q.map 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 : P.RespectsIso) (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (P.inverseImage F).map 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 : P.RespectsIso) (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (P.map F).inverseImage 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.monomorphisms C).RespectsIso

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

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

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

• W₁.prod 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

• W.functorCategory 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)