[Merged by Bors] - feat(CategoryTheory): the class of morphisms given by a family of maps

Mathlib/CategoryTheory/Comma/Arrow.lean

@@ -91,6 +91,35 @@ theorem mk_inj (A B : T) {f g : A ⟶ B} : Arrow.mk f = Arrow.mk g ↔ f = g :=
 instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
   coe := mk
 
+lemma mk_eq_mk_iff {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 := 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]
+
+lemma ext {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 :=
+  (mk_eq_mk_iff _ _).2 (by aesop)
+
+@[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)
+
+@[simp]
+lemma arrow_mk_eqToHom_comp {X' X Y : T} (f : X ⟶ Y) (h : X' = X) :
+    Arrow.mk (eqToHom h ≫ f) = Arrow.mk f :=
+  ext h rfl (by simp)
+
 /-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
     category. -/
 @[simps]
@@ -294,16 +323,6 @@ def rightFunc : Arrow C ⥤ C :=
 @[simps]
 def leftToRight : (leftFunc : Arrow C ⥤ C) ⟶ rightFunc where app f := f.hom
 
-lemma ext {f g : Arrow C}
-    (h₁ : f.left = g.left) (h₂ : f.right = g.right)
-    (h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom h₂.symm) : f = g := by
-  obtain ⟨X, Y, f⟩ := f
-  obtain ⟨X', Y', g⟩ := g
-  obtain rfl : X = X' := h₁
-  obtain rfl : Y = Y' := h₂
-  obtain rfl : f = g := by simpa using h₃
-  rfl
-
 end Arrow
 
 namespace Functor
@@ -315,10 +334,7 @@ variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 /-- A functor `C ⥤ D` induces a functor between the corresponding arrow categories. -/
 @[simps]
 def mapArrow (F : C ⥤ D) : Arrow C ⥤ Arrow D where
-  obj a :=
-    { left := F.obj a.left
-      right := F.obj a.right
-      hom := F.map a.hom }
+  obj a := Arrow.mk (F.map a.hom)
   map f :=
     { left := F.map f.left
       right := F.map f.right
@@ -355,9 +371,11 @@ instance isEquivalence_mapArrow (F : C ⥤ D) [IsEquivalence F] :
 
 end Functor
 
+variable {C D : Type*} [Category C] [Category D]
+
 /-- The images of `f : Arrow C` by two isomorphic functors `F : C ⥤ D` are
 isomorphic arrows in `D`. -/
-def Arrow.isoOfNatIso {C D : Type*} [Category C] [Category D] {F G : C ⥤ D} (e : F ≅ G)
+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)
 
@@ -382,4 +400,14 @@ def Arrow.discreteEquiv (S : Type u) : Arrow (Discrete S) ≃ S where
     rfl
   right_inv _ := rfl
 
+/-- 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)
+
 end CategoryTheory

Mathlib/CategoryTheory/Comma/CardinalArrow.lean

@@ -77,17 +77,16 @@ noncomputable def Arrow.shrinkHomsEquiv (C : Type u) [Category.{v} C] [LocallySm
     Arrow.{w} (ShrinkHoms C) ≃ Arrow C where
   toFun := (ShrinkHoms.equivalence C).inverse.mapArrow.obj
   invFun := (ShrinkHoms.equivalence C).functor.mapArrow.obj
-  left_inv _ := by simp [Functor.mapArrow]; rfl
-  right_inv _ := by simp [Functor.mapArrow]; rfl
+  left_inv _ := by simp
+  right_inv _ := by simp
 
 /-- The bijection `Arrow (Shrink C) ≃ Arrow C`. -/
 noncomputable def Arrow.shrinkEquiv (C : Type u) [Category.{v} C] [Small.{w} C] :
     Arrow (Shrink.{w} C) ≃ Arrow C where
   toFun := (Shrink.equivalence C).inverse.mapArrow.obj
   invFun := (Shrink.equivalence C).functor.mapArrow.obj
-  left_inv f := by
-    refine Arrow.ext (Equiv.apply_symm_apply _ _)
-      ((Equiv.apply_symm_apply _ _)) (by simp; rfl)
+  left_inv _ := Arrow.ext (Equiv.apply_symm_apply _ _)
+      ((Equiv.apply_symm_apply _ _)) (by simp ; rfl)
   right_inv _ := Arrow.ext (by simp [Shrink.equivalence])
     (by simp [Shrink.equivalence]) (by simp [Shrink.equivalence])
 

Mathlib/CategoryTheory/Localization/Triangulated.lean

@@ -136,7 +136,7 @@ lemma distinguished_cocone_triangle {X Y : D} (f : X ⟶ Y) :
     (Iso.refl _) e.inv.w.symm (by simp) ?_
   dsimp
   simp only [assoc, id_comp, ← Functor.map_comp, ← Arrow.comp_left, e.hom_inv_id, Arrow.id_left,
-    Functor.mapArrow_obj_left, Functor.map_id, comp_id]
+    Functor.mapArrow_obj, Arrow.mk_left, Functor.map_id, comp_id]
 
 section
 variable [W.IsCompatibleWithTriangulation]

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -115,14 +115,58 @@ lemma monotone_map (F : C ⥤ D) :
   intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
   exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩
 
-lemma of_eq (P : MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : P f)
+section
+
+variable (P : MorphismProperty C)
+
+/-- The set in `Set (Arrow C)` which corresponds to `P : MorphismProperty C`. -/
+def toSet : Set (Arrow C) := setOf (fun f ↦ P f.hom)
+
+/-- 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
+
+lemma homFamily_apply (f : P.toSet) : P.homFamily f = f.1.hom := rfl
+
+@[simp]
+lemma homFamily_arrow_mk {X Y : C} (f : X ⟶ Y) (hf : P f) :
+    P.homFamily ⟨Arrow.mk f, hf⟩ = f := rfl
+
+@[simp]
+lemma arrow_mk_mem_toSet_iff {X Y : C} (f : X ⟶ Y) : Arrow.mk f ∈ P.toSet ↔ P f := Iff.rfl
+
+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' = eqToHom hX.symm ≫ f ≫ eqToHom hY) :
     P f' := by
-  obtain rfl := hX
-  obtain rfl := hY
-  obtain rfl : f' = f := by simpa using h
-  exact hf
+  rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
+  rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]
+
+end
+
+/-- 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)
+
+lemma ofHoms_iff {ι : 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) := 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
+
+@[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)⟩
 
 /-- 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`