feat(AlgebraicTopology): edges and "triangles" in the nerve of a category (#31274)

We study `Edge` and `Edge.CompStruct` in the case of the nerve of a category. In particular, `Edge.CompStruct` are related to commutative triangles.

Author: joelriou

Mathlib/AlgebraicTopology/SimplicialNerve.lean

@@ -120,7 +120,7 @@ namespace SimplicialCategory
 variable {J : Type*} [LinearOrder J]
 
 /-- The hom simplicial set of the simplicial category structure on `SimplicialThickening J` -/
-abbrev Hom (i j : SimplicialThickening J) : SSet := (nerve (i ⟶ j))
+abbrev Hom (i j : SimplicialThickening J) : SSet := nerve (i ⟶ j)
 
 /-- The identity of the simplicial category structure on `SimplicialThickening J` -/
 abbrev id (i : SimplicialThickening J) : 𝟙_ SSet ⟶ Hom i i :=
@@ -155,7 +155,8 @@ noncomputable instance (J : Type*) [LinearOrder J] :
   Hom := Hom
   id := id
   comp := comp
-  homEquiv {i j} := (nerveEquiv _).symm.trans (SSet.unitHomEquiv _).symm
+  homEquiv {i j} :=
+    nerveEquiv.symm.trans (SSet.unitHomEquiv (SimplicialCategory.Hom i j)).symm
 
 /-- Auxiliary definition for `SimplicialThickening.functorMap` -/
 def orderHom {J K : Type*} [LinearOrder J] [LinearOrder K] (f : J →o K) :
@@ -169,6 +170,8 @@ noncomputable abbrev functorMap {J K : Type u} [LinearOrder J] [LinearOrder K]
     by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)⟩
   map f := ⟨⟨Set.image_mono f.1.1⟩⟩
 
+attribute [local simp] nerveMap_app
+
 /--
 The simplicial thickening defines a functor from the category of linear orders to the category of
 simplicial categories

Mathlib/AlgebraicTopology/SimplicialSet/CompStruct.lean

@@ -74,6 +74,19 @@ lemma tgt_eq (e : Edge x₀ x₁) : X.δ 0 e.edge = x₁ := Truncated.Edge.tgt_e
 lemma ext {e e' : Edge x₀ x₁} (h : e.edge = e'.edge) :
     e = e' := Truncated.Edge.ext h
 
+section
+
+variable (edge : X _⦋1⦌) (src_eq : X.δ 1 edge = x₀ := by cat_disch)
+  (tgt_eq : X.δ 0 edge = x₁ := by cat_disch)
+
+/-- Constructor for edges in a simplicial set. -/
+def mk : Edge x₀ x₁ := ofTruncated { edge := edge }
+
+@[simp]
+lemma mk_edge : (mk edge src_eq tgt_eq).edge = edge := rfl
+
+end
+
 variable (x₀) in
 /-- The constant edge on a `0`-simplex. -/
 def id : Edge x₀ x₀ := ofTruncated (.id _)
@@ -86,15 +99,18 @@ lemma id_edge : (id x₀).edge = X.σ 0 x₀ := rfl
 def map (e : Edge x₀ x₁) (f : X ⟶ Y) : Edge (f.app _ x₀) (f.app _ x₁) :=
   ofTruncated (e.toTruncated.map ((truncation 2).map f))
 
+@[simp]
+lemma map_edge (e : Edge x₀ x₁) (f : X ⟶ Y) :
+    (e.map f).edge = f.app _ e.edge := rfl
+
 variable (x₀) in
 @[simp]
 lemma map_id (f : X ⟶ Y) :
     (Edge.id x₀).map f = Edge.id (f.app _ x₀) :=
   Truncated.Edge.map_id _ _
 
 /-- The edge given by a `1`-simplex. -/
