doc-next-gen

Mathlib.CategoryTheory.MorphismProperty.Basic

Module docstring

{"# Properties of morphisms

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

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

"}

CategoryTheory.MorphismProperty definition
Full source 
/-- A `MorphismProperty C` is a class of morphisms between objects in `C`. -/
def MorphismProperty :=
  ∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop
Morphism Property in a Category
Informal description
A `MorphismProperty` in a category `C` is a predicate that assigns to each morphism `f : X ⟶ Y` between objects `X` and `Y` in `C` a proposition indicating whether `f` satisfies the property.
CategoryTheory.instCompleteBooleanAlgebraMorphismProperty instance
: CompleteBooleanAlgebra (MorphismProperty C)
Full source 
instance : CompleteBooleanAlgebra (MorphismProperty C) where
  le P₁ P₂ := ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P₁ f → P₂ f
  __ := inferInstanceAs (CompleteBooleanAlgebra (∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop))
Complete Boolean Algebra Structure on Morphism Properties
Informal description
For any category $C$, the collection of morphism properties in $C$ forms a complete Boolean algebra. This means that for any family of morphism properties, there exist a greatest lower bound (infimum) and a least upper bound (supremum) with respect to the partial order defined by inclusion of properties, and these operations satisfy the axioms of a complete Boolean algebra.
CategoryTheory.MorphismProperty.le_def theorem
{P Q : MorphismProperty C} : P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f
Full source 
lemma MorphismProperty.le_def {P Q : MorphismProperty C} :
    P ≤ Q ↔ ∀ {X Y : C} (f : X ⟶ Y), P f → Q f := Iff.rfl
Order Relation on Morphism Properties: $P \leq Q$ iff $P(f) \implies Q(f)$ for all $f$
Informal description
For any two morphism properties $P$ and $Q$ in a category $C$, the property $P$ is less than or equal to $Q$ if and only if for all objects $X$ and $Y$ in $C$ and any morphism $f : X \to Y$, if $P(f)$ holds then $Q(f)$ also holds.
CategoryTheory.instInhabitedMorphismProperty instance
: Inhabited (MorphismProperty C)
Full source 
instance : Inhabited (MorphismProperty C) :=
  ⟨⊤⟩
Existence of a Morphism Property in a Category
Informal description
For any category $C$, the collection of morphism properties in $C$ is inhabited. That is, there exists at least one morphism property defined on $C$.
CategoryTheory.MorphismProperty.top_eq theorem
: (⊤ : MorphismProperty C) = fun _ _ _ => True
Full source 
lemma MorphismProperty.top_eq : (⊤ : MorphismProperty C) = fun _ _ _ => True := rfl
Top Morphism Property is the Trivially True Property
Informal description
The top morphism property $\top$ in a category $C$ is equal to the constant function that always returns `True`, i.e., for any objects $X, Y$ and any morphism $f : X \to Y$, $\top(f)$ holds.
CategoryTheory.MorphismProperty.ext theorem
(W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) : W = W'
Full source 
@[ext]
lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) :
    W = W' := by
  funext X Y f
  rw [h]
