Properties of morphisms

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

• RespectsLeft P Q: P respects the property Q on the left if P f → P (i ≫ f) where i satisfies Q.
• RespectsRight P Q: P respects the property Q on the right if P f → P (f ≫ i) where i satisfies Q.
• Respects: P respects Q if P respects Q both on the left and on the right.

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 = CompleteBooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem CategoryTheory.MorphismProperty.le_def (C : Type u) [CategoryTheory.Category.{v, u} C] {P 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 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 Y : C} (f : X ⟶ Y) : ⊤ f

@[simp]

theorem CategoryTheory.MorphismProperty.sSup_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (S : Set (CategoryTheory.MorphismProperty C)) {X Y : C} (f : X ⟶ Y) : sSup S f ↔ ∃ (W : ↑S), ↑W f

@[simp]

theorem CategoryTheory.MorphismProperty.iSup_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (W : ι → CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) : iSup W f ↔ ∃ (i : ι), W i 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 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 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.toSet {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : Set (CategoryTheory.Arrow C)

The set in Set (Arrow C) which corresponds to P : MorphismProperty C.

Equations

• P.toSet = {f : CategoryTheory.Arrow C | P f.hom}

def CategoryTheory.MorphismProperty.homFamily {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (f : ↑P.toSet) : (↑f).left ⟶ (↑f).right

The family of morphisms indexed by P.toSet which corresponds to P : MorphismProperty C, see MorphismProperty.ofHoms_homFamily.

Equations

• P.homFamily f = (↑f).hom

theorem CategoryTheory.MorphismProperty.homFamily_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (f : ↑P.toSet) : P.homFamily f = (↑f).hom

@[simp]

theorem CategoryTheory.MorphismProperty.homFamily_arrow_mk {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) (hf : P f) : P.homFamily ⟨CategoryTheory.Arrow.mk f, hf⟩ = f

@[simp]

theorem CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y) : CategoryTheory.Arrow.mk f ∈ P.toSet ↔ P f

theorem CategoryTheory.MorphismProperty.of_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : P f) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y') (h : f' = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom hY))) : P f'

inductive CategoryTheory.MorphismProperty.ofHoms {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i) : CategoryTheory.MorphismProperty C

The class of morphisms given by a family of morphisms f i : X i ⟶ Y i.

• mk {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X Y : ι → C} {f : (i : ι) → X i ⟶ Y i} (i : ι) : CategoryTheory.MorphismProperty.ofHoms f (f i)

theorem CategoryTheory.MorphismProperty.ofHoms_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i) {A B : C} (g : A ⟶ B) : CategoryTheory.MorphismProperty.ofHoms f g ↔ ∃ (i : ι), CategoryTheory.Arrow.mk g = CategoryTheory.Arrow.mk (f i)

@[simp]

theorem CategoryTheory.MorphismProperty.ofHoms_homFamily {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.ofHoms P.homFamily = P

class CategoryTheory.MorphismProperty.RespectsRight {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) : Prop

A morphism property P satisfies P.RespectsRight Q if it is stable under post-composition with morphisms satisfying Q, i.e. whenever P holds for f and Q holds for i then P holds for f ≫ i.

• postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : Q i) (f : X ⟶ Y) (hf : P f) : P (CategoryTheory.CategoryStruct.comp f i)

class CategoryTheory.MorphismProperty.RespectsLeft {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) : Prop

A morphism property P satisfies P.RespectsLeft Q if it is stable under pre-composition with morphisms satisfying Q, i.e. whenever P holds for f and Q holds for i then P holds for i ≫ f.

• precomp {X Y Z : C} (i : X ⟶ Y) (hi : Q i) (f : Y ⟶ Z) (hf : P f) : P (CategoryTheory.CategoryStruct.comp i f)

class CategoryTheory.MorphismProperty.Respects {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) extends P.RespectsLeft Q, P.RespectsRight Q : Prop

A morphism property P satisfies P.Respects Q if it is stable under composition on the left and right by morphisms satisfying Q.