-def mk' (s : X _⦋1⦌) : Edge (X.δ 1 s) (X.δ 0 s) :=
-  .ofTruncated (Truncated.Edge.mk' (X := (truncation 2).obj X) s)
+def mk' (s : X _⦋1⦌) : Edge (X.δ 1 s) (X.δ 0 s) := mk s
 
 @[simp]
 lemma mk'_edge (s : X _⦋1⦌) : (mk' s).edge = s := rfl
@@ -128,9 +144,23 @@ def toTruncated (h : CompStruct e₀₁ e₁₂ e₀₂) :
     Truncated.Edge.CompStruct e₀₁.toTruncated e₁₂.toTruncated e₀₂.toTruncated :=
   h
 
+section
+
+variable (h : CompStruct e₀₁ e₁₂ e₀₂)
+
 /-- The underlying `2`-simplex in a structure `SSet.Edge.CompStruct`. -/
-def simplex (h : CompStruct e₀₁ e₁₂ e₀₂) : X _⦋2⦌ :=
-    h.toTruncated.simplex
+def simplex : X _⦋2⦌ := h.toTruncated.simplex
+
+@[simp]
+lemma d₂ : X.δ 2 h.simplex = e₀₁.edge := Truncated.Edge.CompStruct.d₂ h
+
+@[simp]
+lemma d₀ : X.δ 0 h.simplex = e₁₂.edge := Truncated.Edge.CompStruct.d₀ h
+
+@[simp]
+lemma d₁ : X.δ 1 h.simplex = e₀₂.edge := Truncated.Edge.CompStruct.d₁ h
+
+end
 
 section
 

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -73,14 +73,14 @@ noncomputable def lift {X : SSet.{u}} (sx : StrictSegal X) {n}
     arrow_src := fun i ↦ by
       let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
         strArrowMk₂ (⦋0⦌.const _ i.castSucc) :=
-          StructuredArrow.homMk (δ 1).op
+          StructuredArrow.homMk (SimplexCategory.δ 1).op
           (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
       exact congr_fun (s.w φ) x
     arrow_tgt := fun i ↦ by
       dsimp
       let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
           strArrowMk₂ (⦋0⦌.const _ i.succ) :=
-        StructuredArrow.homMk (δ 0).op
+        StructuredArrow.homMk (SimplexCategory.δ 0).op
           (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
       exact congr_fun (s.w φ) x }
 
@@ -131,7 +131,7 @@ lemma fac_aux₂ {n : ℕ}
       let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by cutsat⟩ ⟨i + k, by cutsat⟩ (by simp))
       let β₀ : α ⟶ α₀ := StructuredArrow.homMk ((mkOfSucc 1).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))
-      let β₁ : α ⟶ α₁ := StructuredArrow.homMk ((δ 1).op) (Quiver.Hom.unop_inj
+      let β₁ : α ⟶ α₁ := StructuredArrow.homMk ((SimplexCategory.δ 1).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))
       let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((mkOfSucc 0).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))

Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

@@ -167,7 +167,8 @@ def OneTruncation₂.ofNerve₂.natIso :
         ComposableArrows.obj', Fin.zero_eta, Fin.isValue, ReflQuiv.comp_eq_comp, Nat.reduceAdd,
         op_map, Quiver.Hom.unop_op, nerve_map, SimplexCategory.toCat_map, ReflPrefunctor.comp_obj,
         ReflPrefunctor.comp_map]
-      simp [nerveHomEquiv, ReflQuiv.isoOfEquiv, ReflQuiv.isoOfQuivIso, Quiv.isoOfEquiv])
+      simp [nerveMap_app, nerveHomEquiv, ReflQuiv.isoOfEquiv,
+        ReflQuiv.isoOfQuivIso, Quiv.isoOfEquiv])
 
 end
 

Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.AlgebraicTopology.SimplicialSet.Basic
+public import Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
 public import Mathlib.CategoryTheory.ComposableArrows.Basic
 
 /-!