Extensionality of Morphism Properties
Informal description
Let $W$ and $W'$ be two morphism properties in a category $C$. If for all objects $X, Y$ in $C$ and every morphism $f : X \to Y$, we have $W(f) \leftrightarrow W'(f)$, then $W = W'$.
CategoryTheory.MorphismProperty.top_apply theorem
{X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f
Full source 
@[simp]
lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by
  simp only [top_eq]
Every Morphism Satisfies the Top Property
Informal description
For any objects $X$ and $Y$ in a category $C$ and any morphism $f : X \to Y$, the top morphism property $\top$ holds for $f$.
CategoryTheory.MorphismProperty.of_eq_top theorem
{P : MorphismProperty C} (h : P = ⊤) {X Y : C} (f : X ⟶ Y) : P f
Full source 
lemma of_eq_top {P : MorphismProperty C} (h : P = ⊤) {X Y : C} (f : X ⟶ Y) : P f := by
  simp [h]
Top Morphism Property Implies All Morphisms Satisfy It
Informal description
For any morphism property $P$ in a category $C$, if $P$ is equal to the top morphism property $\top$, then for any objects $X$ and $Y$ in $C$ and any morphism $f : X \to Y$, the property $P$ holds for $f$.
CategoryTheory.MorphismProperty.sSup_iff theorem
(S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) : sSup S f ↔ ∃ (W : S), W.1 f
Full source 
@[simp]
lemma sSup_iff (S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) :
    sSupsSup S f ↔ ∃ (W : S), W.1 f := by
  dsimp [sSup, iSup]
  constructor
  · rintro ⟨_, ⟨⟨_, ⟨⟨_, ⟨_, h⟩, rfl⟩, rfl⟩⟩, rfl⟩, hf⟩
    exact ⟨⟨_, h⟩, hf⟩
  · rintro ⟨⟨W, hW⟩, hf⟩
    exact ⟨_, ⟨⟨_, ⟨_, ⟨⟨W, hW⟩, rfl⟩⟩, rfl⟩, rfl⟩, hf⟩
Supremum of Morphism Properties Characterization
Informal description
For any set $S$ of morphism properties in a category $C$ and any morphism $f : X \to Y$ in $C$, the supremum of $S$ holds for $f$ if and only if there exists a morphism property $W \in S$ such that $W(f)$ holds.
CategoryTheory.MorphismProperty.iSup_iff theorem
{ι : Sort*} (W : ι → MorphismProperty C) {X Y : C} (f : X ⟶ Y) : iSup W f ↔ ∃ i, W i f
Full source 
@[simp]
lemma iSup_iff {ι : Sort*} (W : ι → MorphismProperty C) {X Y : C} (f : X ⟶ Y) :
    iSupiSup W f ↔ ∃ i, W i f := by
  apply (sSup_iff (Set.range W) f).trans
  constructor
  · rintro ⟨⟨_, i, rfl⟩, hf⟩
    exact ⟨i, hf⟩
  · rintro ⟨i, hf⟩
    exact ⟨⟨_, i, rfl⟩, hf⟩
Characterization of Supremum of Morphism Properties
Informal description
For any family of morphism properties $(W_i)_{i \in \iota}$ in a category $C$ and any morphism $f \colon X \to Y$ in $C$, the supremum $\bigsqcup_i W_i$ holds for $f$ if and only if there exists an index $i \in \iota$ such that $W_i(f)$ holds.
CategoryTheory.MorphismProperty.op definition
(P : MorphismProperty C) : MorphismProperty Cᵒᵖ
Full source 
/-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C` -/
@[simp]
def op (P : MorphismProperty C) : MorphismProperty Cᵒᵖ := fun _ _ f => P f.unop
Opposite morphism property
Informal description
Given a morphism property $P$ in a category $C$, the morphism property $P^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ is defined such that for any morphism $f : X \to Y$ in $C^{\mathrm{op}}$ (which corresponds to a morphism $f^{\mathrm{unop}} : Y \to X$ in $C$), $P^{\mathrm{op}}(f)$ holds if and only if $P(f^{\mathrm{unop}})$ holds in $C$.
CategoryTheory.MorphismProperty.unop definition
(P : MorphismProperty Cᵒᵖ) : MorphismProperty C
Full source 
/-- The morphism property in `C` associated to a morphism property in `Cᵒᵖ` -/
@[simp]
def unop (P : MorphismProperty Cᵒᵖ) : MorphismProperty C := fun _ _ f => P f.op
Morphism property in the original category induced from the opposite category
Informal description
Given a morphism property $P$ in the opposite category $C^{\mathrm{op}}$, the morphism property `unop P` in the original category $C$ is defined such that for any morphism $f : X \to Y$ in $C$, `unop P f` holds if and only if $P$ holds for the corresponding morphism $f^{\mathrm{op}} : Y \to X$ in $C^{\mathrm{op}}$.
CategoryTheory.MorphismProperty.unop_op theorem
(P : MorphismProperty C) : P.op.unop = P
Full source 
theorem unop_op (P : MorphismProperty C) : P.op.unop = P :=
  rfl
Unopposite of Opposite Morphism Property Equals Original Property
Informal description
For any morphism property $P$ in a category $C$, the unopposite of the opposite of $P$ is equal to $P$ itself, i.e., $(P^{\mathrm{op}})^{\mathrm{unop}} = P$.
CategoryTheory.MorphismProperty.op_unop theorem
(P : MorphismProperty Cᵒᵖ) : P.unop.op = P
Full source 
theorem op_unop (P : MorphismProperty Cᵒᵖ) : P.unop.op = P :=
  rfl
Opposite and Unopposite Morphism Property Identity: $(P^{\mathrm{unop}})^{\mathrm{op}} = P$
Informal description
For any morphism property $P$ in the opposite category $C^{\mathrm{op}}$, the opposite of the unopposite of $P$ is equal to $P$ itself, i.e., $(P^{\mathrm{unop}})^{\mathrm{op}} = P$.
CategoryTheory.MorphismProperty.inverseImage definition
(P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C
Full source 
/-- The inverse image of a `MorphismProperty D` by a functor `C ⥤ D` -/
def inverseImage (P : MorphismProperty D) (F : C ⥤ D) : MorphismProperty C := fun _ _ f =>
  P (F.map f)
Inverse image of a morphism property under a functor
Informal description
Given a morphism property \( P \) in a category \( D \) and a functor \( F : C \to D \), the inverse image of \( P \) under \( F \) is the morphism property in \( C \) defined by: a morphism \( f : X \to Y \) in \( C \) satisfies the inverse image property if and only if its image \( F(f) \) under \( F \) satisfies \( P \) in \( D \).
CategoryTheory.MorphismProperty.inverseImage_iff theorem
(P : MorphismProperty D) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) : P.inverseImage F f ↔ P (F.map f)
Full source 
@[simp]
lemma inverseImage_iff (P : MorphismProperty D) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
    P.inverseImage F f ↔ P (F.map f) := by rfl
Characterization of Inverse Image of Morphism Property under Functor
Informal description
For any morphism property $P$ in a category $D$, a functor $F : C \to D$, and a morphism $f : X \to Y$ in $C$, the morphism $f$ satisfies the inverse image property $P.\mathrm{inverseImage}\,F$ if and only if its image $F(f)$ under $F$ satisfies $P$ in $D$.
CategoryTheory.MorphismProperty.map definition
(P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D
Full source 
/-- The image (up to isomorphisms) of a `MorphismProperty C` by a functor `C ⥤ D` -/
def map (P : MorphismProperty C) (F : C ⥤ D) : MorphismProperty D := fun _ _ f =>
  ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : P f'), Nonempty (Arrow.mk (F.map f') ≅ Arrow.mk f)
Image of a morphism property under a functor
Informal description
Given a morphism property \( P \) in a category \( C \) and a functor \( F : C \to D \), the image of \( P \) under \( F \) is the morphism property in \( D \) defined as follows: a morphism \( f : X \to Y \) in \( D \) satisfies the image property if and only if there exist objects \( X' \) and \( Y' \) in \( C \), a morphism \( f' : X' \to Y' \) in \( C \) satisfying \( P \), and an isomorphism between \( F(f') \) and \( f \) in the arrow category of \( D \).
CategoryTheory.MorphismProperty.map_mem_map theorem
(P : MorphismProperty C) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (hf : P f) : (P.map F) (F.map f)
Full source 
lemma map_mem_map (P : MorphismProperty C) (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (hf : P f) :
    (P.map F) (F.map f) := ⟨X, Y, f, hf, ⟨Iso.refl _⟩⟩
Image of a Morphism under Functor Preserves Property
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$, and let $F : \mathcal{C} \to \mathcal{D}$ be a functor. For any morphism $f : X \to Y$ in $\mathcal{C}$ satisfying $P$, the image $F(f)$ of $f$ under $F$ satisfies the image property $P.\mathrm{map}\,F$ in $\mathcal{D}$.
CategoryTheory.MorphismProperty.monotone_map theorem
(F : C ⥤ D) : Monotone (map · F)
Full source 
lemma monotone_map (F : C ⥤ D) :
    Monotone (map · F) := by
  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
Monotonicity of Morphism Property Image under Functor
Informal description
For any functor $F \colon C \to D$ between categories, the mapping operation that sends a morphism property $P$ in $C$ to its image under $F$ is monotone. That is, if $P \subseteq Q$ for morphism properties $P$ and $Q$ in $C$, then $P.\mathrm{map}\,F \subseteq Q.\mathrm{map}\,F$ in $D$.
CategoryTheory.MorphismProperty.toSet definition
: Set (Arrow C)
Full source 
/-- The set in `Set (Arrow C)` which corresponds to `P : MorphismProperty C`. -/
def toSet : Set (Arrow C) := setOf (fun f ↦ P f.hom)
Set of morphisms satisfying property P
Informal description
The set of all morphisms in the category `C` that satisfy the property `P`, represented as a subset of the type `Arrow C` (which consists of all morphisms in `C`).
CategoryTheory.MorphismProperty.homFamily definition
(f : P.toSet) : f.1.left ⟶ f.1.right
Full source 
/-- The family of morphisms indexed by `P.toSet` which corresponds
to `P : MorphismProperty C`, see `MorphismProperty.ofHoms_homFamily`. -/
def homFamily (f : P.toSet) : f.1.left ⟶ f.1.right := f.1.hom
Underlying morphism of a property-satisfying arrow
Informal description
For a given morphism property \( P \) in a category \( C \), the function `homFamily` maps each morphism \( f \) in the set of morphisms satisfying \( P \) (i.e., \( f \in P.toSet \)) to the underlying morphism \( f \) in the category \( C \). Specifically, if \( f \) is represented as an element of `Arrow C` (which consists of triples \((X, Y, f)\) where \( f : X \to Y \)), then `homFamily f` returns the morphism \( f \) itself.
CategoryTheory.MorphismProperty.homFamily_apply theorem
(f : P.toSet) : P.homFamily f = f.1.hom
Full source 
lemma homFamily_apply (f : P.toSet) : P.homFamily f = f.1.hom := rfl
Underlying Morphism of Property-Satisfying Arrow Equals Original Morphism
Informal description
For any morphism $f$ in the set of morphisms satisfying property $P$ in a category $\mathcal{C}$, the underlying morphism obtained via `homFamily` is equal to the morphism component of $f$ (i.e., $f.1.\mathrm{hom}$).
CategoryTheory.MorphismProperty.homFamily_arrow_mk theorem
{X Y : C} (f : X ⟶ Y) (hf : P f) : P.homFamily ⟨Arrow.mk f, hf⟩ = f
Full source 
@[simp]
lemma homFamily_arrow_mk {X Y : C} (f : X ⟶ Y) (hf : P f) :
    P.homFamily ⟨Arrow.mk f, hf⟩ = f := rfl
Underlying Morphism of Arrow Construction Equals Original Morphism
Informal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$ that satisfies property $P$, the underlying morphism obtained from the arrow construction $\mathrm{Arrow.mk}(f)$ (viewed as an element of $P.\mathrm{toSet}$) is equal to $f$ itself.
CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff theorem
{X Y : C} (f : X ⟶ Y) : Arrow.mk f ∈ P.toSet ↔ P f
Full source 
@[simp]
lemma arrow_mk_mem_toSet_iff {X Y : C} (f : X ⟶ Y) : Arrow.mkArrow.mk f ∈ P.toSetArrow.mk f ∈ P.toSet ↔ P f := Iff.rfl
Membership in Morphism Property Set via Arrow Construction
Informal description
For any morphism $f \colon X \to Y$ in a category $\mathcal{C}$, the arrow $\mathrm{Arrow.mk}(f)$ belongs to the set of morphisms satisfying property $P$ if and only if $f$ satisfies $P$.
CategoryTheory.MorphismProperty.of_eq theorem
{X Y : C} {f : X ⟶ Y} (hf : P f) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y') (h : f' = eqToHom hX.symm ≫ f ≫ eqToHom hY) : P f'
Full source 
lemma of_eq {X Y : C} {f : X ⟶ Y} (hf : P f)
    {X' Y' : C} {f' : X' ⟶ Y'}
    (hX : X = X') (hY : Y = Y') (h : f' = eqToHomeqToHom hX.symm ≫ f ≫ eqToHom hY) :
    P f' := by
  rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
  rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]
Preservation of Morphism Property under Isomorphism of Domain and Codomain
Informal description
Let $\mathcal{C}$ be a category and $P$ a morphism property in $\mathcal{C}$. Given a morphism $f \colon X \to Y$ satisfying $P(f)$, and morphisms $f' \colon X' \to Y'$ with $X = X'$ and $Y = Y'$ via equalities $h_X$ and $h_Y$, if $f'$ can be expressed as the composition $f' = \text{eqToHom}(h_X^{-1}) \circ f \circ \text{eqToHom}(h_Y)$, then $f'$ also satisfies $P$.
CategoryTheory.MorphismProperty.ofHoms inductive
{ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) : MorphismProperty C
Full source 
/-- The class of morphisms given by a family of morphisms `f i : X i ⟶ Y i`. -/
inductive ofHoms {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) : MorphismProperty C
  | mk (i : ι) : ofHoms f (f i)
Morphism Property from a Family of Morphisms
Informal description
Given a family of morphisms `f i : X i ⟶ Y i` indexed by `i` in some type `ι`, the `MorphismProperty.ofHoms` constructs a morphism property in a category `C` that holds for a morphism `g : A ⟶ B` if and only if there exists an index `i` such that `g` is equal to `f i` up to isomorphism (i.e., `Arrow.mk g = Arrow.mk (f i)`). In other words, this property characterizes morphisms that are members of the given family `f i`.
CategoryTheory.MorphismProperty.ofHoms_iff theorem
{ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {A B : C} (g : A ⟶ B) : ofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i)
Full source 
lemma ofHoms_iff {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {A B : C} (g : A ⟶ B) :
    ofHomsofHoms f g ↔ ∃ i, Arrow.mk g = Arrow.mk (f i) := by
  constructor
  · rintro ⟨i⟩
    exact ⟨i, rfl⟩
  · rintro ⟨i, h⟩
    rw [← (ofHoms f).arrow_mk_mem_toSet_iff, h, arrow_mk_mem_toSet_iff]
    constructor
Characterization of Morphism Property from a Family of Morphisms
Informal description
Given a family of morphisms $\{f_i \colon X_i \to Y_i\}_{i \in \iota}$ in a category $\mathcal{C}$ and a morphism $g \colon A \to B$ in $\mathcal{C}$, the morphism property `ofHoms f` holds for $g$ if and only if there exists an index $i \in \iota$ such that the arrow $\mathrm{Arrow.mk}(g)$ is equal to $\mathrm{Arrow.mk}(f_i)$.
CategoryTheory.MorphismProperty.ofHoms_homFamily theorem
(P : MorphismProperty C) : ofHoms P.homFamily = P
Full source 
@[simp]
lemma ofHoms_homFamily (P : MorphismProperty C) : ofHoms P.homFamily = P := by
  ext _ _ f
  constructor
  · intro hf
    rw [ofHoms_iff] at hf
    obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf
    exact hf
  · intro hf
    exact ⟨(⟨f, hf⟩ : P.toSet)⟩
Reconstruction of Morphism Property from Its Satisfying Morphisms
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the morphism property constructed from the family of morphisms satisfying $P$ is equal to $P$ itself. That is, $\mathrm{ofHoms}(P.\mathrm{homFamily}) = P$.
CategoryTheory.MorphismProperty.RespectsRight structure
(P Q : MorphismProperty C)
Full source 
/-- A morphism property `P` satisfies `P.RespectsRight Q` if it is stable under post-composition
with morphisms satisfying `Q`, i.e. whenever `P` holds for `f` and `Q` holds for `i` then `P`
holds for `f ≫ i`. -/
class RespectsRight (P Q : MorphismProperty C) : Prop where
  postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : Q i) (f : X ⟶ Y) (hf : P f) : P (f ≫ i)
Right respect of morphism properties under composition
Informal description
A morphism property \( P \) in a category \( C \) is said to respect a property \( Q \) on the right if \( P \) is stable under post-composition with morphisms satisfying \( Q \). That is, whenever \( P \) holds for a morphism \( f \) and \( Q \) holds for a morphism \( i \), then \( P \) also holds for the composition \( f \circ i \).
CategoryTheory.MorphismProperty.RespectsLeft structure
(P Q : MorphismProperty C)
Full source 
/-- A morphism property `P` satisfies `P.RespectsLeft Q` if it is stable under
pre-composition with morphisms satisfying `Q`, i.e. whenever `P` holds for `f`
and `Q` holds for `i` then `P` holds for `i ≫ f`. -/
class RespectsLeft (P Q : MorphismProperty C) : Prop where
  precomp {X Y Z : C} (i : X ⟶ Y) (hi : Q i) (f : Y ⟶ Z) (hf : P f) : P (i ≫ f)
Left-respect of morphism properties
Informal description
A morphism property \( P \) in a category \( C \) is said to respect another property \( Q \) on the left if for any morphism \( f \) satisfying \( P \) and any morphism \( i \) satisfying \( Q \), the composition \( i \circ f \) also satisfies \( P \). In other words, \( P \) is stable under pre-composition with morphisms that satisfy \( Q \).
CategoryTheory.MorphismProperty.Respects structure
(P Q : MorphismProperty C) : Prop extends P.RespectsLeft Q, P.RespectsRight Q
Full source 
/-- A morphism property `P` satisfies `P.Respects Q` if it is stable under composition on the
left and right by morphisms satisfying `Q`. -/
class Respects (P Q : MorphismProperty C) : Prop extends P.RespectsLeft Q, P.RespectsRight Q where
Respect of morphism properties under composition
Informal description
A morphism property \( P \) in a category \( C \) is said to *respect* another morphism property \( Q \) if \( P \) is stable under both left and right composition with morphisms satisfying \( Q \). That is: - For any morphism \( f \) satisfying \( P \) and any morphism \( i \) satisfying \( Q \), the composition \( i \circ f \) (if defined) also satisfies \( P \) (respects \( Q \) on the left). - For any morphism \( f \) satisfying \( P \) and any morphism \( i \) satisfying \( Q \), the composition \( f \circ i \) (if defined) also satisfies \( P \) (respects \( Q \) on the right).
CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight instance
(P Q : MorphismProperty C) [P.RespectsLeft Q] [P.RespectsRight Q] : P.Respects Q
Full source 
instance (P Q : MorphismProperty C) [P.RespectsLeft Q] [P.RespectsRight Q] : P.Respects Q where
Respect of Morphism Properties from Left and Right Respect
Informal description
For any two morphism properties \( P \) and \( Q \) in a category \( C \), if \( P \) respects \( Q \) both on the left and on the right, then \( P \) respects \( Q \).
CategoryTheory.MorphismProperty.instRespectsRightOppositeOpOfRespectsLeft instance
(P Q : MorphismProperty C) [P.RespectsLeft Q] : P.op.RespectsRight Q.op
Full source 
instance (P Q : MorphismProperty C) [P.RespectsLeft Q] : P.op.RespectsRight Q.op where
  postcomp i hi f hf := RespectsLeft.precomp (Q := Q) i.unop hi f.unop hf
Opposite of Left-Respect Implies Right-Respect in Opposite Category
Informal description
For any morphism properties $P$ and $Q$ in a category $C$, if $P$ respects $Q$ on the left, then the opposite property $P^{\mathrm{op}}$ respects $Q^{\mathrm{op}}$ on the right in the opposite category $C^{\mathrm{op}}$. That is, for any morphism $f$ in $C^{\mathrm{op}}$ satisfying $P^{\mathrm{op}}$ and any morphism $i$ in $C^{\mathrm{op}}$ satisfying $Q^{\mathrm{op}}$, the composition $f \circ i$ in $C^{\mathrm{op}}$ also satisfies $P^{\mathrm{op}}$.
CategoryTheory.MorphismProperty.instRespectsLeftOppositeOpOfRespectsRight instance
(P Q : MorphismProperty C) [P.RespectsRight Q] : P.op.RespectsLeft Q.op
Full source 
instance (P Q : MorphismProperty C) [P.RespectsRight Q] : P.op.RespectsLeft Q.op where
  precomp i hi f hf := RespectsRight.postcomp (Q := Q) i.unop hi f.unop hf
Opposite of Right-Respect Implies Left-Respect in Opposite Category
Informal description
For any morphism properties $P$ and $Q$ in a category $C$, if $P$ respects $Q$ on the right, then the opposite property $P^{\mathrm{op}}$ respects $Q^{\mathrm{op}}$ on the left in the opposite category $C^{\mathrm{op}}$. That is, for any morphism $f$ in $C^{\mathrm{op}}$ satisfying $P^{\mathrm{op}}$ and any morphism $i$ in $C^{\mathrm{op}}$ satisfying $Q^{\mathrm{op}}$, the composition $i \circ f$ in $C^{\mathrm{op}}$ also satisfies $P^{\mathrm{op}}$.
CategoryTheory.MorphismProperty.RespectsLeft.inf instance
(P₁ P₂ Q : MorphismProperty C) [P₁.RespectsLeft Q] [P₂.RespectsLeft Q] : (P₁ ⊓ P₂).RespectsLeft Q
Full source 
instance RespectsLeft.inf (P₁ P₂ Q : MorphismProperty C) [P₁.RespectsLeft Q]
    [P₂.RespectsLeft Q] : (P₁ ⊓ P₂).RespectsLeft Q where
  precomp i hi f hf := ⟨precomp i hi f hf.left, precomp i hi f hf.right⟩
Infimum of Left-Respecting Properties Respects Left
Informal description
For any two morphism properties \( P_1 \) and \( P_2 \) in a category \( C \), if both \( P_1 \) and \( P_2 \) respect a property \( Q \) on the left, then their infimum \( P_1 \sqcap P_2 \) also respects \( Q \) on the left. This means that for any morphism \( f \) satisfying both \( P_1 \) and \( P_2 \), and any morphism \( i \) satisfying \( Q \), the composition \( i \circ f \) satisfies both \( P_1 \) and \( P_2 \).
CategoryTheory.MorphismProperty.RespectsRight.inf instance
(P₁ P₂ Q : MorphismProperty C) [P₁.RespectsRight Q] [P₂.RespectsRight Q] : (P₁ ⊓ P₂).RespectsRight Q
Full source 
instance RespectsRight.inf (P₁ P₂ Q : MorphismProperty C) [P₁.RespectsRight Q]
    [P₂.RespectsRight Q] : (P₁ ⊓ P₂).RespectsRight Q where
  postcomp i hi f hf := ⟨postcomp i hi f hf.left, postcomp i hi f hf.right⟩
Infimum of Right-Respecting Properties Respects Right
Informal description
For any two morphism properties \( P_1 \) and \( P_2 \) in a category \( C \), if both \( P_1 \) and \( P_2 \) respect a property \( Q \) on the right, then their infimum \( P_1 \sqcap P_2 \) also respects \( Q \) on the right. This means that for any morphism \( f \) satisfying both \( P_1 \) and \( P_2 \), and any morphism \( i \) satisfying \( Q \), the composition \( f \circ i \) satisfies both \( P_1 \) and \( P_2 \).
CategoryTheory.MorphismProperty.isomorphisms definition
: MorphismProperty C
Full source 
/-- The `MorphismProperty C` satisfied by isomorphisms in `C`. -/
def isomorphisms : MorphismProperty C := fun _ _ f => IsIso f
Isomorphism property in a category
Informal description
The morphism property `isomorphisms` in a category `C` is defined as the property that holds for a morphism \( f : X \to Y \) if and only if \( f \) is an isomorphism, i.e., there exists an inverse morphism \( f^{-1} : Y \to X \) such that \( f \circ f^{-1} = \text{id}_X \) and \( f^{-1} \circ f = \text{id}_Y \).
CategoryTheory.MorphismProperty.monomorphisms definition
: MorphismProperty C
Full source 
/-- The `MorphismProperty C` satisfied by monomorphisms in `C`. -/
def monomorphisms : MorphismProperty C := fun _ _ f => Mono f
Monomorphism property in a category
Informal description
The property that a morphism \( f : X \longrightarrow Y \) in a category \( C \) is a monomorphism, i.e., for any pair of morphisms \( g, h : Z \longrightarrow X \), if \( f \circ g = f \circ h \), then \( g = h \).
CategoryTheory.MorphismProperty.epimorphisms definition
: MorphismProperty C
Full source 
/-- The `MorphismProperty C` satisfied by epimorphisms in `C`. -/
def epimorphisms : MorphismProperty C := fun _ _ f => Epi f
Epimorphism Property in a Category
Informal description
The `MorphismProperty` in a category `C` that is satisfied by epimorphisms, i.e., morphisms `f : X ⟶ Y` such that for any two morphisms `g₁ g₂ : Y ⟶ Z`, if `f ≫ g₁ = f ≫ g₂`, then `g₁ = g₂`.
CategoryTheory.MorphismProperty.RespectsIso abbrev
(P : MorphismProperty C) : Prop
Full source 
/-- `P` respects isomorphisms, if it respects the morphism property `isomorphisms C`, i.e.
it is stable under pre- and postcomposition with isomorphisms. -/
abbrev RespectsIso (P : MorphismProperty C) : Prop := P.Respects (isomorphisms C)
Respect for Isomorphisms of Morphism Properties
Informal description
A morphism property $P$ in a category $C$ is said to *respect isomorphisms* if it is stable under both precomposition and postcomposition with isomorphisms. That is: - For any isomorphism $e: X \xrightarrow{\sim} Y$ and any morphism $f: Y \to Z$ satisfying $P(f)$, the composition $e \circ f$ also satisfies $P$. - For any isomorphism $e: Y \xrightarrow{\sim} Z$ and any morphism $f: X \to Y$ satisfying $P(f)$, the composition $f \circ e$ also satisfies $P$.
CategoryTheory.MorphismProperty.RespectsIso.mk theorem
(P : MorphismProperty C) (hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z) (_ : P f), P (e.hom ≫ f)) (hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y) (_ : P f), P (f ≫ e.hom)) : P.RespectsIso
Full source 
lemma RespectsIso.mk (P : MorphismProperty C)
    (hprecomp : ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z) (_ : P f), P (e.hom ≫ f))
    (hpostcomp : ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y) (_ : P f), P (f ≫ e.hom)) :
    P.RespectsIso where
  precomp e (_ : IsIso e) f hf := hprecomp (asIso e) f hf
  postcomp e (_ : IsIso e) f hf := hpostcomp (asIso e) f hf
Construction of Respect for Isomorphisms in Morphism Properties
Informal description
A morphism property $P$ in a category $\mathcal{C}$ respects isomorphisms if it satisfies the following two conditions: 1. For any isomorphism $e: X \xrightarrow{\sim} Y$ and any morphism $f: Y \to Z$ such that $P(f)$ holds, the composition $e \circ f$ also satisfies $P$. 2. For any isomorphism $e: Y \xrightarrow{\sim} Z$ and any morphism $f: X \to Y$ such that $P(f)$ holds, the composition $f \circ e$ also satisfies $P$.
CategoryTheory.MorphismProperty.RespectsIso.precomp theorem
(P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : X ⟶ Y) [IsIso e] (f : Y ⟶ Z) (hf : P f) : P (e ≫ f)
Full source 
lemma RespectsIso.precomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : X ⟶ Y)
    [IsIso e] (f : Y ⟶ Z) (hf : P f) : P (e ≫ f) :=
  RespectsLeft.precomp (Q := isomorphisms C) e ‹IsIso e› f hf
Precomposition with Isomorphism Preserves Morphism Property
Informal description
Let $P$ be a morphism property in a category $C$ that respects isomorphisms. For any isomorphism $e : X \to Y$ and any morphism $f : Y \to Z$ satisfying $P(f)$, the composition $e \circ f$ also satisfies $P$.
CategoryTheory.MorphismProperty.instRespectsIsoTop instance
: RespectsIso (⊤ : MorphismProperty C)
Full source 
instance : RespectsIso (⊤ : MorphismProperty C) where
  precomp _ _ _ _ := trivial
  postcomp _ _ _ _ := trivial
Top Morphism Property Respects Isomorphisms
Informal description
The top morphism property in a category $C$, which holds for all morphisms, respects isomorphisms. That is, precomposition or postcomposition with an isomorphism preserves the property of being in the top morphism property.
CategoryTheory.MorphismProperty.RespectsIso.postcomp theorem
(P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y ⟶ Z) [IsIso e] (f : X ⟶ Y) (hf : P f) : P (f ≫ e)
Full source 
lemma RespectsIso.postcomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y ⟶ Z)
    [IsIso e] (f : X ⟶ Y) (hf : P f) : P (f ≫ e) :=
  RespectsRight.postcomp (Q := isomorphisms C) e ‹IsIso e› f hf
Postcomposition with Isomorphism Preserves Morphism Property
Informal description
Let $P$ be a morphism property in a category $C$ that respects isomorphisms. For any isomorphism $e : Y \to Z$ and any morphism $f : X \to Y$ satisfying $P(f)$, the composition $f \circ e$ also satisfies $P$.
CategoryTheory.MorphismProperty.RespectsIso.op instance
(P : MorphismProperty C) [RespectsIso P] : RespectsIso P.op
Full source 
instance RespectsIso.op (P : MorphismProperty C) [RespectsIso P] : RespectsIso P.op where
  precomp e (_ : IsIso e) f hf := postcomp P e.unop f.unop hf
  postcomp e (_ : IsIso e) f hf := precomp P e.unop f.unop hf
Opposite of an Isomorphism-Respecting Property Respects Isomorphisms
Informal description
For any morphism property $P$ in a category $C$ that respects isomorphisms, the opposite property $P^{\mathrm{op}}$ in the opposite category $C^{\mathrm{op}}$ also respects isomorphisms.
CategoryTheory.MorphismProperty.RespectsIso.unop instance
(P : MorphismProperty Cᵒᵖ) [RespectsIso P] : RespectsIso P.unop
Full source 
instance RespectsIso.unop (P : MorphismProperty Cᵒᵖ) [RespectsIso P] : RespectsIso P.unop where
  precomp e (_ : IsIso e) f hf := postcomp P e.op f.op hf
  postcomp e (_ : IsIso e) f hf := precomp P e.op f.op hf
Isomorphism Respect for the Induced Morphism Property from the Opposite Category
Informal description
For any morphism property $P$ in the opposite category $C^{\mathrm{op}}$ that respects isomorphisms, the induced morphism property $\mathrm{unop}\, P$ in the original category $C$ also respects isomorphisms. This means that $\mathrm{unop}\, P$ is stable under both precomposition and postcomposition with isomorphisms in $C$.
CategoryTheory.MorphismProperty.isoClosure definition
(P : MorphismProperty C) : MorphismProperty C
Full source 
/-- The closure by isomorphisms of a `MorphismProperty` -/
def isoClosure (P : MorphismProperty C) : MorphismProperty C :=
  fun _ _ f => ∃ (Y₁ Y₂ : C) (f' : Y₁ ⟶ Y₂) (_ : P f'), Nonempty (Arrow.mk f' ≅ Arrow.mk f)
Isomorphism closure of a morphism property
Informal description
The *isomorphism closure* of a morphism property $P$ in a category $\mathcal{C}$ is the smallest morphism property containing $P$ that is closed under isomorphisms. Specifically, a morphism $f : X \to Y$ is in the isomorphism closure of $P$ if there exist objects $Y_1, Y_2$ in $\mathcal{C}$ and a morphism $f' : Y_1 \to Y_2$ such that $P(f')$ holds and there exists an isomorphism between the arrows $\text{Arrow.mk}(f')$ and $\text{Arrow.mk}(f)$.
CategoryTheory.MorphismProperty.le_isoClosure theorem
(P : MorphismProperty C) : P ≤ P.isoClosure
Full source 
lemma le_isoClosure (P : MorphismProperty C) : P ≤ P.isoClosure :=
  fun _ _ f hf => ⟨_, _, f, hf, ⟨Iso.refl _⟩⟩
Inclusion of Morphism Property in its Isomorphism Closure
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the property $P$ is contained in its isomorphism closure, i.e., $P \subseteq P.\text{isoClosure}$.
CategoryTheory.MorphismProperty.isoClosure_respectsIso instance
(P : MorphismProperty C) : RespectsIso P.isoClosure
Full source 
instance isoClosure_respectsIso (P : MorphismProperty C) :
    RespectsIso P.isoClosure where
  precomp := fun e (he : IsIso e) f ⟨_, _, f', hf', ⟨iso⟩⟩ => ⟨_, _, f', hf',
      ⟨Arrow.isoMk (asIso iso.hom.left ≪≫ asIso (inv e)) (asIso iso.hom.right) (by simp)⟩⟩
  postcomp := fun e (he : IsIso e) f ⟨_, _, f', hf', ⟨iso⟩⟩ => ⟨_, _, f', hf',
      ⟨Arrow.isoMk (asIso iso.hom.left) (asIso iso.hom.right ≪≫ asIso e) (by simp)⟩⟩
Isomorphism Closure Respects Isomorphisms
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the isomorphism closure of $P$ respects isomorphisms. That is, the property $P.\text{isoClosure}$ is stable under both precomposition and postcomposition with isomorphisms.
CategoryTheory.MorphismProperty.monotone_isoClosure theorem
: Monotone (isoClosure (C := C))
Full source 
lemma monotone_isoClosure : Monotone (isoClosure (C := C)) := by
  intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
Monotonicity of Isomorphism Closure for Morphism Properties
Informal description
The isomorphism closure operation on morphism properties in a category $\mathcal{C}$ is monotone. That is, for any two morphism properties $P$ and $Q$ in $\mathcal{C}$, if $P \leq Q$ (meaning $P(f)$ implies $Q(f)$ for all morphisms $f$), then the isomorphism closure of $P$ is less than or equal to the isomorphism closure of $Q$.
CategoryTheory.MorphismProperty.cancel_left_of_respectsIso theorem
(P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g
Full source 
theorem cancel_left_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g :=
  ⟨fun h => by simpa using RespectsIso.precomp P (inv f) (f ≫ g) h, RespectsIso.precomp P f g⟩
Cancellation of Isomorphism on the Left for Morphism Properties: $P(f \circ g) \leftrightarrow P(g)$ when $f$ is an isomorphism
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms. For any isomorphism $f : X \to Y$ and any morphism $g : Y \to Z$, the composition $f \circ g$ satisfies $P$ if and only if $g$ satisfies $P$.
CategoryTheory.MorphismProperty.cancel_right_of_respectsIso theorem
(P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f
Full source 
theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f :=
  ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩
Right Cancellation of Morphism Property with Respect to Isomorphisms
Informal description
Let $P$ be a morphism property in a category $C$ that respects isomorphisms. For any morphisms $f : X \to Y$ and $g : Y \to Z$ in $C$, if $g$ is an isomorphism, then $P(f \circ g)$ holds if and only if $P(f)$ holds.
CategoryTheory.MorphismProperty.comma_iso_iff theorem
(P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B] {L : A ⥤ C} {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) : P f.hom ↔ P g.hom
Full source 
lemma comma_iso_iff (P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B]
    {L : A ⥤ C} {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) :
    P f.hom ↔ P g.hom := by
  simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]
Isomorphism Invariance of Morphism Properties in Comma Categories: $P(f_{\text{hom}}) \leftrightarrow P(g_{\text{hom}})$ for $f \cong g$
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms. Given two objects $f$ and $g$ in the comma category $\text{Comma}(L, R)$ (where $L \colon \mathcal{A} \to \mathcal{C}$ and $R \colon \mathcal{B} \to \mathcal{C}$ are functors), if $f$ and $g$ are isomorphic (i.e., there exists an isomorphism $e \colon f \cong g$), then $P$ holds for the morphism $f_{\text{hom}}$ if and only if $P$ holds for the morphism $g_{\text{hom}}$.
CategoryTheory.MorphismProperty.arrow_iso_iff theorem
(P : MorphismProperty C) [RespectsIso P] {f g : Arrow C} (e : f ≅ g) : P f.hom ↔ P g.hom
Full source 
theorem arrow_iso_iff (P : MorphismProperty C) [RespectsIso P] {f g : Arrow C}
    (e : f ≅ g) : P f.hom ↔ P g.hom :=
  P.comma_iso_iff e
Isomorphism Invariance of Morphism Properties in the Arrow Category: $P(f_{\text{hom}}) \leftrightarrow P(g_{\text{hom}})$ for $f \cong g$
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms. For any two objects $f$ and $g$ in the arrow category $\text{Arrow}(\mathcal{C})$, if $f$ and $g$ are isomorphic (i.e., there exists an isomorphism $e : f \cong g$), then $P$ holds for the morphism $f_{\text{hom}}$ if and only if $P$ holds for the morphism $g_{\text{hom}}$.
CategoryTheory.MorphismProperty.arrow_mk_iso_iff theorem
(P : MorphismProperty C) [RespectsIso P] {W X Y Z : C} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g
Full source 
theorem arrow_mk_iso_iff (P : MorphismProperty C) [RespectsIso P] {W X Y Z : C}
    {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mkArrow.mk f ≅ Arrow.mk g) : P f ↔ P g :=
  P.arrow_iso_iff e
Isomorphism Invariance of Morphism Properties via Arrow Construction: $P(f) \leftrightarrow P(g)$ for $\text{Arrow.mk}(f) \cong \text{Arrow.mk}(g)$
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms. For any morphisms $f \colon W \to X$ and $g \colon Y \to Z$ in $\mathcal{C}$, if there exists an isomorphism $e$ between the corresponding objects $\text{Arrow.mk}(f)$ and $\text{Arrow.mk}(g)$ in the arrow category, then $P(f)$ holds if and only if $P(g)$ holds.
CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso theorem
(P : MorphismProperty C) (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) : RespectsIso P
Full source 
theorem RespectsIso.of_respects_arrow_iso (P : MorphismProperty C)
    (hP : ∀ (f g : Arrow C) (_ : f ≅ g) (_ : P f.hom), P g.hom) : RespectsIso P where
  precomp {X Y Z} e (he : IsIso e) f hf := by
    refine hP (Arrow.mk f) (Arrow.mk (e ≫ f)) (Arrow.isoMk (asIso (inv e)) (Iso.refl _) ?_) hf
    simp
  postcomp {X Y Z} e (he : IsIso e) f hf := by
    refine hP (Arrow.mk f) (Arrow.mk (f ≫ e)) (Arrow.isoMk (Iso.refl _) (asIso e) ?_) hf
    simp
Respect for Isomorphisms via Arrow Category Isomorphisms
Informal description
A morphism property $P$ in a category $\mathcal{C}$ respects isomorphisms if, for any two morphisms $f$ and $g$ represented as objects in the arrow category $\text{Arrow}(\mathcal{C})$, and any isomorphism $e : f \cong g$ between them, the property $P(f)$ implies $P(g)$.
CategoryTheory.MorphismProperty.isoClosure_eq_iff theorem
(P : MorphismProperty C) : P.isoClosure = P ↔ P.RespectsIso
Full source 
lemma isoClosure_eq_iff (P : MorphismProperty C) :
    P.isoClosure = P ↔ P.RespectsIso := by
  refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
  intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact (P.arrow_mk_iso_iff e).1 hf'
Isomorphism Closure Equals Original Property if and only if Property Respects Isomorphisms
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the isomorphism closure of $P$ equals $P$ if and only if $P$ respects isomorphisms. That is, $P.\text{isoClosure} = P$ holds precisely when $P$ is stable under both precomposition and postcomposition with isomorphisms.
CategoryTheory.MorphismProperty.isoClosure_eq_self theorem
(P : MorphismProperty C) [P.RespectsIso] : P.isoClosure = P
Full source 
lemma isoClosure_eq_self (P : MorphismProperty C) [P.RespectsIso] :
    P.isoClosure = P := by rwa [isoClosure_eq_iff]
Isomorphism Closure of a Respecting-Iso Property Equals Itself
Informal description
For any morphism property $P$ in a category $\mathcal{C}$ that respects isomorphisms, the isomorphism closure of $P$ is equal to $P$ itself.
CategoryTheory.MorphismProperty.isoClosure_isoClosure theorem
(P : MorphismProperty C) : P.isoClosure.isoClosure = P.isoClosure
Full source 
@[simp]
lemma isoClosure_isoClosure (P : MorphismProperty C) :
    P.isoClosure.isoClosure = P.isoClosure :=
  P.isoClosure.isoClosure_eq_self
Idempotence of Isomorphism Closure for Morphism Properties
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the isomorphism closure of the isomorphism closure of $P$ is equal to the isomorphism closure of $P$. That is, $(P.\text{isoClosure}).\text{isoClosure} = P.\text{isoClosure}$.
CategoryTheory.MorphismProperty.isoClosure_le_iff theorem
(P Q : MorphismProperty C) [Q.RespectsIso] : P.isoClosure ≤ Q ↔ P ≤ Q
Full source 
lemma isoClosure_le_iff (P Q : MorphismProperty C) [Q.RespectsIso] :
    P.isoClosure ≤ Q ↔ P ≤ Q := by
  constructor
  · exact P.le_isoClosure.trans
  · intro h
    exact (monotone_isoClosure h).trans (by rw [Q.isoClosure_eq_self])
Isomorphism Closure Containment Criterion for Morphism Properties
Informal description
For any morphism properties $P$ and $Q$ in a category $\mathcal{C}$, where $Q$ respects isomorphisms, the isomorphism closure of $P$ is contained in $Q$ if and only if $P$ itself is contained in $Q$. In symbols: \[ \overline{P} \leq Q \leftrightarrow P \leq Q \] where $\overline{P}$ denotes the isomorphism closure of $P$.
CategoryTheory.MorphismProperty.map_respectsIso instance
(P : MorphismProperty C) (F : C ⥤ D) : (P.map F).RespectsIso
Full source 
instance map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) :
    (P.map F).RespectsIso := by
  apply RespectsIso.of_respects_arrow_iso
  intro f g e ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨e' ≪≫ e⟩⟩
Image of a Morphism Property Respects Isomorphisms
Informal description
For any morphism property $P$ in a category $\mathcal{C}$ and any functor $F \colon \mathcal{C} \to \mathcal{D}$, the image of $P$ under $F$ respects isomorphisms in $\mathcal{D}$. That is, if a morphism $f$ in $\mathcal{D}$ satisfies $P.map(F)$, then any morphism isomorphic to $f$ (via pre- or post-composition with an isomorphism) also satisfies $P.map(F)$.
CategoryTheory.MorphismProperty.map_le_iff theorem
(P : MorphismProperty C) {F : C ⥤ D} (Q : MorphismProperty D) [RespectsIso Q] : P.map F ≤ Q ↔ P ≤ Q.inverseImage F
Full source 
lemma map_le_iff (P : MorphismProperty C) {F : C ⥤ D} (Q : MorphismProperty D)
    [RespectsIso Q] :
    P.map F ≤ Q ↔ P ≤ Q.inverseImage F := by
  constructor
  · intro h X Y f hf
    exact h (F.map f) (map_mem_map P F f hf)
  · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact (Q.arrow_mk_iso_iff e).1 (h _ hf')
Image and Inverse Image Comparison for Morphism Properties: $P.\mathrm{map}\,F \leq Q \leftrightarrow P \leq Q.\mathrm{inverseImage}\,F$
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$, $F \colon \mathcal{C} \to \mathcal{D}$ a functor, and $Q$ a morphism property in $\mathcal{D}$ that respects isomorphisms. Then the image of $P$ under $F$ is contained in $Q$ if and only if $P$ is contained in the inverse image of $Q$ under $F$. In symbols: \[ P.\mathrm{map}\,F \leq Q \leftrightarrow P \leq Q.\mathrm{inverseImage}\,F \]
CategoryTheory.MorphismProperty.map_isoClosure theorem
(P : MorphismProperty C) (F : C ⥤ D) : P.isoClosure.map F = P.map F
Full source 
@[simp]
lemma map_isoClosure (P : MorphismProperty C) (F : C ⥤ D) :
    P.isoClosure.map F = P.map F := by
  apply le_antisymm
  · rw [map_le_iff]
    intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact ⟨_, _, f', hf', ⟨F.mapArrow.mapIso e⟩⟩
  · exact monotone_map _ (le_isoClosure P)
Image of Isomorphism Closure Equals Image of Property
Informal description
For any morphism property $P$ in a category $\mathcal{C}$ and any functor $F \colon \mathcal{C} \to \mathcal{D}$, the image under $F$ of the isomorphism closure of $P$ is equal to the image of $P$ under $F$. In symbols: \[ (P.\mathrm{isoClosure}).\mathrm{map}\,F = P.\mathrm{map}\,F \]
CategoryTheory.MorphismProperty.map_id_eq_isoClosure theorem
(P : MorphismProperty C) : P.map (𝟭 _) = P.isoClosure
Full source 
lemma map_id_eq_isoClosure (P : MorphismProperty C) :
    P.map (𝟭 _) = P.isoClosure := by
  apply le_antisymm
  · rw [map_le_iff]
    intro X Y f hf
    exact P.le_isoClosure _ hf
  · intro X Y f hf
    exact hf
Image under Identity Functor Equals Isomorphism Closure
Informal description
For any morphism property $P$ in a category $\mathcal{C}$, the image of $P$ under the identity functor $\mathrm{id}_\mathcal{C}$ is equal to the isomorphism closure of $P$. In other words, $P.\mathrm{map}(\mathrm{id}_\mathcal{C}) = P.\mathrm{isoClosure}$.
CategoryTheory.MorphismProperty.map_id theorem
(P : MorphismProperty C) [RespectsIso P] : P.map (𝟭 _) = P
Full source 
lemma map_id (P : MorphismProperty C) [RespectsIso P] :
    P.map (𝟭 _) = P := by
  rw [map_id_eq_isoClosure, P.isoClosure_eq_self]
Image of Isomorphism-Respecting Property under Identity Functor Equals Itself
Informal description
For any morphism property $P$ in a category $\mathcal{C}$ that respects isomorphisms, the image of $P$ under the identity functor $\mathrm{id}_\mathcal{C}$ is equal to $P$ itself. In other words, $P.\mathrm{map}(\mathrm{id}_\mathcal{C}) = P$.
CategoryTheory.MorphismProperty.map_map theorem
(P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) : (P.map F).map G = P.map (F ⋙ G)
Full source 
@[simp]
lemma map_map (P : MorphismProperty C) (F : C ⥤ D) {E : Type*} [Category E] (G : D ⥤ E) :
    (P.map F).map G = P.map (F ⋙ G) := by
  apply le_antisymm
  · rw [map_le_iff]
    intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩
  · rw [map_le_iff]
    intro X Y f hf
    exact map_mem_map _ _ _ (map_mem_map _ _ _ hf)
Functoriality of Morphism Property Image: $(P.\mathrm{map}\,F).\mathrm{map}\,G = P.\mathrm{map}\,(F \circ G)$
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$, $F \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{E}$ be functors. Then the image of $P$ under the composition $F \circ G$ is equal to the image under $G$ of the image of $P$ under $F$. In symbols: \[ (P.\mathrm{map}\,F).\mathrm{map}\,G = P.\mathrm{map}\,(F \circ G) \]
CategoryTheory.MorphismProperty.RespectsIso.inverseImage instance
(P : MorphismProperty D) [RespectsIso P] (F : C ⥤ D) : RespectsIso (P.inverseImage F)
Full source 
instance RespectsIso.inverseImage (P : MorphismProperty D) [RespectsIso P] (F : C ⥤ D) :
    RespectsIso (P.inverseImage F) where
  precomp {X Y Z} e (he : IsIso e) f hf := by
    simpa [MorphismProperty.inverseImage, cancel_left_of_respectsIso] using hf
  postcomp {X Y Z} e (he : IsIso e) f hf := by
    simpa [MorphismProperty.inverseImage, cancel_right_of_respectsIso] using hf
Inverse Image of an Isomorphism-Respecting Property Respects Isomorphisms
Informal description
For any morphism property $P$ in a category $\mathcal{D}$ that respects isomorphisms and any functor $F : \mathcal{C} \to \mathcal{D}$, the inverse image of $P$ under $F$ also respects isomorphisms in $\mathcal{C}$.
CategoryTheory.MorphismProperty.map_eq_of_iso theorem
(P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) : P.map F = P.map G
Full source 
lemma map_eq_of_iso (P : MorphismProperty C) {F G : C ⥤ D} (e : F ≅ G) :
    P.map F = P.map G := by
  revert F G e
  suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)
  intro F G e X Y f ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨((Functor.mapArrowFunctor _ _).mapIso e.symm).app (Arrow.mk f') ≪≫ e'⟩⟩
Equality of Mapped Morphism Properties under Naturally Isomorphic Functors
Informal description
For any morphism property $P$ in a category $C$ and any pair of naturally isomorphic functors $F, G : C \to D$, the image of $P$ under $F$ is equal to the image of $P$ under $G$. That is, if $F \cong G$ via a natural isomorphism $e$, then $P.\text{map} F = P.\text{map} G$.
CategoryTheory.MorphismProperty.map_inverseImage_le theorem
(P : MorphismProperty D) (F : C ⥤ D) : (P.inverseImage F).map F ≤ P.isoClosure
Full source 
lemma map_inverseImage_le (P : MorphismProperty D) (F : C ⥤ D) :
    (P.inverseImage F).map F ≤ P.isoClosure :=
  fun _ _ _ ⟨_, _, f, hf, ⟨e⟩⟩ => ⟨_, _, F.map f, hf, ⟨e⟩⟩
Inclusion of Mapped Inverse Image in Isomorphism Closure
Informal description
For any morphism property $P$ in a category $D$ and any functor $F : C \to D$, the image of the inverse image of $P$ under $F$ is contained in the isomorphism closure of $P$. In other words, if a morphism $f$ in $D$ is in $(P.\text{inverseImage} F).\text{map} F$, then $f$ is in $P.\text{isoClosure}$.
CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor theorem
(P : MorphismProperty D) [RespectsIso P] (E : C ≌ D) : P.inverseImage E.functor = P.map E.inverse
Full source 
lemma inverseImage_equivalence_inverse_eq_map_functor
    (P : MorphismProperty D) [RespectsIso P] (E : C ≌ D) :
    P.inverseImage E.functor = P.map E.inverse := by
  apply le_antisymm
  · intro X Y f hf
    refine ⟨_, _, _, hf, ⟨?_⟩⟩
    exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)
  · rw [map_le_iff]
    intro X Y f hf
    exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf
Equivalence of Inverse Image and Image under Equivalence: $P.\text{inverseImage}\,F = P.\text{map}\,F^{-1}$ for $F \colon \mathcal{C} \simeq \mathcal{D}$
Informal description
Let $P$ be a morphism property in a category $\mathcal{D}$ that respects isomorphisms, and let $E \colon \mathcal{C} \simeq \mathcal{D}$ be an equivalence of categories. Then the inverse image of $P$ under the functor $E.functor$ is equal to the image of $P$ under the inverse functor $E.inverse$. In symbols: \[ P.\text{inverseImage}\,E.functor = P.\text{map}\,E.inverse \]
CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse theorem
(Q : MorphismProperty C) [RespectsIso Q] (E : C ≌ D) : Q.inverseImage E.inverse = Q.map E.functor
Full source 
lemma inverseImage_equivalence_functor_eq_map_inverse
    (Q : MorphismProperty C) [RespectsIso Q] (E : C ≌ D) :
    Q.inverseImage E.inverse = Q.map E.functor :=
  inverseImage_equivalence_inverse_eq_map_functor Q E.symm
Equivalence of Inverse Image and Image under Equivalence: $Q.\text{inverseImage}\,E^{-1} = Q.\text{map}\,E$
Informal description
Let $Q$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms, and let $E \colon \mathcal{C} \simeq \mathcal{D}$ be an equivalence of categories. Then the inverse image of $Q$ under the inverse functor $E^{-1}$ is equal to the image of $Q$ under the functor $E$. In symbols: \[ Q.\text{inverseImage}\,E^{-1} = Q.\text{map}\,E \]
CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence theorem
(P : MorphismProperty D) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] : (P.inverseImage F).map F = P
Full source 
lemma map_inverseImage_eq_of_isEquivalence
    (P : MorphismProperty D) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] :
    (P.inverseImage F).map F = P := by
  erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
    P.map_eq_of_iso F.asEquivalence.counitIso, map_id]
Equivalence of Image and Inverse Image for Isomorphism-Respecting Properties: $(P.F^{-1}).F = P$
Informal description
Let $P$ be a morphism property in a category $\mathcal{D}$ that respects isomorphisms, and let $F \colon \mathcal{C} \to \mathcal{D}$ be an equivalence of categories. Then the image under $F$ of the inverse image of $P$ under $F$ equals $P$ itself. In symbols: \[ (P.\text{inverseImage}\,F).\text{map}\,F = P \]
CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence theorem
(P : MorphismProperty C) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] : (P.map F).inverseImage F = P
Full source 
lemma inverseImage_map_eq_of_isEquivalence
    (P : MorphismProperty C) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] :
    (P.map F).inverseImage F = P := by
  erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
    P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]
Inverse Image of Mapped Property under Equivalence Equals Original Property
Informal description
Let $P$ be a morphism property in a category $\mathcal{C}$ that respects isomorphisms, and let $F \colon \mathcal{C} \to \mathcal{D}$ be an equivalence of categories. Then the inverse image of the image of $P$ under $F$ is equal to $P$ itself. In symbols: \[ (P.\mathrm{map}\,F).\mathrm{inverseImage}\,F = P \]
CategoryTheory.MorphismProperty.isomorphisms.iff theorem
: (isomorphisms C) f ↔ IsIso f
Full source 
@[simp]
theorem isomorphisms.iff : (isomorphisms C) f ↔ IsIso f := by rfl
Characterization of Isomorphisms via Morphism Property
Informal description
A morphism $f$ in a category $\mathcal{C}$ satisfies the isomorphism property if and only if $f$ is an isomorphism, i.e., there exists an inverse morphism $f^{-1}$ such that $f \circ f^{-1} = \text{id}$ and $f^{-1} \circ f = \text{id}$.
CategoryTheory.MorphismProperty.monomorphisms.iff theorem
: (monomorphisms C) f ↔ Mono f
Full source 
@[simp]
theorem monomorphisms.iff : (monomorphisms C) f ↔ Mono f := by rfl
Characterization of Monomorphisms via Morphism Property
Informal description
A morphism $f$ in a category $\mathcal{C}$ satisfies the monomorphism property if and only if it is a monomorphism, i.e., for any pair of morphisms $g, h : Z \to X$, if $f \circ g = f \circ h$, then $g = h$.
CategoryTheory.MorphismProperty.epimorphisms.iff theorem
: (epimorphisms C) f ↔ Epi f
Full source 
@[simp]
theorem epimorphisms.iff : (epimorphisms C) f ↔ Epi f := by rfl
Characterization of Epimorphisms via Morphism Property
Informal description
A morphism $f$ in a category $\mathcal{C}$ satisfies the epimorphism property if and only if $f$ is an epimorphism, i.e., for any pair of morphisms $g_1, g_2 : Y \to Z$, if $g_1 \circ f = g_2 \circ f$, then $g_1 = g_2$.
CategoryTheory.MorphismProperty.isomorphisms.infer_property theorem
[hf : IsIso f] : (isomorphisms C) f
Full source 
theorem isomorphisms.infer_property [hf : IsIso f] : (isomorphisms C) f :=
  hf
Isomorphism Property Inference Rule
Informal description
If a morphism \( f : X \to Y \) in a category \( \mathcal{C} \) is an isomorphism, then \( f \) satisfies the isomorphism property in \( \mathcal{C} \).
CategoryTheory.MorphismProperty.monomorphisms.infer_property theorem
[hf : Mono f] : (monomorphisms C) f
Full source 
theorem monomorphisms.infer_property [hf : Mono f] : (monomorphisms C) f :=
  hf
Monomorphism Property Inference Rule
Informal description
If a morphism $f$ in a category $\mathcal{C}$ is a monomorphism, then $f$ satisfies the monomorphism property in $\mathcal{C}$.
CategoryTheory.MorphismProperty.epimorphisms.infer_property theorem
[hf : Epi f] : (epimorphisms C) f
Full source 
theorem epimorphisms.infer_property [hf : Epi f] : (epimorphisms C) f :=
  hf
Epimorphism Property Inference Rule
Informal description
If a morphism $f$ in a category $\mathcal{C}$ is an epimorphism, then $f$ satisfies the epimorphism property in $\mathcal{C}$.
CategoryTheory.MorphismProperty.isomorphisms_op theorem
: (isomorphisms C).op = isomorphisms Cᵒᵖ
Full source 
lemma isomorphisms_op : (isomorphisms C).op = isomorphisms Cᵒᵖ := by
  ext X Y f
  simp only [op, isomorphisms.iff]
  exact ⟨fun _ ↦ inferInstanceAs (IsIso f.unop.op), fun _ ↦ inferInstance⟩
Isomorphism Property in Opposite Category Equals Opposite of Isomorphism Property
Informal description
The opposite of the isomorphism property in a category $C$ is equal to the isomorphism property in the opposite category $C^{\mathrm{op}}$. That is, for any morphism $f$ in $C^{\mathrm{op}}$, $f$ satisfies $(\text{isomorphisms } C)^{\mathrm{op}}$ if and only if $f$ satisfies $\text{isomorphisms } C^{\mathrm{op}}$.
CategoryTheory.MorphismProperty.RespectsIso.monomorphisms instance
: RespectsIso (monomorphisms C)
Full source 
instance RespectsIso.monomorphisms : RespectsIso (monomorphisms C) := by
  apply RespectsIso.mk <;>
    · intro X Y Z e f
      simp only [monomorphisms.iff]
      intro
      apply mono_comp
Monomorphism Property Respects Isomorphisms
Informal description
The property of being a monomorphism in a category $\mathcal{C}$ respects isomorphisms. That is, for any isomorphism $e: X \xrightarrow{\sim} Y$ and any monomorphism $f: Y \to Z$, the composition $e \circ f$ is also a monomorphism; and for any isomorphism $e: Y \xrightarrow{\sim} Z$ and any monomorphism $f: X \to Y$, the composition $f \circ e$ is also a monomorphism.
CategoryTheory.MorphismProperty.RespectsIso.epimorphisms instance
: RespectsIso (epimorphisms C)
Full source 
instance RespectsIso.epimorphisms : RespectsIso (epimorphisms C) := by
  apply RespectsIso.mk <;>
    · intro X Y Z e f
      simp only [epimorphisms.iff]
      intro
      apply epi_comp
Epimorphism Property Respects Isomorphisms
Informal description
The property of being an epimorphism in a category $\mathcal{C}$ respects isomorphisms. That is, for any isomorphism $e: X \xrightarrow{\sim} Y$ and any epimorphism $f: Y \to Z$, the composition $e \circ f$ is also an epimorphism; and for any isomorphism $e: Y \xrightarrow{\sim} Z$ and any epimorphism $f: X \to Y$, the composition $f \circ e$ is also an epimorphism.
CategoryTheory.MorphismProperty.RespectsIso.isomorphisms instance
: RespectsIso (isomorphisms C)
Full source 
instance RespectsIso.isomorphisms : RespectsIso (isomorphisms C) := by
  apply RespectsIso.mk <;>
    · intro X Y Z e f
      simp only [isomorphisms.iff]
      intro
      exact IsIso.comp_isIso
Isomorphism Property Respects Isomorphisms
Informal description
The property of being an isomorphism in a category $\mathcal{C}$ respects isomorphisms. That is, the property is stable under both precomposition and postcomposition with isomorphisms.
CategoryTheory.MorphismProperty.prod definition
{C₁ C₂ : Type*} [Category C₁] [Category C₂] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) : MorphismProperty (C₁ × C₂)
Full source 
/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`,
this is the induced morphism property on `C₁ × C₂`. -/
def prod {C₁ C₂ : Type*} [Category C₁] [Category C₂]
    (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) :
    MorphismProperty (C₁ × C₂) :=
  fun _ _ f => W₁ f.1 ∧ W₂ f.2
Product of morphism properties
Informal description
Given two categories \( C_1 \) and \( C_2 \) with morphism properties \( W_1 \) and \( W_2 \) respectively, the morphism property \( W_1 \times W_2 \) on the product category \( C_1 \times C_2 \) is defined such that a morphism \( f = (f_1, f_2) \) in \( C_1 \times C_2 \) satisfies \( W_1 \times W_2 \) if and only if \( f_1 \) satisfies \( W_1 \) and \( f_2 \) satisfies \( W_2 \).
CategoryTheory.MorphismProperty.pi definition
{J : Type w} {C : J → Type u} [∀ j, Category.{v} (C j)] (W : ∀ j, MorphismProperty (C j)) : MorphismProperty (∀ j, C j)
Full source 
/-- 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`. -/
def pi {J : Type w} {C : J → Type u} [∀ j, Category.{v} (C j)]
    (W : ∀ j, MorphismProperty (C j)) : MorphismProperty (∀ j, C j) :=
  fun _ _ f => ∀ j, (W j) (f j)
Product of morphism properties in a family of categories
Informal description
Given a family of categories $\{C_j\}_{j \in J}$ indexed by a type $J$, and for each $j \in J$ a morphism property $W_j$ on $C_j$, the morphism property $\prod_{j \in J} W_j$ on the product category $\prod_{j \in J} C_j$ is defined such that a morphism $f$ satisfies $\prod_{j \in J} W_j$ if and only if for every $j \in J$, the component $f_j$ satisfies $W_j$.
CategoryTheory.MorphismProperty.functorCategory definition
(W : MorphismProperty C) (J : Type*) [Category J] : MorphismProperty (J ⥤ C)
Full source 
/-- The morphism property on `J ⥤ C` which is defined objectwise
from `W : MorphismProperty C`. -/
def functorCategory (W : MorphismProperty C) (J : Type*) [Category J] :
    MorphismProperty (J ⥤ C) :=
  fun _ _ f => ∀ (j : J), W (f.app j)
Morphism property on functor category induced by \( W \)
Informal description
Given a morphism property \( W \) in a category \( C \) and a small category \( J \), the morphism property \( W \) induces a morphism property on the functor category \( J \to C \) where a natural transformation \( f \) satisfies the property if for every object \( j \) in \( J \), the component \( f_j \) satisfies \( W \).
CategoryTheory.MorphismProperty.arrow definition
(W : MorphismProperty C) : MorphismProperty (Arrow C)
Full source 
/-- Given `W : MorphismProperty C`, this is the morphism property on `Arrow C` of morphisms
whose left and right parts are in `W`. -/
def arrow (W : MorphismProperty C) :
    MorphismProperty (Arrow C) :=
  fun _ _ f => W f.left ∧ W f.right
Morphism property on arrow category induced by \( W \)
Informal description
Given a morphism property \( W \) in a category \( C \), this defines a morphism property on the arrow category \( \text{Arrow}(C) \) where a morphism \( f \) satisfies the property if both its left and right parts satisfy \( W \).
CategoryTheory.NatTrans.isIso_app_iff_of_iso theorem
{F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : IsIso (α.app X) ↔ IsIso (α.app Y)
Full source 
lemma isIso_app_iff_of_iso {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) :
    IsIsoIsIso (α.app X) ↔ IsIso (α.app Y) :=
  (MorphismProperty.isomorphisms D).arrow_mk_iso_iff
    (Arrow.isoMk (F.mapIso e) (G.mapIso e) (by simp))
Isomorphism of Natural Transformation Components via Object Isomorphism
Informal description
Let $\mathcal{C}$ and $\mathcal{D}$ be categories, and let $F, G : \mathcal{C} \to \mathcal{D}$ be functors. Given a natural transformation $\alpha : F \to G$ and an isomorphism $e : X \cong Y$ in $\mathcal{C}$, the component $\alpha_X : F(X) \to G(X)$ is an isomorphism if and only if the component $\alpha_Y : F(Y) \to G(Y)$ is an isomorphism.