Mathlib.CategoryTheory.Comma.Arrow

CategoryTheory.Arrow definition

Full source

/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
     squares in `T`. -/
def Arrow :=
  Comma.{v, v, v} (𝟭 T) (𝟭 T)

Arrow category

Informal description

The arrow category of a category $T$ has as objects all morphisms in $T$ and as morphisms commutative squares in $T$. This is constructed as a specialization of the comma category where both functors are the identity functor on $T$.

CategoryTheory.instCategoryArrow instance

: Category (Arrow T)

Full source

instance : Category (Arrow T) := commaCategory

The Arrow Category is a Category

Informal description

For any category $T$, the arrow category $\mathrm{Arrow}(T)$ is itself a category, where objects are morphisms in $T$ and morphisms are commutative squares in $T$.

CategoryTheory.Arrow.inhabited instance

[Inhabited T] : Inhabited (Arrow T)

Full source

instance Arrow.inhabited [Inhabited T] : Inhabited (Arrow T) where
  default := show Comma (𝟭 T) (𝟭 T) from default

Inhabitedness of the Arrow Category

Informal description

For any category $T$ that is inhabited (i.e., has at least one object), the arrow category of $T$ is also inhabited.

CategoryTheory.Arrow.hom_ext theorem

{X Y : Arrow T} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

Full source

@[ext]
lemma hom_ext {X Y : Arrow T} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
    f = g :=
  CommaMorphism.ext h₁ h₂

Extensionality of Morphisms in the Arrow Category

Informal description

For any two morphisms $f, g$ between objects $X$ and $Y$ in the arrow category of $T$, if the left components of $f$ and $g$ are equal and the right components of $f$ and $g$ are equal, then $f = g$.

CategoryTheory.Arrow.id_left theorem

(f : Arrow T) : CommaMorphism.left (𝟙 f) = 𝟙 f.left

Full source

@[simp]
theorem id_left (f : Arrow T) : CommaMorphism.left (𝟙 f) = 𝟙 f.left :=
  rfl

Identity Morphism Preserves Left Component in Arrow Category

Informal description

For any object $f$ in the arrow category of $T$, the left component of the identity morphism on $f$ is equal to the identity morphism on the left component of $f$.

CategoryTheory.Arrow.id_right theorem