@@ -31,19 +31,21 @@ universe v u
 namespace CategoryTheory
 
 /-- The nerve of a category -/
-@[simps]
+@[simps -isSimp]
 def nerve (C : Type u) [Category.{v} C] : SSet.{max u v} where
   obj Δ := ComposableArrows C (Δ.unop.len)
   map f x := x.whiskerLeft (SimplexCategory.toCat.map f.unop)
   -- `aesop` can prove these but is slow, help it out:
   map_id _ := rfl
   map_comp _ _ := rfl
 
+attribute [simp] nerve_obj
+
 instance {C : Type*} [Category C] {Δ : SimplexCategoryᵒᵖ} : Category ((nerve C).obj Δ) :=
   (inferInstance : Category (ComposableArrows C (Δ.unop.len)))
 
 /-- Given a functor `C ⥤ D`, we obtain a morphism `nerve C ⟶ nerve D` of simplicial sets. -/
-@[simps]
+@[simps -isSimp]
 def nerveMap {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) : nerve C ⟶ nerve D :=
   { app := fun _ => (F.mapComposableArrows _).obj }
 
@@ -54,9 +56,9 @@ def nerveFunctor : Cat.{v, u} ⥤ SSet where
   map F := nerveMap F
 
 /-- The 0-simplices of the nerve of a category are equivalent to the objects of the category. -/
-def nerveEquiv (C : Type u) [Category.{v} C] : nerve C _⦋0⦌ ≃ C where
+def nerveEquiv {C : Type u} [Category.{v} C] : ComposableArrows C 0 ≃ C where
   toFun f := f.obj ⟨0, by omega⟩
-  invFun f := (Functor.const _).obj f
+  invFun f := ComposableArrows.mk₀ f
   left_inv f := ComposableArrows.ext₀ rfl
 
 namespace nerve