• precomp {X Y Z : C} (i : X ⟶ Y) (hi : Q i) (f : Y ⟶ Z) (hf : P f) : P (CategoryTheory.CategoryStruct.comp i f)
• postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : Q i) (f : X ⟶ Y) (hf : P f) : P (CategoryTheory.CategoryStruct.comp f i)

instance CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [P.RespectsLeft Q] [P.RespectsRight Q] : P.Respects Q

instance CategoryTheory.MorphismProperty.instRespectsRightOppositeOpOfRespectsLeft {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [P.RespectsLeft Q] : P.op.RespectsRight Q.op

instance CategoryTheory.MorphismProperty.instRespectsLeftOppositeOpOfRespectsRight {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [P.RespectsRight Q] : P.op.RespectsLeft Q.op

instance CategoryTheory.MorphismProperty.RespectsLeft.inf {C : Type u} [CategoryTheory.Category.{v, u} C] (P₁ P₂ Q : CategoryTheory.MorphismProperty C) [P₁.RespectsLeft Q] [P₂.RespectsLeft Q] : (P₁ ⊓ P₂).RespectsLeft Q

instance CategoryTheory.MorphismProperty.RespectsRight.inf {C : Type u} [CategoryTheory.Category.{v, u} C] (P₁ P₂ Q : CategoryTheory.MorphismProperty C) [P₁.RespectsRight Q] [P₂.RespectsRight Q] : (P₁ ⊓ P₂).RespectsRight Q

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

@[reducible, inline]

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

P respects isomorphisms, if it respects the morphism property isomorphisms C, i.e. it is stable under pre- and postcomposition with isomorphisms.

Equations

• P.RespectsIso = P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)

theorem CategoryTheory.MorphismProperty.RespectsIso.mk {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) (hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) : P.RespectsIso

theorem CategoryTheory.MorphismProperty.RespectsIso.precomp {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : X ⟶ Y) [CategoryTheory.IsIso e] (f : Y ⟶ Z) (hf : P f) : P (CategoryTheory.CategoryStruct.comp e f)

instance CategoryTheory.MorphismProperty.instRespectsIsoTop {C : Type u} [CategoryTheory.Category.{v, u} C] : ⊤.RespectsIso

theorem CategoryTheory.MorphismProperty.RespectsIso.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y ⟶ Z) [CategoryTheory.IsIso e] (f : X ⟶ Y) (hf : P f) : P (CategoryTheory.CategoryStruct.comp f e)

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

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

instance 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.cancel_left_of_respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [hP : P.RespectsIso] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : P (CategoryTheory.CategoryStruct.comp f g) ↔ P g

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

theorem CategoryTheory.MorphismProperty.comma_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {A : Type u_2} {B : Type u_3} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.Category.{u_5, u_3} B] {L : CategoryTheory.Functor A C} {R : CategoryTheory.Functor B C} {f g : CategoryTheory.Comma L R} (e : f ≅ g) : P f.hom ↔ P g.hom

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

theorem CategoryTheory.MorphismProperty.arrow_mk_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {W X Y 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.isoClosure_eq_self {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [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 Q : CategoryTheory.MorphismProperty C) [Q.RespectsIso] : P.isoClosure ≤ Q ↔ P ≤ Q

instance 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) [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) [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)

instance 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) [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 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) [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) [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) [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) [P.RespectsIso] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : (P.map F).inverseImage F = P

@[simp]

theorem CategoryTheory.MorphismProperty.isomorphisms.iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X 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 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 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 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 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 Y : C} (f : X ⟶ Y) [hf : CategoryTheory.Epi f] : CategoryTheory.MorphismProperty.epimorphisms C f

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

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

instance 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)

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

Given W : MorphismProperty C, this is the morphism property on Arrow C of morphisms whose left and right parts are in W.

Equations

• W.arrow f = (W f.left ∧ W f.right)

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 G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : CategoryTheory.IsIso (α.app X) ↔ CategoryTheory.IsIso (α.app Y)