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.

Equations

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

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

Equations

• CategoryTheory.instCompleteLatticeMorphismProperty C = id inferInstance

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'

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)

Equations

• CategoryTheory.MorphismProperty.instHasSubsetMorphismProperty = { Subset := fun (P₁ P₂ : CategoryTheory.MorphismProperty C) => ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P₁ f → P₂ f }

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.MorphismProperty.instInterMorphismProperty = { inter := fun (P₁ P₂ : CategoryTheory.MorphismProperty C) (x x_1 : C) (f : x ⟶ x_1) => P₁ f ∧ P₂ f }

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 : CategoryTheory.MorphismProperty C) => x ⊆ x_1

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

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] (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

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

Equations

• CategoryTheory.MorphismProperty.StableUnderComposition P = ∀ ⦃X Y Z : C⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (CategoryTheory.CategoryStruct.comp f g)

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.

Equations

• CategoryTheory.MorphismProperty.StableUnderInverse P = ∀ ⦃X Y : C⦄ (e : X ≅ Y), P e.hom → P e.inv

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.

Equations

• CategoryTheory.MorphismProperty.StableUnderBaseChange P = ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄, CategoryTheory.IsPullback f' g' g f → P g → P g'

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.

Equations

• CategoryTheory.MorphismProperty.StableUnderCobaseChange P = ∀ ⦃A A' B B' : C⦄ ⦃f : A ⟶ A'⦄ ⦃g : A ⟶ B⦄ ⦃f' : B ⟶ B'⦄ ⦃g' : A' ⟶ B'⦄, CategoryTheory.IsPushout g f f' g' → P f → P f'

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 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 (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.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 g → P 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 g) : P 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 f) : P 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 X.hom) : P ((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 g.left) : P ((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 i₁) (h₂ : P i₂) (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

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 f → P 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 g) : P 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 f) : P 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.

Equations

• CategoryTheory.MorphismProperty.IsInvertedBy P F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → CategoryTheory.IsIso (F.map f)

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 L.unop

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.

Equations

• CategoryTheory.MorphismProperty.naturalityProperty app f = (CategoryTheory.CategoryStruct.comp (F₁.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (F₂.map f))

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.

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)

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

Equations

• CategoryTheory.MorphismProperty.FunctorsInverting W D = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => CategoryTheory.MorphismProperty.IsInvertedBy W F

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)

Equations

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

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

Equations

• CategoryTheory.MorphismProperty.FunctorsInverting.mk F hF = { obj := F, property := hF }

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.Functor.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 f → Q (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.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.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.

Equations

• CategoryTheory.MorphismProperty.diagonal P f = P (CategoryTheory.Limits.pullback.diagonal f)

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 (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'.

Equations

• CategoryTheory.MorphismProperty.universally P f = ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), CategoryTheory.IsPullback f' i₁ i₂ f → P f'

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

Equations

• CategoryTheory.MorphismProperty.injective C f = Function.Injective ⇑f

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

Equations

• CategoryTheory.MorphismProperty.surjective C f = Function.Surjective ⇑f

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

Equations

• CategoryTheory.MorphismProperty.bijective C f = Function.Bijective ⇑f

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

Typeclass expressing that a morphism property contain identities.

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

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

theorem CategoryTheory.MorphismProperty.id_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.MorphismProperty.ContainsIdentities W] (X : C) : W (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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

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

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

  compatibility of

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 f) (hg : W g) [CategoryTheory.MorphismProperty.IsMultiplicative W] : W (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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

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)

instance CategoryTheory.MorphismProperty.Prod.containsIdentities {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.ContainsIdentities W₁] [CategoryTheory.MorphismProperty.ContainsIdentities W₂] : CategoryTheory.MorphismProperty.ContainsIdentities (CategoryTheory.MorphismProperty.prod W₁ W₂)

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.IsInvertedBy.prod {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_6, u_2} C₁] [CategoryTheory.Category.{u_7, u_3} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {E₁ : Type u_4} {E₂ : Type u_5} [CategoryTheory.Category.{u_8, u_4} E₁] [CategoryTheory.Category.{u_9, u_5} E₂] {F₁ : CategoryTheory.Functor C₁ E₁} {F₂ : CategoryTheory.Functor C₂ E₂} (h₁ : CategoryTheory.MorphismProperty.IsInvertedBy W₁ F₁) (h₂ : CategoryTheory.MorphismProperty.IsInvertedBy W₂ F₂) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.prod W₁ W₂) (CategoryTheory.Functor.prod F₁ F₂)

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)

instance CategoryTheory.MorphismProperty.Pi.containsIdentities {J : Type w} {C : J → Type u} [(j : J) → CategoryTheory.Category.{v, u} (C j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), CategoryTheory.MorphismProperty.ContainsIdentities (W j)] : CategoryTheory.MorphismProperty.ContainsIdentities (CategoryTheory.MorphismProperty.pi W)

Equations

• ⋯ = ⋯

theorem CategoryTheory.MorphismProperty.IsInvertedBy.pi {J : Type w} {C : J → Type u} {D : J → Type u'} [(j : J) → CategoryTheory.Category.{v, u} (C j)] [(j : J) → CategoryTheory.Category.{v', u'} (D j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) (F : (j : J) → CategoryTheory.Functor (C j) (D j)) (hF : ∀ (j : J), CategoryTheory.MorphismProperty.IsInvertedBy (W j) (F j)) : CategoryTheory.MorphismProperty.IsInvertedBy (CategoryTheory.MorphismProperty.pi W) (CategoryTheory.Functor.pi F)

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)

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

The property that a morphism property W is stable under limits indexed by a category J.

Equations

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

theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.lim_map {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_2} [CategoryTheory.Category.{u_3, u_2} J] (hW : CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape W J) {X : CategoryTheory.Functor J C} {Y : CategoryTheory.Functor J C} (f : X ⟶ Y) [CategoryTheory.Limits.HasLimitsOfShape J C] (hf : CategoryTheory.MorphismProperty.functorCategory W J f) : W (CategoryTheory.Limits.lim.map f)

@[inline, reducible]

abbrev CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_2) : Prop

The property that a morphism property W is stable under products indexed by a type J.

Equations

• CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J = CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape W (CategoryTheory.Discrete J)

theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_2) (hW₀ : CategoryTheory.MorphismProperty.RespectsIso W) [CategoryTheory.Limits.HasProductsOfShape J C] (hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J

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

The condition that a property of morphisms is stable by finite products.

• isStableUnderProductsOfShape : ∀ (J : Type) [inst : Finite J], CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W J

theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type) [Finite J] [CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts W] : CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape W 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)