@@ -71,17 +73,17 @@ def representableBy {n : ℕ} (α : Type u) [Preorder α] (e : α ≃o Fin (n +
       right_inv F := Functor.ext (fun x ↦ by simp) }
   homEquiv_comp _ _ := rfl
 
-variable {C : Type*} [Category C] {n : ℕ}
+variable {C : Type u} [Category.{v} C] {n : ℕ}
 
-lemma δ_obj {n : ℕ} (i : Fin (n + 2)) (x : (nerve C) _⦋n + 1⦌) (j : Fin (n + 1)) :
+lemma δ_obj {n : ℕ} (i : Fin (n + 2)) (x : ComposableArrows C (n + 1)) (j : Fin (n + 1)) :
     ((nerve C).δ i x).obj j = x.obj (i.succAbove j) :=
   rfl
 
-lemma σ_obj {n : ℕ} (i : Fin (n + 1)) (x : (nerve C) _⦋n⦌) (j : Fin (n + 2)) :
+lemma σ_obj {n : ℕ} (i : Fin (n + 1)) (x : ComposableArrows C n) (j : Fin (n + 2)) :
     ((nerve C).σ i x).obj j = x.obj (i.predAbove j) :=
   rfl
 
-lemma δ₀_eq {x : nerve C _⦋n + 1⦌} : (nerve C).δ (0 : Fin (n + 2)) x = x.δ₀ := rfl
+lemma δ₀_eq {x : ComposableArrows C (n + 1)} : (nerve C).δ (0 : Fin (n + 2)) x = x.δ₀ := rfl
 
 lemma σ₀_mk₀_eq (x : C) : (nerve C).σ (0 : Fin 1) (.mk₀ x) = .mk₁ (𝟙 x) :=
   ComposableArrows.ext₁ rfl rfl (by simp; rfl)
@@ -107,6 +109,115 @@ lemma ext_of_isThin [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ} {x y : (nerve
     x = y :=
   ComposableArrows.ext (by simp [h]) (by subsingleton)
 
+open SSet
+
+@[simp]
+lemma left_edge {x y : ComposableArrows C 0} (e : (nerve C).Edge x y) :
+    ComposableArrows.left (n := 1) e.edge = nerveEquiv x := by
+  simp only [← e.src_eq]
+  rfl
+
+@[simp]
+lemma right_edge {x y : ComposableArrows C 0} (e : (nerve C).Edge x y) :
+    ComposableArrows.right  (n := 1) e.edge = nerveEquiv y := by
+  simp only [← e.tgt_eq]
+  rfl
+
+lemma δ₂_two (x : ComposableArrows C 2) :
+    (nerve C).δ 2 x = .mk₁ (x.map' 0 1) :=
+  ComposableArrows.ext₁ rfl rfl (by cat_disch)
+
+lemma δ₂_zero (x : ComposableArrows C 2) :
+    (nerve C).δ 0 x = .mk₁ (x.map' 1 2) :=
+  ComposableArrows.ext₁ rfl rfl (by cat_disch)
+
+section
+
+attribute [local ext (iff := false)] ComposableArrows.ext₀ ComposableArrows.ext₁
+
+/-- Bijection between edges in the nerve of category and morphisms in the category. -/
+def homEquiv {x y : ComposableArrows C 0} :
+    (nerve C).Edge x y ≃ (nerveEquiv x ⟶ nerveEquiv y) where
+  toFun e := eqToHom (by simp) ≫ e.edge.hom ≫ eqToHom (by simp)
+  invFun f := .mk (ComposableArrows.mk₁ f) (ComposableArrows.ext₀ rfl) (ComposableArrows.ext₀ rfl)
+  left_inv e := by cat_disch
+  right_inv f := by simp
+
+lemma mk₁_homEquiv_apply {x y : ComposableArrows C 0} (e : (nerve C).Edge x y) :
+    ComposableArrows.mk₁ (homEquiv e) = ComposableArrows.mk₁ e.edge.hom := by
+  simp [homEquiv, ComposableArrows.mk₁_eqToHom_comp, ComposableArrows.mk₁_comp_eqToHom]
+
+/-- Constructor for edges in the nerve of a category. (See also `homEquiv`.) -/
+def edgeMk {x y : C} (f : x ⟶ y) : (nerve C).Edge (nerveEquiv.symm x) (nerveEquiv.symm y) :=
+  Edge.mk (ComposableArrows.mk₁ f)
+
+@[simp]
+lemma edgeMk_edge {x y : C} (f : x ⟶ y) : (edgeMk f).edge = ComposableArrows.mk₁ f := rfl
+
+lemma edgeMk_surjective {x y : C} :
+    Function.Surjective (edgeMk : (x ⟶ y) → _) :=
+  fun e ↦ ⟨eqToHom (by simp) ≫ homEquiv e ≫ eqToHom (by simp), by cat_disch⟩
+
+@[simp]
+lemma homEquiv_edgeMk {x y : C} (f : x ⟶ y) :
+    homEquiv (edgeMk f) = f :=
+  homEquiv.symm.injective (by cat_disch)
+
+lemma homEquiv_id (x : ComposableArrows C 0) :
+    homEquiv (Edge.id x) = 𝟙 _ := by
+  obtain ⟨x, rfl⟩ := nerveEquiv.symm.surjective x
+  dsimp [homEquiv]
+  cat_disch
+
+lemma nonempty_compStruct_iff {x₀ x₁ x₂ : C}
+    (f₀₁ : x₀ ⟶ x₁) (f₁₂ : x₁ ⟶ x₂) (f₀₂ : x₀ ⟶ x₂) :
+    Nonempty (Edge.CompStruct (edgeMk f₀₁) (edgeMk f₁₂) (edgeMk f₀₂)) ↔
+      f₀₁ ≫ f₁₂ = f₀₂ := by
+  let h' : Edge.CompStruct (edgeMk f₀₁) (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
+      Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂)
+        (by cat_disch) (by cat_disch) (by cat_disch)
+  refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩
+  rw [← Arrow.mk_inj]
+  apply ComposableArrows.arrowEquiv.symm.injective
+  convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
+  · exact (h'.d₁).symm
+  · exact (h.d₁).symm
+  · have h₀ := h.d₀
+    have h₂ := h.d₂
+    have h'₀ := h'.d₀
+    have h'₂ := h'.d₂
+    simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂
+    exact congr_arg _ (ComposableArrows.ext₂_of_arrow
+      (ComposableArrows.arrowEquiv.symm.injective
+        (by simp [-Edge.CompStruct.d₂, h'₂, ← h₂]))
+      (ComposableArrows.arrowEquiv.symm.injective
+        (by simp [-Edge.CompStruct.d₀, h'₀, ← h₀])))
+
+lemma homEquiv_comp {x₀ x₁ x₂ : ComposableArrows C 0}
+    {e₀₁ : (nerve C).Edge x₀ x₁}
+    {e₁₂ : (nerve C).Edge x₁ x₂} {e₀₂ : (nerve C).Edge x₀ x₂}
+    (h : Edge.CompStruct e₀₁ e₁₂ e₀₂) :
+    homEquiv e₀₁ ≫ homEquiv e₁₂ = homEquiv e₀₂ := by
+  obtain ⟨x₀, rfl⟩ := nerveEquiv.symm.surjective x₀
+  obtain ⟨x₁, rfl⟩ := nerveEquiv.symm.surjective x₁
+  obtain ⟨x₂, rfl⟩ := nerveEquiv.symm.surjective x₂
+  obtain ⟨f₀₁, rfl⟩ := edgeMk_surjective e₀₁
+  obtain ⟨f₁₂, rfl⟩ := edgeMk_surjective e₁₂
+  obtain ⟨f₀₂, rfl⟩ := edgeMk_surjective e₀₂
+  convert (nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩ <;> apply homEquiv_edgeMk
+
+lemma σ_zero_nerveEquiv_symm (x : C) :
+    (nerve C).σ 0 (nerveEquiv.symm x) = ComposableArrows.mk₁ (𝟙 x) := by
+  cat_disch
+
+@[simp]
+lemma homEquiv_edgeMk_map_nerveMap {D : Type u} [Category.{v} D] {x y : C}
+    (f : x ⟶ y) (F : C ⥤ D) :
+    homEquiv ((edgeMk f).map (nerveMap F)) = F.map f := by
+  simp [homEquiv, nerveMap_app]
+
+end
+
 end nerve
 
 end CategoryTheory

Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

@@ -449,7 +449,7 @@ instance nerveFunctor₂.full : nerveFunctor₂.{u, u}.Full where
         simp [uF', nerveFunctor₂, SSet.truncation, ReflQuiv.comp_eq_comp, uF, Fhk] <;>
         [let ι := ι0₂; let ι := ι1₂; let ι := ι2₂] <;>
       · replace := congr_arg (·.obj 0) (congr_fun (F.naturality ι.op) hk)
-        dsimp [oneTruncation₂, ComposableArrows.left, SimplicialObject.truncation,
+        dsimp [nerve_map, oneTruncation₂, ComposableArrows.left, SimplicialObject.truncation,
           nerveFunctor₂, SSet.truncation, forget₂, HasForget₂.forget₂] at this ⊢
         convert this.symm
         apply ComposableArrows.ext₀; rfl

Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

@@ -202,8 +202,8 @@ lemma spine_δ_vertex_lt (hij : i.castSucc < j) :
       (sx.spineToSimplex (m + 1) _ f))).vertex i = f.vertex i.castSucc := by
   rw [spine_vertex, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp,
     SimplexCategory.const_comp, spineToSimplex_vertex]
-  dsimp only [δ, len_mk, mkHom, Hom.toOrderHom_mk, Fin.succAboveOrderEmb_apply,
-    OrderEmbedding.toOrderHom_coe]
+  dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
+    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]
   rw [Fin.succAbove_of_castSucc_lt j i hij]
 
 /-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
@@ -214,8 +214,8 @@ lemma spine_δ_vertex_ge (hij : j ≤ i.castSucc) :
       (sx.spineToSimplex (m + 1) _ f))).vertex i = f.vertex i.succ := by
   rw [spine_vertex, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp,
     SimplexCategory.const_comp, spineToSimplex_vertex]
-  dsimp only [δ, len_mk, mkHom, Hom.toOrderHom_mk, Fin.succAboveOrderEmb_apply,
-    OrderEmbedding.toOrderHom_coe]
+  dsimp only [SimplexCategory.δ, len_mk, mkHom, Hom.toOrderHom_mk,
+    Fin.succAboveOrderEmb_apply, OrderEmbedding.toOrderHom_coe]
   rw [Fin.succAbove_of_le_castSucc j i hij]
 
 variable {i : Fin m} {j : Fin (m + 2)}

Mathlib/CategoryTheory/ComposableArrows/Basic.lean

@@ -280,6 +280,18 @@ lemma ext₁ {F G : ComposableArrows C 1}
 lemma mk₁_surjective (X : ComposableArrows C 1) : ∃ (X₀ X₁ : C) (f : X₀ ⟶ X₁), X = mk₁ f :=
   ⟨_, _, X.map' 0 1, ext₁ rfl rfl (by simp)⟩
 
+lemma mk₁_eqToHom_comp {X₀' X₀ X₁ : C} (h : X₀' = X₀) (f : X₀ ⟶ X₁) :
+    ComposableArrows.mk₁ (eqToHom h ≫ f) = ComposableArrows.mk₁ f := by
+  cat_disch
+
+lemma mk₁_comp_eqToHom {X₀ X₁ X₁' : C} (f : X₀ ⟶ X₁) (h : X₁ = X₁') :
+    ComposableArrows.mk₁ (f ≫ eqToHom h) = ComposableArrows.mk₁ f := by
+  cat_disch
+
+lemma mk₁_hom (X : ComposableArrows C 1) :
+    mk₁ X.hom = X :=
+  ext₁ rfl rfl (by simp)
+
 /-- The bijection between `ComposableArrows C 1` and `Arrow C`. -/
 @[simps]
 def arrowEquiv : ComposableArrows C 1 ≃ Arrow C where
@@ -606,6 +618,18 @@ lemma mk₂_surjective (X : ComposableArrows C 2) :
     ∃ (X₀ X₁ X₂ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂), X = mk₂ f₀ f₁ :=
   ⟨_, _, _, X.map' 0 1, X.map' 1 2, ext₂ rfl rfl rfl (by simp) (by simp)⟩
 
+lemma ext₂_of_arrow {f g : ComposableArrows C 2}
+    (h₀₁ : Arrow.mk (f.map' 0 1) = Arrow.mk (g.map' 0 1))
+    (h₁₂ : Arrow.mk (f.map' 1 2) = Arrow.mk (g.map' 1 2)) : f = g := by
+  obtain ⟨x₀, x₁, x₂, f, f', rfl⟩ := mk₂_surjective f
+  obtain ⟨y₀, y₁, y₂, g, g', rfl⟩ := mk₂_surjective g
+  obtain rfl : x₀ = y₀ := congr_arg Arrow.leftFunc.obj h₀₁
+  obtain rfl : x₁ = y₁ := congr_arg Arrow.rightFunc.obj h₀₁
+  obtain rfl : x₂ = y₂ := congr_arg Arrow.rightFunc.obj h₁₂
+  obtain rfl : f = g := by rwa [← Arrow.mk_inj]
+  obtain rfl : f' = g' := by rwa [← Arrow.mk_inj]
+  rfl
+
 section
 
 variable