(f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right

Full source

@[simp]
theorem id_right (f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right :=
  rfl

Identity Morphism Preserves Right Component in Arrow Category

Informal description

For any object $f$ in the arrow category of $T$, the right component of the identity morphism on $f$ is equal to the identity morphism on the right component of $f$.

CategoryTheory.Arrow.comp_left theorem

{X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).left = f.left ≫ g.left

Full source

@[simp, reassoc]
theorem comp_left {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).left = f.left ≫ g.left := rfl

Composition Preserves Left Component in Arrow Category

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the arrow category of $T$, the left component of the composition $f \circ g$ is equal to the composition of the left components of $f$ and $g$, i.e., $(f \circ g)_{\text{left}} = f_{\text{left}} \circ g_{\text{left}}$.

CategoryTheory.Arrow.comp_right theorem

{X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).right = f.right ≫ g.right

Full source

@[simp, reassoc]
theorem comp_right {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).right = f.right ≫ g.right := rfl

Composition Preserves Right Component in Arrow Category

Informal description

For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the arrow category of $T$, the right component of the composition $f \circ g$ is equal to the composition of the right components of $f$ and $g$, i.e., $(f \circ g)_{\text{right}} = f_{\text{right}} \circ g_{\text{right}}$.

CategoryTheory.Arrow.mk definition

{X Y : T} (f : X ⟶ Y) : Arrow T

Full source

/-- An object in the arrow category is simply a morphism in `T`. -/
@[simps]
def mk {X Y : T} (f : X ⟶ Y) : Arrow T where
  left := X
  right := Y
  hom := f

Arrow object from a morphism

Informal description

Given objects $X$ and $Y$ in a category $T$ and a morphism $f : X \to Y$, the function `Arrow.mk` constructs an object in the arrow category of $T$ represented by the morphism $f$.

CategoryTheory.Arrow.mk_eq theorem

(f : Arrow T) : Arrow.mk f.hom = f

Full source

@[simp]
theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f := by
  cases f
  rfl

Equality of Arrow Construction with Its Underlying Morphism

Informal description

For any object $f$ in the arrow category of $T$, the construction `Arrow.mk f.hom` is equal to $f$ itself, where $f.hom$ denotes the underlying morphism of $f$.

CategoryTheory.Arrow.mk_injective theorem

(A B : T) : Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T)

Full source

theorem mk_injective (A B : T) :
    Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => by
  cases h
  rfl

Injectivity of Arrow Construction from Morphisms

Informal description

For any objects $A$ and $B$ in a category $T$, the function $\operatorname{Arrow.mk} : (A \to B) \to \operatorname{Arrow}(T)$ that constructs an arrow object from a morphism is injective. That is, if $\operatorname{Arrow.mk}(f) = \operatorname{Arrow.mk}(g)$ for two morphisms $f, g : A \to B$, then $f = g$.

CategoryTheory.Arrow.mk_inj theorem

(A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g

Full source

theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mkArrow.mk f = Arrow.mk g ↔ f = g :=
  (mk_injective A B).eq_iff

Injectivity of Arrow Construction: $\mathrm{Arrow.mk}(f) = \mathrm{Arrow.mk}(g) \leftrightarrow f = g$

Informal description

For any objects $A$ and $B$ in a category $T$ and any morphisms $f, g \colon A \to B$, the arrow objects $\mathrm{Arrow.mk}(f)$ and $\mathrm{Arrow.mk}(g)$ in the arrow category of $T$ are equal if and only if the morphisms $f$ and $g$ are equal.

CategoryTheory.Arrow.instCoeOutHom instance

{X Y : T} : CoeOut (X ⟶ Y) (Arrow T)

Full source

instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
  coe := mk

Morphisms as Objects in the Arrow Category

Informal description

For any objects $X$ and $Y$ in a category $T$, there is a canonical way to view a morphism $f : X \to Y$ as an object in the arrow category of $T$.

CategoryTheory.Arrow.mk_eq_mk_iff theorem

 {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y') :
  Arrow.mk f = Arrow.mk f' ↔ ∃ (hX : X = X') (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom hY.symm

Full source

lemma mk_eq_mk_iff {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y') :
    Arrow.mkArrow.mk f = Arrow.mk f' ↔
      ∃ (hX : X = X') (hY : Y = Y'), f = eqToHom hX ≫ f' ≫ eqToHom hY.symm := by
  constructor
  · intro h
    refine ⟨congr_arg Comma.left h, congr_arg Comma.right h, ?_⟩
    have := (eqToIso h).hom.w
    dsimp at this
    rw [Comma.eqToHom_left, Comma.eqToHom_right] at this
    rw [reassoc_of% this, eqToHom_trans, eqToHom_refl, Category.comp_id]
  · rintro ⟨rfl, rfl, h⟩
    simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h
    rw [h]

Equality of Arrow Objects via Commutative Squares

Informal description

For any morphisms $f \colon X \to Y$ and $f' \colon X' \to Y'$ in a category $T$, the objects $\mathrm{Arrow.mk}(f)$ and $\mathrm{Arrow.mk}(f')$ in the arrow category of $T$ are equal if and only if there exist equalities $h_X \colon X = X'$ and $h_Y \colon Y = Y'$ such that $f = \mathrm{eqToHom}(h_X) \circ f' \circ \mathrm{eqToHom}(h_Y^{-1})$.

CategoryTheory.Arrow.ext theorem

 {f g : Arrow T} (h₁ : f.left = g.left) (h₂ : f.right = g.right) (h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) :
  f = g

Full source

lemma ext {f g : Arrow T}
    (h₁ : f.left = g.left) (h₂ : f.right = g.right)
    (h₃ : f.hom = eqToHomeqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) : f = g :=
  (mk_eq_mk_iff _ _).2 (by aesop)

Extensionality for Arrow Category Objects

Informal description

For any two objects $f$ and $g$ in the arrow category of $T$, if their left objects are equal ($h_1 : f_{\text{left}} = g_{\text{left}}$), their right objects are equal ($h_2 : f_{\text{right}} = g_{\text{right}}$), and their morphisms satisfy $f_{\text{hom}} = \text{eqToHom}(h_1) \circ g_{\text{hom}} \circ \text{eqToHom}(h_2^{-1})$, then $f = g$.

CategoryTheory.Arrow.arrow_mk_comp_eqToHom theorem

{X Y Y' : T} (f : X ⟶ Y) (h : Y = Y') : Arrow.mk (f ≫ eqToHom h) = Arrow.mk f

Full source

@[simp]
lemma arrow_mk_comp_eqToHom {X Y Y' : T} (f : X ⟶ Y) (h : Y = Y') :
    Arrow.mk (f ≫ eqToHom h) = Arrow.mk f :=
  ext rfl h.symm (by simp)

Equality of Arrow Objects under Post-Composition with Identity Morphism

Informal description

For any morphism $f \colon X \to Y$ in a category $T$ and any equality $h \colon Y = Y'$, the object $\mathrm{Arrow.mk}(f \circ \mathrm{eqToHom}(h))$ in the arrow category of $T$ is equal to $\mathrm{Arrow.mk}(f)$.

CategoryTheory.Arrow.arrow_mk_eqToHom_comp theorem

{X' X Y : T} (f : X ⟶ Y) (h : X' = X) : Arrow.mk (eqToHom h ≫ f) = Arrow.mk f

Full source

@[simp]
lemma arrow_mk_eqToHom_comp {X' X Y : T} (f : X ⟶ Y) (h : X' = X) :
    Arrow.mk (eqToHomeqToHom h ≫ f) = Arrow.mk f :=
  ext h rfl (by simp)

Equality of Arrow Objects under Precomposition with eqToHom

Informal description

For any objects $X'$, $X$, and $Y$ in a category $T$, a morphism $f : X \to Y$, and an equality $h : X' = X$, the arrow object constructed from the composition $\text{eqToHom}(h) \circ f$ is equal to the arrow object constructed from $f$ alone, i.e., $\text{Arrow.mk}(\text{eqToHom}(h) \circ f) = \text{Arrow.mk}(f)$.

CategoryTheory.Arrow.w_mk_right theorem

{f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) : sq.left ≫ g = f.hom ≫ sq.right

Full source

@[reassoc (attr := simp)]
theorem w_mk_right {f : Arrow T} {X Y : T} {g : X ⟶ Y} (sq : f ⟶ mk g) :
    sq.left ≫ g = f.hom ≫ sq.right :=
  sq.w

Commutativity of Squares in the Arrow Category

Informal description

Given an object $f$ in the arrow category of $T$, objects $X$ and $Y$ in $T$, a morphism $g : X \to Y$, and a morphism $\mathrm{sq} : f \to \mathrm{mk}(g)$ in the arrow category, the composition $\mathrm{sq}.\mathrm{left} \circ g$ equals the composition $f.\mathrm{hom} \circ \mathrm{sq}.\mathrm{right}$.

CategoryTheory.Arrow.w theorem

{f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right

Full source

@[reassoc]
theorem w {f g : Arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := by
  simp

Commutativity of Squares in the Arrow Category

Informal description

Given two objects $f$ and $g$ in the arrow category of $T$ and a morphism $\mathrm{sq} : f \to g$ between them, the composition $\mathrm{sq}.\mathrm{left} \circ g.\mathrm{hom}$ equals the composition $f.\mathrm{hom} \circ \mathrm{sq}.\mathrm{right}$.

CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_right theorem

{f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left] [IsIso ff.right] : IsIso ff

Full source

theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
    [IsIso ff.right] : IsIso ff where
  out := by
    let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
    apply Exists.intro inverse
    aesop_cat

Morphism in Arrow Category is Isomorphism if Components Are Isomorphisms

Informal description

Let $T$ be a category, and let $f, g$ be objects in the arrow category of $T$ (i.e., $f$ and $g$ are morphisms in $T$). Given a morphism $\phi : f \to g$ in the arrow category, if both the left component $\phi.\mathrm{left}$ and the right component $\phi.\mathrm{right}$ of $\phi$ are isomorphisms in $T$, then $\phi$ itself is an isomorphism in the arrow category.

CategoryTheory.Arrow.hom.congr_left theorem

{f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left

Full source

theorem hom.congr_left {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left := by
  rw [h]

Equality of Morphisms Implies Equality of Left Components in Arrow Category

Informal description

For any two morphisms $\phi_1, \phi_2$ between objects $f$ and $g$ in the arrow category of $T$, if $\phi_1 = \phi_2$, then their left components are equal, i.e., $\phi_1.\mathrm{left} = \phi_2.\mathrm{left}$.

CategoryTheory.Arrow.hom.congr_right theorem

{f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right

Full source

@[simp]
theorem hom.congr_right {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right := by
  rw [h]

Equality of Morphisms Implies Equality of Right Components in Arrow Category

Informal description

For any two morphisms $\phi_1, \phi_2$ between objects $f$ and $g$ in the arrow category of $T$, if $\phi_1 = \phi_2$, then their right components are equal, i.e., $\phi_1.\mathrm{right} = \phi_2.\mathrm{right}$.

CategoryTheory.Arrow.iso_w theorem

{f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right

Full source

theorem iso_w {f g : Arrow T} (e : f ≅ g) : g.hom = e.inv.left ≫ f.hom ≫ e.hom.right := by
  have eq := Arrow.hom.congr_right e.inv_hom_id
  rw [Arrow.comp_right, Arrow.id_right] at eq
  rw [Arrow.w_assoc, eq, Category.comp_id]

Isomorphism Decomposition in the Arrow Category

Informal description

For any isomorphism $e \colon f \to g$ in the arrow category of $T$, the morphism $g$ can be expressed as the composition $e^{-1}_{\text{left}} \circ f \circ e_{\text{right}}$, where $e^{-1}_{\text{left}}$ is the left component of the inverse of $e$, and $e_{\text{right}}$ is the right component of $e$.

CategoryTheory.Arrow.iso_w' theorem

{W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : g = e.inv.left ≫ f ≫ e.hom.right

Full source

theorem iso_w' {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mkArrow.mk f ≅ Arrow.mk g) :
    g = e.inv.left ≫ f ≫ e.hom.right :=
  iso_w e

Isomorphism Decomposition in the Arrow Category for Explicit Morphisms

Informal description

For any objects $W, X, Y, Z$ in a category $T$ and morphisms $f \colon W \to X$ and $g \colon Y \to Z$, given an isomorphism $e \colon \mathrm{Arrow.mk}(f) \to \mathrm{Arrow.mk}(g)$ in the arrow category of $T$, the morphism $g$ can be expressed as the composition $e^{-1}_{\text{left}} \circ f \circ e_{\text{right}}$, where $e^{-1}_{\text{left}}$ is the left component of the inverse of $e$, and $e_{\text{right}}$ is the right component of $e$.

CategoryTheory.Arrow.isIso_left instance

[IsIso sq] : IsIso sq.left

Full source

instance isIso_left [IsIso sq] : IsIso sq.left where
  out := by
    apply Exists.intro (inv sq).left
    simp only [← Comma.comp_left, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_left,
      eq_self_iff_true, and_self_iff]
    simp

Isomorphism of Left Morphism in Arrow Category

Informal description

For any commutative square $sq$ in the arrow category of a category $T$, if $sq$ is an isomorphism, then the left morphism $sq.left$ is also an isomorphism.

CategoryTheory.Arrow.isIso_right instance

[IsIso sq] : IsIso sq.right

Full source

instance isIso_right [IsIso sq] : IsIso sq.right where
  out := by
    apply Exists.intro (inv sq).right
    simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_right,
      eq_self_iff_true, and_self_iff]
    simp

Isomorphism of Right Morphism in Arrow Category

Informal description

For any commutative square $sq$ in the arrow category of a category $T$, if $sq$ is an isomorphism, then the right morphism $sq.right$ is also an isomorphism.

CategoryTheory.Arrow.isIso_of_isIso theorem

{X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mk f ⟶ g) [IsIso sq] [IsIso f] : IsIso g.hom

Full source

lemma isIso_of_isIso {X Y : T} {f : X ⟶ Y} {g : Arrow T} (sq : mkmk f ⟶ g) [IsIso sq] [IsIso f] :
    IsIso g.hom := by
  rw [iso_w' (asIso sq)]
  infer_instance

Isomorphism of Target Morphism in Arrow Category Given Isomorphism of Source and Square

Informal description

Let $T$ be a category, $X$ and $Y$ objects in $T$, and $f : X \to Y$ a morphism in $T$. Given an object $g$ in the arrow category of $T$ and a morphism $sq : \mathrm{Arrow.mk}(f) \to g$ in the arrow category, if $sq$ is an isomorphism and $f$ is an isomorphism, then the underlying morphism $g.hom$ of $g$ is also an isomorphism.

CategoryTheory.Arrow.isIso_hom_iff_isIso_hom_of_isIso theorem

{f g : Arrow T} (sq : f ⟶ g) [IsIso sq] : IsIso f.hom ↔ IsIso g.hom

Full source

lemma isIso_hom_iff_isIso_hom_of_isIso {f g : Arrow T} (sq : f ⟶ g) [IsIso sq] :
    IsIsoIsIso f.hom ↔ IsIso g.hom :=
  ⟨fun _ => isIso_of_isIso sq, fun _ => isIso_of_isIso (inv sq)⟩

Isomorphism of Underlying Morphisms in Arrow Category Given Isomorphic Squares

Informal description

Let $T$ be a category, and let $f$ and $g$ be objects in the arrow category of $T$ (i.e., $f$ and $g$ are morphisms in $T$). Given a morphism $sq : f \to g$ in the arrow category (i.e., a commutative square in $T$), if $sq$ is an isomorphism, then the underlying morphism $f.hom$ is an isomorphism if and only if the underlying morphism $g.hom$ is an isomorphism.

CategoryTheory.Arrow.isIso_iff_isIso_of_isIso theorem

{W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (sq : mk f ⟶ mk g) [IsIso sq] : IsIso f ↔ IsIso g

Full source

lemma isIso_iff_isIso_of_isIso {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z} (sq : mkmk f ⟶ mk g) [IsIso sq] :
    IsIsoIsIso f ↔ IsIso g :=
  isIso_hom_iff_isIso_hom_of_isIso sq

Isomorphism Equivalence in Arrow Category via Isomorphic Squares

Informal description

Let $T$ be a category, and let $f : W \to X$ and $g : Y \to Z$ be morphisms in $T$. Given a commutative square $sq$ between $\mathrm{Arrow.mk}(f)$ and $\mathrm{Arrow.mk}(g)$ in the arrow category of $T$, if $sq$ is an isomorphism, then $f$ is an isomorphism if and only if $g$ is an isomorphism.

CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIso theorem

{Y Z : T} {f : Arrow T} {g : Y ⟶ Z} (sq : f ⟶ mk g) [IsIso sq] : IsIso f.hom ↔ IsIso g

Full source

lemma isIso_hom_iff_isIso_of_isIso {Y Z : T} {f : Arrow T} {g : Y ⟶ Z} (sq : f ⟶ mk g) [IsIso sq] :
    IsIsoIsIso f.hom ↔ IsIso g :=
  isIso_hom_iff_isIso_hom_of_isIso sq

Isomorphism of Underlying Morphisms in Arrow Category via Isomorphic Square to Generated Arrow

Informal description

Let $T$ be a category, $f$ be an object in the arrow category of $T$ (i.e., a morphism in $T$), and $g : Y \to Z$ be a morphism in $T$. Given a morphism $sq : f \to \mathrm{mk}(g)$ in the arrow category (i.e., a commutative square in $T$), if $sq$ is an isomorphism, then the underlying morphism $f.\mathrm{hom}$ is an isomorphism if and only if $g$ is an isomorphism.

CategoryTheory.Arrow.inv_left theorem

[IsIso sq] : (inv sq).left = inv sq.left

Full source

@[simp]
theorem inv_left [IsIso sq] : (inv sq).left = inv sq.left :=
  IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Inverse of Left Component in Arrow Category

Informal description

For any commutative square $sq$ in the arrow category of a category $T$, if $sq$ is an isomorphism, then the left component of the inverse square $(sq)^{-1}$ is equal to the inverse of the left component of $sq$. That is, $(sq^{-1}).left = (sq.left)^{-1}$.

CategoryTheory.Arrow.inv_right theorem

[IsIso sq] : (inv sq).right = inv sq.right

Full source

@[simp]
theorem inv_right [IsIso sq] : (inv sq).right = inv sq.right :=
  IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Inverse of Arrow Isomorphism Preserves Right Component

Informal description

For any commutative square $sq$ in the arrow category of a category $T$, if $sq$ is an isomorphism, then the right component of the inverse of $sq$ is equal to the inverse of the right component of $sq$. That is, $(sq^{-1}).right = (sq.right)^{-1}$.

CategoryTheory.Arrow.left_hom_inv_right theorem

[IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom

Full source

theorem left_hom_inv_right [IsIso sq] : sq.left ≫ g.hom ≫ inv sq.right = f.hom := by
  simp only [← Category.assoc, IsIso.comp_inv_eq, w]

Composition with Inverse in Arrow Category

Informal description

For any isomorphism $\mathrm{sq} : f \to g$ in the arrow category of $T$, the composition $\mathrm{sq}.\mathrm{left} \circ g.\mathrm{hom} \circ (\mathrm{sq}.\mathrm{right})^{-1}$ equals $f.\mathrm{hom}$.

CategoryTheory.Arrow.inv_left_hom_right theorem

[IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.hom

Full source

theorem inv_left_hom_right [IsIso sq] : invinv sq.left ≫ f.hom ≫ sq.right = g.hom := by
  simp only [w, IsIso.inv_comp_eq]

Inverse Left Homomorphism Right Identity in Arrow Category

Informal description

Let $f$ and $g$ be objects in the arrow category of a category $T$, and let $\mathrm{sq} : f \to g$ be an isomorphism in this category. Then the composition of the inverse of the left morphism of $\mathrm{sq}$, the morphism $f.\mathrm{hom}$, and the right morphism of $\mathrm{sq}$ equals the morphism $g.\mathrm{hom}$, i.e., \[ \mathrm{sq}^{-1}.\mathrm{left} \circ f.\mathrm{hom} \circ \mathrm{sq}.\mathrm{right} = g.\mathrm{hom}. \]

CategoryTheory.Arrow.mono_left instance

[Mono sq] : Mono sq.left

Full source

instance mono_left [Mono sq] : Mono sq.left where
  right_cancellation {Z} φ ψ h := by
    let aux : (Z ⟶ f.left) → (Arrow.mkArrow.mk (𝟙 Z) ⟶ f) := fun φ =>
      { left := φ
        right := φ ≫ f.hom }
    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp
    show (aux φ).left = (aux ψ).left
    congr 1
    rw [← cancel_mono sq]
    apply CommaMorphism.ext
    · exact h
    · rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc]
      rw [← Arrow.w]
      simp only [← Category.assoc, h]

Left Component of a Monomorphism in the Arrow Category is Monic

Informal description

For any monomorphism $\mathrm{sq} \colon f \to g$ in the arrow category of $T$, the left component $\mathrm{sq}.\mathrm{left}$ is a monomorphism in $T$.

CategoryTheory.Arrow.epi_right instance

[Epi sq] : Epi sq.right

Full source

instance epi_right [Epi sq] : Epi sq.right where
  left_cancellation {Z} φ ψ h := by
    let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
      { right := φ
        left := g.hom ≫ φ }
    show (aux φ).right = (aux ψ).right
    congr 1
    rw [← cancel_epi sq]
    apply CommaMorphism.ext
    · rw [Comma.comp_left, Comma.comp_left, Arrow.w_assoc, Arrow.w_assoc, h]
    · exact h

Right Component of an Epimorphism in the Arrow Category is Epimorphic

Informal description

For any epimorphism $sq$ in the arrow category of a category $T$, the right component $sq.right$ is an epimorphism in $T$.

CategoryTheory.Arrow.hom_inv_id_left theorem

(e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma hom_inv_id_left (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 _ := by
  rw [← comp_left, e.hom_inv_id, id_left]

Left Component of Isomorphism in Arrow Category Satisfies Hom-Inv Identity

Informal description

For any isomorphism $e \colon f \cong g$ in the arrow category of $T$, the composition of the left component of the homomorphism $e.hom$ with the left component of the inverse $e.inv$ is equal to the identity morphism on the domain of $f$, i.e., $e.hom.left \circ e.inv.left = \text{id}_{f.left}$.

CategoryTheory.Arrow.inv_hom_id_left theorem

(e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma inv_hom_id_left (e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 _ := by
  rw [← comp_left, e.inv_hom_id, id_left]

Left Component of Isomorphism in Arrow Category Satisfies Inv-Hom Identity

Informal description

For any isomorphism $e \colon f \cong g$ in the arrow category of $T$, the composition of the left component of the inverse morphism $e^{-1}$ with the left component of the morphism $e$ is equal to the identity morphism on the domain of $f$, i.e., $e^{-1}_{\text{left}} \circ e_{\text{left}} = \text{id}_{f_{\text{left}}}$.

CategoryTheory.Arrow.hom_inv_id_right theorem

(e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma hom_inv_id_right (e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 _ := by
  rw [← comp_right, e.hom_inv_id, id_right]

Right Component of Isomorphism in Arrow Category Satisfies Hom-Inv Identity

Informal description

For any isomorphism $e \colon f \cong g$ in the arrow category of $T$, the composition of the right component of the homomorphism $e.hom$ with the right component of the inverse $e.inv$ is equal to the identity morphism on the codomain of $f$, i.e., $e.hom.right \circ e.inv.right = \text{id}_{f.right}$.

CategoryTheory.Arrow.inv_hom_id_right theorem

(e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 _

Full source

@[reassoc (attr := simp)]
lemma inv_hom_id_right (e : f ≅ g) : e.inv.right ≫ e.hom.right = 𝟙 _ := by
  rw [← comp_right, e.inv_hom_id, id_right]

Right Component of Isomorphism in Arrow Category Satisfies Inv-Hom Identity

Informal description

For any isomorphism $e \colon f \cong g$ in the arrow category of $T$, the composition of the right component of the inverse morphism $e^{-1}$ with the right component of the morphism $e$ is equal to the identity morphism on the codomain of $f$, i.e., $e^{-1}_{\text{right}} \circ e_{\text{right}} = \text{id}_{f_{\text{right}}}$.

CategoryTheory.Arrow.square_to_iso_invert theorem

(i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ Arrow.mk p.hom) : i.hom ≫ sq.right ≫ p.inv = sq.left

Full source

/-- Given a square from an arrow `i` to an isomorphism `p`, express the source part of `sq`
in terms of the inverse of `p`. -/
@[simp]
theorem square_to_iso_invert (i : Arrow T) {X Y : T} (p : X ≅ Y) (sq : i ⟶ Arrow.mk p.hom) :
    i.hom ≫ sq.right ≫ p.inv = sq.left := by
  simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm

Commutative Square to Isomorphism Inversion in Arrow Category

Informal description

Given an object $i$ in the arrow category of $T$, objects $X$ and $Y$ in $T$, an isomorphism $p : X \cong Y$, and a commutative square $sq$ from $i$ to the arrow object of $p$, the composition $i.\mathrm{hom} \circ sq.\mathrm{right} \circ p^{-1}$ equals $sq.\mathrm{left}$.

CategoryTheory.Arrow.square_from_iso_invert theorem

{X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : Arrow.mk i.hom ⟶ p) : i.inv ≫ sq.left ≫ p.hom = sq.right

Full source

/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq`
in terms of the inverse of `i`. -/
theorem square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : Arrow.mkArrow.mk i.hom ⟶ p) :
    i.inv ≫ sq.left ≫ p.hom = sq.right := by simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom]

Commutative Square from Isomorphism Inversion in Arrow Category

Informal description

Given an isomorphism $i \colon X \cong Y$ in a category $T$, an object $p$ in the arrow category of $T$, and a commutative square $sq$ from the arrow object of $i$ to $p$, the composition $i^{-1} \circ sq.\mathrm{left} \circ p.\mathrm{hom}$ equals $sq.\mathrm{right}$.

CategoryTheory.Arrow.squareToSnd definition

{X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ Arrow.mk (f ≫ g)) : i ⟶ Arrow.mk g

Full source

/-- A helper construction: given a square between `i` and `f ≫ g`, produce a square between
`i` and `g`, whose top leg uses `f`:
A  → X
     ↓f
↓i   Y             --> A → Y
     ↓g                ↓i  ↓g
B  → Z                 B → Z
-/
@[simps]
def squareToSnd {X Y Z : C} {i : Arrow C} {f : X ⟶ Y} {g : Y ⟶ Z} (sq : i ⟶ Arrow.mk (f ≫ g)) :
    i ⟶ Arrow.mk g where
  left := sq.left ≫ f
  right := sq.right

Induced square from composition to second morphism

Informal description

Given objects $X, Y, Z$ in a category $C$, an object $i$ in the arrow category of $C$, and morphisms $f : X \to Y$ and $g : Y \to Z$, any commutative square $sq$ from $i$ to the arrow object of $f \circ g$ induces a commutative square from $i$ to the arrow object of $g$. The top leg of the new square is obtained by composing the top leg of $sq$ with $f$, while the bottom leg remains unchanged.

CategoryTheory.Arrow.leftFunc definition

: Arrow C ⥤ C

Full source

/-- The functor sending an arrow to its source. -/
@[simps!]
def leftFunc : ArrowArrow C ⥤ C :=
  Comma.fst _ _

Source functor of the arrow category

Informal description

The functor that maps each object in the arrow category of $C$ (i.e., each morphism in $C$) to its source object in $C$.

CategoryTheory.Arrow.rightFunc definition

: Arrow C ⥤ C

Full source

/-- The functor sending an arrow to its target. -/
@[simps!]
def rightFunc : ArrowArrow C ⥤ C :=
  Comma.snd _ _

Target functor of the arrow category

Informal description

The functor that maps each object in the arrow category of $C$ (i.e., each morphism in $C$) to its target object in $C$.

CategoryTheory.Arrow.leftToRight definition

: (leftFunc : Arrow C ⥤ C) ⟶ rightFunc

Full source

/-- The natural transformation from `leftFunc` to `rightFunc`, given by the arrow itself. -/
@[simps]
def leftToRight : (leftFunc : Arrow C ⥤ C) ⟶ rightFunc where app f := f.hom

Natural transformation from source to target functor in arrow category

Informal description

The natural transformation from the source functor to the target functor of the arrow category, which assigns to each object (a morphism $f$ in $C$) the morphism $f$ itself.

CategoryTheory.Functor.mapArrow definition

(F : C ⥤ D) : Arrow C ⥤ Arrow D

Full source

/-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/
@[simps]
def mapArrow (F : C ⥤ D) : ArrowArrow C ⥤ Arrow D where
  obj a := Arrow.mk (F.map a.hom)
  map f :=
    { left := F.map f.left
      right := F.map f.right
      w := by
        let w := f.w
        simp only [id_map] at w
        dsimp
        simp only [← F.map_comp, w] }

Functor between arrow categories induced by a functor

Informal description

Given a functor $F : C \to D$ between categories $C$ and $D$, the induced functor $\mathrm{Arrow}(C) \to \mathrm{Arrow}(D)$ maps each object (a morphism $f$ in $C$) to the object $F(f)$ in $\mathrm{Arrow}(D)$, and each morphism (a commutative square in $C$) to the corresponding commutative square in $D$ obtained by applying $F$ to all morphisms involved.

CategoryTheory.Functor.mapArrowFunctor definition

: (C ⥤ D) ⥤ (Arrow C ⥤ Arrow D)

Full source

/-- The functor `(C ⥤ D) ⥤ (Arrow C ⥤ Arrow D)` which sends
a functor `F : C ⥤ D` to `F.mapArrow`. -/
@[simps]
def mapArrowFunctor : (C ⥤ D) ⥤ (Arrow C ⥤ Arrow D) where
  obj F := F.mapArrow
  map τ :=
    { app := fun f =>
        { left := τ.app _
          right := τ.app _ } }

Functor from $(C \to D)$ to $(\mathrm{Arrow}(C) \to \mathrm{Arrow}(D))$

Informal description

The functor that maps a functor $F \colon C \to D$ between categories $C$ and $D$ to the induced functor $\mathrm{Arrow}(C) \to \mathrm{Arrow}(D)$, which sends each object (a morphism $f$ in $C$) to $F(f)$ and each morphism (a commutative square in $C$) to the corresponding commutative square in $D$ obtained by applying $F$ to all morphisms involved.

CategoryTheory.Functor.mapArrowEquivalence definition

(e : C ≌ D) : Arrow C ≌ Arrow D

Full source

/-- The equivalence of categories `Arrow C ≌ Arrow D` induced by an equivalence `C ≌ D`. -/
def mapArrowEquivalence (e : C ≌ D) : ArrowArrow C ≌ Arrow D where
  functor := e.functor.mapArrow
  inverse := e.inverse.mapArrow
  unitIso := Functor.mapIso (mapArrowFunctor C C) e.unitIso
  counitIso := Functor.mapIso (mapArrowFunctor D D) e.counitIso

Equivalence of arrow categories induced by an equivalence

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the induced equivalence $\mathrm{Arrow}(C) \simeq \mathrm{Arrow}(D)$ between their arrow categories is constructed as follows: - The forward functor is the application of $e$'s functor component to arrows in $C$, - The inverse functor is the application of $e$'s inverse component to arrows in $D$, - The unit and counit isomorphisms are obtained by applying the corresponding isomorphisms from $e$ to the identity functors on $C$ and $D$ respectively.

CategoryTheory.Functor.isEquivalence_mapArrow instance

(F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.mapArrow

Full source

instance isEquivalence_mapArrow (F : C ⥤ D) [IsEquivalence F] :
    IsEquivalence F.mapArrow :=
  (mapArrowEquivalence (asEquivalence F)).isEquivalence_functor

Equivalence of Arrow Categories Induced by an Equivalence

Informal description

Given an equivalence of categories $F \colon C \simeq D$, the induced functor $F.\mathrm{mapArrow} \colon \mathrm{Arrow}(C) \to \mathrm{Arrow}(D)$ is also an equivalence of categories.

CategoryTheory.Arrow.isoOfNatIso definition

{F G : C ⥤ D} (e : F ≅ G) (f : Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f

Full source

/-- The images of `f : Arrow C` by two isomorphic functors `F : C ⥤ D` are
isomorphic arrows in `D`. -/
def Arrow.isoOfNatIso {F G : C ⥤ D} (e : F ≅ G)
    (f : Arrow C) : F.mapArrow.obj f ≅ G.mapArrow.obj f :=
  Arrow.isoMk (e.app f.left) (e.app f.right)

Isomorphism of arrow images under isomorphic functors

Informal description

Given two isomorphic functors $F, G : C \to D$ and an object $f$ in the arrow category of $C$, the images of $f$ under $F$ and $G$ are isomorphic in the arrow category of $D$. Specifically, the isomorphism is constructed using the components of the natural isomorphism $e : F \cong G$ applied to the domain and codomain of $f$.

CategoryTheory.Arrow.equivSigma definition

: Arrow T ≃ Σ (X Y : T), X ⟶ Y

Full source

/-- `Arrow T` is equivalent to a sigma type. -/
@[simps!]
def Arrow.equivSigma :
    ArrowArrow T ≃ Σ (X Y : T), X ⟶ Y where
  toFun f := ⟨_, _, f.hom⟩
  invFun x := Arrow.mk x.2.2
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between arrow category and sigma type of morphisms

Informal description

The arrow category of a category $T$ is equivalent to the sigma type consisting of triples $(X, Y, f)$ where $X$ and $Y$ are objects in $T$ and $f : X \to Y$ is a morphism in $T$. The equivalence is given by mapping an arrow object to its underlying morphism and vice versa.

CategoryTheory.Arrow.discreteEquiv definition

(S : Type u) : Arrow (Discrete S) ≃ S

Full source

/-- The equivalence `Arrow (Discrete S) ≃ S`. -/
def Arrow.discreteEquiv (S : Type u) : ArrowArrow (Discrete S) ≃ S where
  toFun f := f.left.as
  invFun s := Arrow.mk (𝟙 (Discrete.mk s))
  left_inv := by
    rintro ⟨⟨_⟩, ⟨_⟩, f⟩
    obtain rfl := Discrete.eq_of_hom f
    rfl
  right_inv _ := rfl

Equivalence between arrow category of discrete category and base type

Informal description

The equivalence between the arrow category of the discrete category over a type $S$ and the type $S$ itself. Specifically, it maps an object in the arrow category (which is an identity morphism in the discrete category) to its underlying element in $S$, and conversely, it maps an element $s \in S$ to the identity morphism on $s$ in the discrete category.

CategoryTheory.Arrow.functor_ext theorem

 {F G : C ⥤ D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)) : F = G

Full source

/-- Extensionality lemma for functors `C ⥤ D` which uses as an assumption
that the induced maps `Arrow C → Arrow D` coincide. -/
lemma Arrow.functor_ext {F G : C ⥤ D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)) :
    F = G :=
  Functor.ext (fun X ↦ congr_arg Comma.left (h (𝟙 X))) (fun X Y f ↦ by
    have := h f
    simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this
    tauto)

Extensionality of Functors via Arrow Category

Informal description

For any two functors $F, G \colon C \to D$, if for all objects $X, Y$ in $C$ and all morphisms $f \colon X \to Y$, the objects $F(f)$ and $G(f)$ in the arrow category of $D$ are equal, then $F = G$.

Tags