feat(CategoryTheory/ComposableArrows): compositions of 1 or 2 morphisms (#31588)

Author: joelriou

Mathlib.lean

@@ -2286,6 +2286,8 @@ public import Mathlib.CategoryTheory.Comma.StructuredArrow.Final
 public import Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
 public import Mathlib.CategoryTheory.Comma.StructuredArrow.Small
 public import Mathlib.CategoryTheory.ComposableArrows.Basic
+public import Mathlib.CategoryTheory.ComposableArrows.One
+public import Mathlib.CategoryTheory.ComposableArrows.Two
 public import Mathlib.CategoryTheory.ConcreteCategory.Basic
 public import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 public import Mathlib.CategoryTheory.ConcreteCategory.BundledHom

Mathlib/CategoryTheory/ComposableArrows/One.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.ComposableArrows.Basic
+
+/-!
+# Functors to `ComposableArrows C 1`
+
+-/
+
+@[expose] public section
+
+universe v u
+
+namespace CategoryTheory
+
+namespace ComposableArrows
+
+variable (C : Type u) [Category.{v} C]
+
+/-- The functor `ComposableArrows C n ⥤ ComposableArrows C 1`
+which sends `S` to `mk₁ (S.map' i j)` when `i`, `j` and `n`
+are such that `i ≤ j` and `j ≤ n`. -/
+@[simps]
+noncomputable def functorArrows (i j n : ℕ) (hij : i ≤ j := by cutsat)
+      (hj : j ≤ n := by cutsat) :
+    ComposableArrows C n ⥤ ComposableArrows C 1 where
+  obj S := mk₁ (S.map' i j)
+  map {S S'} φ := homMk₁ (φ.app _) (φ.app _) (φ.naturality _)
+
+/-- The natural transformation `functorArrows C i j n ⟶ functorArrows C i' j' n`
+when `i ≤ i'` and `j ≤ j'`. -/
+@[simps]
+noncomputable def mapFunctorArrows (i j i' j' n : ℕ)
+    (_ : i ≤ j := by cutsat) (_ : i' ≤ j' := by cutsat)
+    (_ : i ≤ i' := by cutsat) (_ : j ≤ j' := by cutsat)
+    (_ : j' ≤ n := by cutsat) :
+    functorArrows C i j n ⟶ functorArrows C i' j' n where
+  app S := homMk₁ (S.map' i i') (S.map' j j')
+    (by simp [← Functor.map_comp])
+
+end ComposableArrows
+
+end CategoryTheory

Mathlib/CategoryTheory/ComposableArrows/Two.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.ComposableArrows.Basic
+
+/-!
+# API for compositions of two arrows
+
+Given morphisms `f : i ⟶ j`, `g : j ⟶ k`, and `fg : i ⟶ k` in a category `C`
+such that `f ≫ g = fg`, we define maps `twoδ₂Toδ₁ : mk₁ f ⟶ mk₁ fg` and
+`twoδ₁Toδ₀ : mk₁ fg ⟶ mk₁ g` in the category `ComposableArrows C 1`.
+The names are justified by the fact that `ComposableArrow.mk₂ f g`
+can be thought of as a `2`-simplex in the simplicial set `nerve C`,
+and its faces (numbered from `0` to `2`) are respectively `mk₁ g`,
+`mk₁ fg` and `mk₁ f`.
+
+-/
+
+@[expose] public section
+
+universe v u
+
+namespace CategoryTheory
+
+namespace ComposableArrows
+
+variable {C : Type u} [Category.{v} C]
+  {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : f ≫ g = fg)
+
+/-- The morphism `mk₁ f ⟶ mk₁ fg` when `f ≫ g = fg` for some morphism `g`. -/
+def twoδ₂Toδ₁ :
+    mk₁ f ⟶ mk₁ fg :=
+  homMk₁ (𝟙 _) g
+
+@[simp]
+lemma twoδ₂Toδ₁_app_zero :
+    (twoδ₂Toδ₁ f g fg h).app 0 = 𝟙 _ := rfl
+
+@[simp]
+lemma twoδ₂Toδ₁_app_one :
+    (twoδ₂Toδ₁ f g fg h).app 1 = g := rfl
+
+/-- The morphism `mk₁ fg ⟶ mk₁ g` when `f ≫ g = fg` for some morphism `f`. -/
+def twoδ₁Toδ₀ :
+    mk₁ fg ⟶ mk₁ g :=
+  homMk₁ f (𝟙 _)
+
+@[simp]
+lemma twoδ₁Toδ₀_app_zero :
+    (twoδ₁Toδ₀ f g fg h).app 0 = f := rfl
+
+@[simp]
+lemma twoδ₁Toδ₀_app_one :
+    (twoδ₁Toδ₀ f g fg h).app 1 = 𝟙 _ := rfl
+
+end ComposableArrows
+
+end CategoryTheory