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.

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.

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

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

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

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

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

instance CategoryTheory.MorphismProperty.instIsTransMorphismPropertySubsetInstHasSubsetMorphismProperty {C : Type u} [CategoryTheory.Category.{v, u} C] : IsTrans (CategoryTheory.MorphismProperty C) fun x x_1 => x ⊆ x_1

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

theorem CategoryTheory.MorphismProperty.subset_iff_le {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) : P ⊆ Q ↔ P ≤ Q

instance CategoryTheory.MorphismProperty.instIsAntisymmMorphismPropertySubsetInstHasSubsetMorphismProperty {C : Type u} [CategoryTheory.Category.{v, u} C] : IsAntisymm (CategoryTheory.MorphismProperty C) fun x x_1 => x ⊆ x_1

instance CategoryTheory.MorphismProperty.instIsReflMorphismPropertySubsetInstHasSubsetMorphismProperty {C : Type u} [CategoryTheory.Category.{v, u} C] : IsRefl (CategoryTheory.MorphismProperty C) fun x x_1 => x ⊆ x_1

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

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ᵒᵖ

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

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

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 X Y 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] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) (h : P ⊆ Q) : CategoryTheory.MorphismProperty.map P F ⊆ CategoryTheory.MorphismProperty.map Q 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

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

theorem CategoryTheory.MorphismProperty.subset_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] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (h : P ⊆ Q) : CategoryTheory.MorphismProperty.isoClosure P ⊆ CategoryTheory.MorphismProperty.isoClosure Q

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderComposition P) (hP' : {X Y : C} → (e : X ≅ Y) → P X Y e.hom) : CategoryTheory.MorphismProperty.RespectsIso P

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 X Z (CategoryTheory.CategoryStruct.comp f g) ↔ P Y Z 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 X Z (CategoryTheory.CategoryStruct.comp f g) ↔ P X Y 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 ((CategoryTheory.Functor.id C).obj f.left) ((CategoryTheory.Functor.id C).obj f.right) f.hom ↔ P ((CategoryTheory.Functor.id C).obj g.left) ((CategoryTheory.Functor.id C).obj g.right) 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 W X f ↔ P Y Z 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 ((CategoryTheory.Functor.id C).obj f.left) ((CategoryTheory.Functor.id C).obj f.right) f.hom → P ((CategoryTheory.Functor.id C).obj g.left) ((CategoryTheory.Functor.id C).obj g.right) g.hom) : 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.StableUnderBaseChange.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] (hP₁ : CategoryTheory.MorphismProperty.RespectsIso P) (hP₂ : (X Y S : C) → (f : X ⟶ S) → (g : Y ⟶ S) → P Y S g → P (CategoryTheory.Limits.pullback f g) X CategoryTheory.Limits.pullback.fst) : CategoryTheory.MorphismProperty.StableUnderBaseChange P

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

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) {X : C} {Y : C} {S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P Y S g) : P (CategoryTheory.Limits.pullback f g) X CategoryTheory.Limits.pullback.fst

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) {X : C} {Y : C} {S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P X S f) : P (CategoryTheory.Limits.pullback f g) Y CategoryTheory.Limits.pullback.snd

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) {S : C} {S' : C} (f : S' ⟶ S) (X : CategoryTheory.Over S) (H : P ((CategoryTheory.Functor.id C).obj X.left) ((CategoryTheory.Functor.fromPUnit S).obj X.right) X.hom) : P ((CategoryTheory.Functor.id C).obj ((CategoryTheory.Limits.baseChange f).obj X).left) ((CategoryTheory.Functor.fromPUnit S').obj ((CategoryTheory.Limits.baseChange f).obj X).right) ((CategoryTheory.Limits.baseChange f).obj X).hom

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) {S : C} {S' : C} (f : S' ⟶ S) {X : CategoryTheory.Over S} {Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P X.left Y.left g.left) : P ((CategoryTheory.Limits.baseChange f).obj X).left ((CategoryTheory.Limits.baseChange f).obj Y).left ((CategoryTheory.Limits.baseChange f).map g).left

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) (hP' : CategoryTheory.MorphismProperty.StableUnderComposition P) {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₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback f g) (CategoryTheory.Limits.pullback f' g') (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp i₁ f') (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.comp i₂ g'))

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPushouts C] (hP₁ : CategoryTheory.MorphismProperty.RespectsIso P) (hP₂ : (A B A' : C) → (f : A ⟶ A') → (g : A ⟶ B) → P A A' f → P B (CategoryTheory.Limits.pushout f g) CategoryTheory.Limits.pushout.inr) : CategoryTheory.MorphismProperty.StableUnderCobaseChange P

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

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderCobaseChange P) {A : C} {B : C} {A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P A B g) : P A' (CategoryTheory.Limits.pushout f g) CategoryTheory.Limits.pushout.inl

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderCobaseChange P) {A : C} {B : C} {A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P A A' f) : P B (CategoryTheory.Limits.pushout f g) CategoryTheory.Limits.pushout.inr

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderCobaseChange P) : CategoryTheory.MorphismProperty.StableUnderBaseChange (CategoryTheory.MorphismProperty.op P)

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

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) : CategoryTheory.MorphismProperty.StableUnderCobaseChange (CategoryTheory.MorphismProperty.op P)

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

