<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.comma

/-!
# The category of arrows

The category of arrows, with morphisms commutative squares.
We set this up as a specialization of the comma category `comma L R`,
where `L` and `R` are both the identity functor.

We also define the typeclass `has_lift`, representing a choice of a lift
of a commutative square (that is, a diagonal morphism making the two triangles commute).

## Tags

comma, arrow
-/

namespace category_theory

universes v u -- morphism levels before object levels. See note [category_theory universes].
variables {T : Type u} [category.{v} T]

section
variables (T)

/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
     squares in `T`. -/
@[derive category]
def arrow := comma.{v v v} (𝟭 T) (𝟭 T)

-- Satisfying the inhabited linter
instance arrow.inhabited [inhabited T] : inhabited (arrow T) :=
{ default := show comma (𝟭 T) (𝟭 T), from default (comma (𝟭 T) (𝟭 T)) }

end

namespace arrow

@[simp] lemma id_left (f : arrow T) : comma_morphism.left (𝟙 f) = 𝟙 (f.left) := rfl
@[simp] lemma id_right (f : arrow T) : comma_morphism.right (𝟙 f) = 𝟙 (f.right) := rfl

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

theorem mk_injective (A B : T) :
  function.injective (arrow.mk : (A ⟶ B) → arrow T) :=
λ f g h, by { cases h, refl }

theorem mk_inj (A B : T) {f g : A ⟶ B} : arrow.mk f = arrow.mk g ↔ f = g :=
(mk_injective A B).eq_iff
instance {X Y : T} : has_coe (X ⟶ Y) (arrow T) := ⟨mk⟩

/-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
    category. -/