def CategoryTheory.MorphismProperty.IsInvertedBy {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) : Prop

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.

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) (hQ : CategoryTheory.MorphismProperty.IsInvertedBy Q F) (h : P ⊆ Q) : CategoryTheory.MorphismProperty.IsInvertedBy P F

theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [CategoryTheory.Category.{u_5, u_2} C₁] [CategoryTheory.Category.{u_6, u_3} C₂] [CategoryTheory.Category.{u_7, u_4} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) (G : CategoryTheory.Functor C₂ C₃) : CategoryTheory.MorphismProperty.IsInvertedBy W (CategoryTheory.Functor.comp F G)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.op {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C D} (h : CategoryTheory.MorphismProperty.IsInvertedBy W L) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.op W) L.op

theorem CategoryTheory.MorphismProperty.IsInvertedBy.rightOp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.op W) L) : CategoryTheory.MorphismProperty.IsInvertedBy W L.rightOp

theorem CategoryTheory.MorphismProperty.IsInvertedBy.leftOp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C Dᵒᵖ} (h : CategoryTheory.MorphismProperty.IsInvertedBy W L) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.op W) L.leftOp

theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (h : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.op W) L) : CategoryTheory.MorphismProperty.IsInvertedBy W (CategoryTheory.Functor.unop L)

def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : CategoryTheory.MorphismProperty 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.

theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.naturalityProperty app)

theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) : CategoryTheory.MorphismProperty.StableUnderInverse (CategoryTheory.MorphismProperty.naturalityProperty app)

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.StableUnderComposition.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.StableUnderComposition P) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.inverseImage P F)

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

The MorphismProperty C satisfied by isomorphisms in C.

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

The MorphismProperty C satisfied by monomorphisms in C.

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

The MorphismProperty C satisfied by epimorphisms in C.

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

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

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

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

def CategoryTheory.MorphismProperty.FunctorsInverting {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (D : Type u_2) [CategoryTheory.Category.{u_3, u_2} D] : Type (max (max (max u u_2) v) u_3)

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

theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {F₁ : CategoryTheory.MorphismProperty.FunctorsInverting W D} {F₂ : CategoryTheory.MorphismProperty.FunctorsInverting W D} (h : F₁.obj = F₂.obj) : F₁ = F₂

instance CategoryTheory.MorphismProperty.instCategoryFunctorsInverting {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (D : Type u_2) [CategoryTheory.Category.{u_3, u_2} D] : CategoryTheory.Category.{max u u_3, max (max (max u_3 u) v) u_2} (CategoryTheory.MorphismProperty.FunctorsInverting W D)

theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {W : CategoryTheory.MorphismProperty C} {F₁ : CategoryTheory.MorphismProperty.FunctorsInverting W D} {F₂ : CategoryTheory.MorphismProperty.FunctorsInverting W D} {α : F₁ ⟶ F₂} {β : F₁ ⟶ F₂} (h : α.app = β.app) : α = β

def CategoryTheory.MorphismProperty.FunctorsInverting.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (F : CategoryTheory.Functor C D) (hF : CategoryTheory.MorphismProperty.IsInvertedBy W F) : CategoryTheory.MorphismProperty.FunctorsInverting W D

A constructor for W.FunctorsInverting D

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (W : CategoryTheory.MorphismProperty C) {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) : CategoryTheory.MorphismProperty.IsInvertedBy W F₁ ↔ CategoryTheory.MorphismProperty.IsInvertedBy W F₂

@[simp]

theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.isoClosure W) F ↔ CategoryTheory.MorphismProperty.IsInvertedBy W F

@[simp]

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [CategoryTheory.Category.{u_5, u_2} C₁] [CategoryTheory.Category.{u_6, u_3} C₂] [CategoryTheory.Category.{u_7, u_4} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃) [CategoryTheory.ReflectsIsomorphisms G] : CategoryTheory.MorphismProperty.IsInvertedBy W (CategoryTheory.Functor.comp F G) ↔ CategoryTheory.MorphismProperty.IsInvertedBy W F

theorem CategoryTheory.MorphismProperty.isoClosure_subset_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_subset_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 ↔ (X Y : C) → (f : X ⟶ Y) → P X Y f → Q (F.obj X) (F.obj Y) (F.map f)

theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_subset_isomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.MorphismProperty.IsInvertedBy W F ↔ CategoryTheory.MorphismProperty.map W F ⊆ CategoryTheory.MorphismProperty.isomorphisms D

@[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.IsInvertedBy.map_iff {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [CategoryTheory.Category.{u_5, u_2} C₁] [CategoryTheory.Category.{u_6, u_3} C₂] [CategoryTheory.Category.{u_7, u_4} C₃] (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂) (G : CategoryTheory.Functor C₂ C₃) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.map W F) G ↔ CategoryTheory.MorphismProperty.IsInvertedBy W (CategoryTheory.Functor.comp F G)

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_subset {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.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.IsEquivalence F] : CategoryTheory.MorphismProperty.inverseImage (CategoryTheory.MorphismProperty.map P F) F = P

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

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

theorem CategoryTheory.MorphismProperty.diagonal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.MorphismProperty.diagonal P f ↔ P X (CategoryTheory.Limits.pullback.diagonalObj f) (CategoryTheory.Limits.pullback.diagonal f)

theorem CategoryTheory.MorphismProperty.RespectsIso.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.RespectsIso P) : CategoryTheory.MorphismProperty.RespectsIso (CategoryTheory.MorphismProperty.diagonal P)

theorem CategoryTheory.MorphismProperty.StableUnderComposition.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderComposition P) (hP' : CategoryTheory.MorphismProperty.RespectsIso P) (hP'' : CategoryTheory.MorphismProperty.StableUnderBaseChange P) : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.diagonal P)

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) (hP' : CategoryTheory.MorphismProperty.RespectsIso P) : CategoryTheory.MorphismProperty.StableUnderBaseChange (CategoryTheory.MorphismProperty.diagonal P)

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

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

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

theorem CategoryTheory.MorphismProperty.universally_stableUnderBaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty.StableUnderBaseChange (CategoryTheory.MorphismProperty.universally P)

theorem CategoryTheory.MorphismProperty.StableUnderComposition.universally {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderComposition P) : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.universally P)

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

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : CategoryTheory.MorphismProperty.StableUnderBaseChange P) : CategoryTheory.MorphismProperty.universally P = P

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

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

Injectiveness (in a concrete category) as a MorphismProperty

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

Surjectiveness (in a concrete category) as a MorphismProperty

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

Bijectiveness (in a concrete category) as a MorphismProperty

theorem CategoryTheory.MorphismProperty.bijective_eq_sup (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.bijective C = CategoryTheory.MorphismProperty.injective C ⊓ CategoryTheory.MorphismProperty.surjective C

theorem CategoryTheory.MorphismProperty.injective_stableUnderComposition (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.injective C)

theorem CategoryTheory.MorphismProperty.surjective_stableUnderComposition (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.surjective C)

theorem CategoryTheory.MorphismProperty.bijective_stableUnderComposition (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.StableUnderComposition (CategoryTheory.MorphismProperty.bijective C)

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

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

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

class CategoryTheory.MorphismProperty.ContainsIdentities {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) : Prop

• id_mem' : ∀ (X : C), W (CategoryTheory.CategoryStruct.id X)

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

Typeclass expressing that a morphism property contain identities.

theorem CategoryTheory.MorphismProperty.id_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MorphismProperty.ContainsIdentities W] (X : C) : W X X (CategoryTheory.CategoryStruct.id X)

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

instance CategoryTheory.MorphismProperty.ContainsIdentities.unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [CategoryTheory.MorphismProperty.ContainsIdentities W] : CategoryTheory.MorphismProperty.ContainsIdentities (CategoryTheory.MorphismProperty.unop W)

theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MorphismProperty.ContainsIdentities (CategoryTheory.MorphismProperty.op W)] : CategoryTheory.MorphismProperty.ContainsIdentities W

theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [CategoryTheory.MorphismProperty.ContainsIdentities (CategoryTheory.MorphismProperty.unop W)] : CategoryTheory.MorphismProperty.ContainsIdentities W

class CategoryTheory.MorphismProperty.IsMultiplicative {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) extends CategoryTheory.MorphismProperty.ContainsIdentities : Prop

• id_mem' : ∀ (X : C), W (CategoryTheory.CategoryStruct.id X)
• stableUnderComposition : CategoryTheory.MorphismProperty.StableUnderComposition W

  compatibility of

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

theorem CategoryTheory.MorphismProperty.comp_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W X Y f) (hg : W Y Z g) [CategoryTheory.MorphismProperty.IsMultiplicative W] : W X Z (CategoryTheory.CategoryStruct.comp f g)

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

instance CategoryTheory.MorphismProperty.IsMultiplicative.unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [CategoryTheory.MorphismProperty.IsMultiplicative W] : CategoryTheory.MorphismProperty.IsMultiplicative (CategoryTheory.MorphismProperty.unop W)

theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MorphismProperty.IsMultiplicative (CategoryTheory.MorphismProperty.op W)] : CategoryTheory.MorphismProperty.IsMultiplicative W

theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_unop {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [CategoryTheory.MorphismProperty.IsMultiplicative (CategoryTheory.MorphismProperty.unop W)] : CategoryTheory.MorphismProperty.IsMultiplicative W