@[simps]
def hom_mk {f g : arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right}
  (w : u ≫ g.hom = f.hom ≫ v) : f ⟶ g :=
{ left := u,
  right := v,
  w' := w }

/-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/
@[simps]
def hom_mk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
  (w : u ≫ g = f ≫ v) : arrow.mk f ⟶ arrow.mk g :=
{ left := u,
  right := v,
  w' := w }

@[simp, reassoc] lemma w {f g : arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := sq.w

-- `w_mk_left` is not needed, as it is a consequence of `w` and `mk_hom`.
@[simp, reassoc] lemma 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

instance {f g : arrow T} (ff : f ⟶ g) [is_iso ff.left] [is_iso ff.right] :
  is_iso ff :=
{ out := ⟨⟨inv ff.left, inv ff.right⟩,
          by { ext; dsimp; simp only [is_iso.hom_inv_id] },
          by { ext; dsimp; simp only [is_iso.inv_hom_id] }⟩ }

/-- Create an isomorphism between arrows,
by providing isomorphisms between the domains and codomains,
and a proof that the square commutes. -/
@[simps] def iso_mk {f g : arrow T}
  (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : l.hom ≫ g.hom = f.hom ≫ r.hom) :
  f ≅ g :=
comma.iso_mk l r h

/-- 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] lemma 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)

/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq`
in terms of the inverse of `i`. -/
lemma square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : arrow T) (sq : arrow.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]

/-- A lift of a commutative square is a diagonal morphism making the two triangles commute. -/
@[ext] structure lift_struct {f g : arrow T} (sq : f ⟶ g) :=
(lift : f.right ⟶ g.left)
(fac_left' : f.hom ≫ lift = sq.left . obviously)
(fac_right' : lift ≫ g.hom = sq.right . obviously)

restate_axiom lift_struct.fac_left'
restate_axiom lift_struct.fac_right'

instance lift_struct_inhabited {X : T} : inhabited (lift_struct (𝟙 (arrow.mk (𝟙 X)))) :=
⟨⟨𝟙 _, category.id_comp _, category.comp_id _⟩⟩<commit_msg>feat(category_theory/arrow): is_iso, mono, epi instances for maps between arrows (#9976)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.comma

/-!
# The category of arrows

The category of arrows, with morphisms commutative squares.
We set this up as a specialization of the comma category `comma L R`,
where `L` and `R` are both the identity functor.

We also define the typeclass `has_lift`, representing a choice of a lift
of a commutative square (that is, a diagonal morphism making the two triangles commute).

## Tags

comma, arrow
-/

namespace category_theory

universes v u -- morphism levels before object levels. See note [category_theory universes].
variables {T : Type u} [category.{v} T]

section
variables (T)

/-- The arrow category of `T` has as objects all morphisms in `T` and as morphisms commutative
     squares in `T`. -/
@[derive category]
def arrow := comma.{v v v} (𝟭 T) (𝟭 T)

-- Satisfying the inhabited linter
instance arrow.inhabited [inhabited T] : inhabited (arrow T) :=
{ default := show comma (𝟭 T) (𝟭 T), from default (comma (𝟭 T) (𝟭 T)) }

end

namespace arrow

@[simp] lemma id_left (f : arrow T) : comma_morphism.left (𝟙 f) = 𝟙 (f.left) := rfl
@[simp] lemma id_right (f : arrow T) : comma_morphism.right (𝟙 f) = 𝟙 (f.right) := rfl

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

theorem mk_injective (A B : T) :
  function.injective (arrow.mk : (A ⟶ B) → arrow T) :=
λ f g h, by { cases h, refl }

theorem mk_inj (A B : T) {f g : A ⟶ B} : arrow.mk f = arrow.mk g ↔ f = g :=
(mk_injective A B).eq_iff
instance {X Y : T} : has_coe (X ⟶ Y) (arrow T) := ⟨mk⟩

/-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
    category. -/
@[simps]
def hom_mk {f g : arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right}
  (w : u ≫ g.hom = f.hom ≫ v) : f ⟶ g :=
{ left := u,
  right := v,
  w' := w }

/-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/
@[simps]
def hom_mk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q}
  (w : u ≫ g = f ≫ v) : arrow.mk f ⟶ arrow.mk g :=
{ left := u,
  right := v,
  w' := w }

@[simp, reassoc] lemma w {f g : arrow T} (sq : f ⟶ g) : sq.left ≫ g.hom = f.hom ≫ sq.right := sq.w

-- `w_mk_left` is not needed, as it is a consequence of `w` and `mk_hom`.
@[simp, reassoc] lemma 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

lemma is_iso_of_iso_left_of_is_iso_right
  {f g : arrow T} (ff : f ⟶ g) [is_iso ff.left] [is_iso ff.right] : is_iso ff :=
{ out := ⟨⟨inv ff.left, inv ff.right⟩,
          by { ext; dsimp; simp only [is_iso.hom_inv_id] },
          by { ext; dsimp; simp only [is_iso.inv_hom_id] }⟩ }

/-- Create an isomorphism between arrows,
by providing isomorphisms between the domains and codomains,
and a proof that the square commutes. -/
@[simps] def iso_mk {f g : arrow T}
  (l : f.left ≅ g.left) (r : f.right ≅ g.right) (h : l.hom ≫ g.hom = f.hom ≫ r.hom) :
  f ≅ g :=
comma.iso_mk l r h

section

variables {f g : arrow T} (sq : f ⟶ g)

instance is_iso_left [is_iso sq] : is_iso sq.left :=
{ out := ⟨(inv sq).left, by simp only [← comma.comp_left, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_left, eq_self_iff_true, and_self]⟩ }

instance is_iso_right [is_iso sq] : is_iso sq.right :=
{ out := ⟨(inv sq).right, by simp only [← comma.comp_right, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_right, eq_self_iff_true, and_self]⟩ }

instance mono_left [mono sq] : mono sq.left :=
{ right_cancellation := λ Z φ ψ h, begin
    let aux : (Z ⟶ f.left) → (arrow.mk (𝟙 Z) ⟶ f) := λ φ, { left := φ, right := φ ≫ f.hom },
    show (aux φ).left = (aux ψ).left,
    congr' 1,
    rw ← cancel_mono sq,
    ext,
    { exact h },
    { simp only [comma.comp_right, category.assoc, ← arrow.w],
      simp only [← category.assoc, h], },
  end }

instance epi_right [epi sq] : epi sq.right :=
{ left_cancellation := λ Z φ ψ h, begin
    let aux : (g.right ⟶ Z) → (g ⟶ arrow.mk (𝟙 Z)) := λ φ, { right := φ, left := g.hom ≫ φ },
    show (aux φ).right = (aux ψ).right,
    congr' 1,
    rw ← cancel_epi sq,
    ext,
    { simp only [comma.comp_left, category.assoc, arrow.w_assoc, h], },
    { exact h },
  end }

end

/-- 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] lemma 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)

/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq`
in terms of the inverse of `i`. -/
lemma square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : arrow T) (sq : arrow.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]

/-- A lift of a commutative square is a diagonal morphism making the two triangles commute. -/
@[ext] structure lift_struct {f g : arrow T} (sq : f ⟶ g) :=
(lift : f.right ⟶ g.left)
(fac_left' : f.hom ≫ lift = sq.left . obviously)
(fac_right' : lift ≫ g.hom = sq.right . obviously)

restate_axiom lift_struct.fac_left'
restate_axiom lift_struct.fac_right'

instance lift_struct_inhabited {X : T} : inhabited (lift_struct (𝟙 (arrow.mk (𝟙 X)))) :=
⟨⟨𝟙 _, category.id_comp _, category.comp_id _⟩⟩
{'fraction_non_alphanumeric': 0.1496149614961496, 'fraction_numerical': 0.0046004600460046, 'mean_word_length': 3.035512510088781, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6176922', 'n_tokens_mistral': 4326, 'n_tokens_neox': 4082, 'n_words': 1553}