feat(AlgebraicTopology/Quasicategory): define the homotopy category of a 2-truncated quasicategory (#31630)

The homotopy category `HomotopyCategory₂ A` of a 2-truncated quasicategory `A` has:
* objects given by the vertices of `A`
* morphisms given by (left) homotopy classes of edges between two vertices.

From: https://github.com/emilyriehl/infinity-cosmos

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: 3 people

Mathlib/AlgebraicTopology/Quasicategory/TwoTruncated.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Julian Komaromy. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julian Komaromy
+Authors: Julian Komaromy, Joël Riou
 -/
 module
 
@@ -18,6 +18,15 @@ and the left and right homotopy relations `HomotopicL` and `HomotopicR` on the e
 We prove that for 2-truncated quasicategories, both homotopy relations are equivalence
 relations, and that the left and right homotopy relations coincide.
 
+For a 2-truncated quasicategory `A`, we define a category `HomotopyCategory₂ A` whose
+morphisms are given by (left) homotopy classes of edges. The construction of this category
+is different from `HomotopyCategory A` in `AlgebraicTopology.SimplicialSet.HomotopyCat`:
+* `HomotopyCategory₂ A` has morphisms given by homotopy classes of edges
+* `HomotopyCategory A` has morphisms given by equivalence classes of paths in the underlying
+  reflexive quiver of `A`.
+
+The two constructions agree for 2-truncated quasicategories (TODO: handled by future PR).
+
 ## Implementation notes
 
 Throughout this file, we make use of `Edge` and `CompStruct` to conveniently deal with
@@ -63,15 +72,15 @@ class Quasicategory₂ (X : Truncated 2) where
 
 /--
 Two edges `f` and `g` are left homotopic if there is a `CompStruct` with
-(0, 1)-edge `f`, (1, 2)-edge `id` and (0, 2)-edge `g`. We use `Nonempty` to
+(0, 1)-edge `f`, (1, 2)-edge `Edge.id` and (0, 2)-edge `g`. We use `Nonempty` to
 have a `Prop` valued `HomotopicL`.
 -/
 abbrev HomotopicL {X : Truncated 2} {x y : X _⦋0⦌₂} (f g : Edge x y) :=
   Nonempty (CompStruct f (id y) g)
 
 /--
 Two edges `f` and `g` are right homotopic if there is a `CompStruct` with
-(0, 1)-edge `id`, (1, 2)-edge `f`, and (0, 2)-edge `g`. We use `Nonempty` to
+(0, 1)-edge `Edge.id`, (1, 2)-edge `f`, and (0, 2)-edge `g`. We use `Nonempty` to
 have a `Prop` valued `HomotopicR`.
 -/
 abbrev HomotopicR {X : Truncated 2} {x y : X _⦋0⦌₂} (f g : Edge x y) :=
@@ -81,20 +90,20 @@ section homotopy_eqrel
 variable {X : Truncated 2}
 
 /--
-Left homotopy relation is reflexive
+The left homotopy relation is reflexive.
 -/
 lemma HomotopicL.refl {x y : X _⦋0⦌₂} {f : Edge x y} : HomotopicL f f := ⟨compId f⟩
 
 /--
-Left homotopy relation is symmetric
+The left homotopy relation is symmetric.
 -/
 lemma HomotopicL.symm [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g : Edge x y} (hfg : HomotopicL f g) :
     HomotopicL g f := by
   rcases hfg with ⟨hfg⟩
   exact Quasicategory₂.fill31 hfg (idComp (id y)) (compId f)
 
 /--
-Left homotopy relation is transitive
+The left homotopy relation is transitive.
 -/
 lemma HomotopicL.trans [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g h : Edge x y} (hfg : HomotopicL f g)
     (hgh : HomotopicL g h) : HomotopicL f h := by
@@ -103,20 +112,20 @@ lemma HomotopicL.trans [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g h : Edge
   exact Quasicategory₂.fill32 hfg (idComp (id y)) hgh
 
 /--
-Right homotopy relation is reflexive
+The right homotopy relation is reflexive.
 -/
 lemma HomotopicR.refl {x y : X _⦋0⦌₂} {f : Edge x y} : HomotopicR f f := ⟨idComp f⟩
 
 /--
-Right homotopy relation is symmetric
+The right homotopy relation is symmetric.
 -/
 lemma HomotopicR.symm [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g : Edge x y} (hfg : HomotopicR f g) :
     HomotopicR g f := by
   rcases hfg with ⟨hfg⟩
   exact Quasicategory₂.fill32 (idComp (id x)) hfg (idComp f)
 
 /--
-Right homotopy relation is transitive
+The right homotopy relation is transitive.
 -/
 lemma HomotopicR.trans [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g h : Edge x y} (hfg : HomotopicR f g)
     (hgh : HomotopicR g h) : HomotopicR f h := by
@@ -125,28 +134,180 @@ lemma HomotopicR.trans [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g h : Edge
   exact Quasicategory₂.fill31 (idComp (id x)) hfg hgh
 
 /--
-In a 2-truncated quasicategory, left homotopy implies right homotopy
+In a 2-truncated quasicategory, left homotopy implies right homotopy.
 -/
 lemma HomotopicL.homotopicR [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g : Edge x y}
     (h : HomotopicL f g) : HomotopicR f g := by
   rcases h with ⟨h⟩
   exact Quasicategory₂.fill32 (idComp f) (compId f) h
 
 /--
-In a 2-truncated quasicategory, right homotopy implies left homotopy
+In a 2-truncated quasicategory, right homotopy implies left homotopy.
 -/
 lemma HomotopicR.homotopicL [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g : Edge x y}
     (h : HomotopicR f g) : HomotopicL f g := by
   rcases h with ⟨h⟩
   exact Quasicategory₂.fill31 (idComp f) (compId f) h
 
 /--
-In a 2-truncated quasicategory, the right and left homotopy relations coincide
+In a 2-truncated quasicategory, the right and left homotopy relations coincide.
 -/
 theorem homotopicL_iff_homotopicR [Quasicategory₂ X] {x y : X _⦋0⦌₂} {f g : Edge x y} :
     HomotopicL f g ↔ HomotopicR f g :=
   ⟨HomotopicL.homotopicR, HomotopicR.homotopicL⟩
 
 end homotopy_eqrel
 
+section homotopy_category
+
+variable {A : Truncated 2} [Quasicategory₂ A] {x y z : A _⦋0⦌₂}
+
+/--
+Given `CompStruct f g h` and `CompStruct f' g' h'` with the same vertices and edges such
+that `f` ≃ `f'` and `g` ≃ `g'`, then the long diagonal edges `h` and `h'` are also homotopic.
+-/
+lemma Edge.CompStruct.comp_unique {f f' : Edge x y} {g g' : Edge y z} {h h' : Edge x z}
+    (s : CompStruct f g h) (s' : CompStruct f' g' h')
+    (hf : HomotopicL f f') (hg : HomotopicL g g') : HomotopicL h h' := by
+  rcases hg.homotopicR with ⟨hg⟩
+  rcases hf with ⟨hf⟩
+  let ⟨s₁⟩ := Quasicategory₂.fill32 hf (idComp g') s'
+  let ⟨s₂⟩ := Quasicategory₂.fill31 (compId f) hg s₁
+  exact Quasicategory₂.fill31 s (compId g) s₂
+
+/--
+Given two consecutive edges `f`, `g`  in a 2-truncated quasicategory, nonconstructively choose
+an edge that is the diagonal of a 2-simplex with spine given by `f` and `g`. The `CompStruct`
+witnessing this property is given by `Edge.composeStruct`.
+-/
+noncomputable def Edge.comp (f : Edge x y) (g : Edge y z) : Edge x z :=
+  (Quasicategory₂.fill21 f g).some.1
+
+/--
+See `Edge.comp`
+-/
+noncomputable def Edge.compStruct (f : Edge x y) (g : Edge y z) : CompStruct f g (f.comp g) :=
+  (Quasicategory₂.fill21 f g).some.2
+
+/--
+The homotopy category of a 2-truncated quasicategory `A` has as objects the vertices of `A`
+-/
+structure HomotopyCategory₂ (A : Truncated 2) where
+  /-- An object of the homotopy category is a vertex of `A`. -/
+  pt : A _⦋0⦌₂
+
+/--
+Left homotopy is an equivalence relation on the edges of `A`.
+Remark: We could have equivalently chosen right homotopy, as shown by `homotopicL_iff_homotopicR`.
+-/
+instance instSetoidEdge (x y : A _⦋0⦌₂) : Setoid (Edge x y) where
+  r := HomotopicL
+  iseqv := ⟨fun _ ↦ HomotopicL.refl, HomotopicL.symm, HomotopicL.trans⟩
+
+namespace HomotopyCategory₂
+
+/--
+The morphisms between two vertices `x`, `y` in `HomotopyCategory₂ A` are homotopy classes
+of edges between `x` and `y`.
+-/
+def Hom (x y : HomotopyCategory₂ A) := Quotient (instSetoidEdge x.pt y.pt)
+
+/--
+Composition of morphisms in `HomotopyCategory₂ A` is given by lifting the edge
+chosen by `composeEdges`.
+-/
+noncomputable
+instance : CategoryStruct (HomotopyCategory₂ A) where
+  Hom x y := Hom x y
+  id x := Quotient.mk' (Edge.id x.pt)
+  comp := Quotient.lift₂ (fun f g ↦ ⟦comp f g⟧)
+    (fun _ _ _ _ hf hg ↦ Quotient.sound
+      (Edge.CompStruct.comp_unique (compStruct _ _) (compStruct _ _) hf hg))
+
+omit [A.Quasicategory₂] in
+/--
+The function `HomotopyCategory₂.mk` taking a vertex of `A` and sending it to the corresponding
+object of `HomotopyCategory₂ A` is surjective.
+-/
+lemma mk_surjective : Function.Surjective (mk : A _⦋0⦌₂ → _) :=
+  fun ⟨x⟩ ↦ ⟨x, rfl⟩
+
+/--
+Any edge in the 2-truncated simplicial set `A` defines a morphism in the homotopy category
+by taking its equivalence class.
+-/
+def homMk (f : Edge x y) : mk x ⟶ mk y := ⟦f⟧
+
+/--
+Every morphism in the homotopy category `HomotopyCategory₂ A` is the equivalence class of
+an edge of `A`.
+-/
+lemma homMk_surjective : Function.Surjective (homMk : Edge x y → _) := Quotient.mk_surjective
+
+/--
+The trivial (degenerate) edge at a vertex `x` is a representative for the
+identity morphism `x ⟶ x`.
+-/
+@[simp]
+lemma homMk_id (x : HomotopyCategory₂ A) : homMk (Edge.id x.pt) = 𝟙 x := rfl
+
+end HomotopyCategory₂
+
+open HomotopyCategory₂
+
+/--
+Left homotopic edges represent the same morphism in the homotopy category.
+-/
+lemma HomotopicL.congr_homotopyCategory₂HomMk {f g : Edge x y} (h : HomotopicL f g) :
+    homMk f = homMk g := Quotient.sound h
+
+/--
+Right homotopic edges represent the same morphism in the homotopy category.
+-/
+lemma HomotopicR.congr_homotopyCategory₂HomMk {f g : Edge x y} (h : HomotopicR f g) :
+    homMk f = homMk g := Quotient.sound h.homotopicL
+
+/--
+A `CompStruct f g h` is a witness for the fact that the morphisms represented by
+`f` and `g` compose to the morphism represented by `h`.
+-/
+lemma Edge.CompStruct.homotopyCategory₂_fac {f : Edge x y} {g : Edge y z} {h : Edge x z}
+    (s : CompStruct f g h) : homMk f ≫ homMk g = homMk h :=
+  (comp_unique (compStruct _ _) s .refl .refl).congr_homotopyCategory₂HomMk
+
+/--
+If we have a factorization `homMk f ≫ homMk g = homMk h`, this is the choice
+of a structure `CompStruct f g h`.
+-/
+noncomputable def Edge.CompStruct.ofHomotopyCategory₂Fac
+    {f : Edge x y} {g : Edge y z} {h : Edge x z}
+    (fac : homMk f ≫ homMk g = homMk h) : CompStruct f g h := by
+  dsimp [homMk, CategoryStruct.comp] at fac
+  rw [Quotient.eq_iff_equiv] at fac
+  exact (Quasicategory₂.fill32 (compStruct f g) (compId g) fac.some).some
+
+/--
+Given edges `f`, `g` and `h` of a `2`-truncated quasicategory,
+there exists a structure `CompStruct f g h` iff
+`homMk f ≫ homMk g = homMk h` holds in the homotopy category.
+-/
+lemma Edge.CompStruct.nonempty_iff {f : Edge x y} {g : Edge y z} {h : Edge x z} :
+    Nonempty (CompStruct f g h) ↔ homMk f ≫ homMk g = homMk h :=
+  ⟨fun ⟨h⟩ ↦ h.homotopyCategory₂_fac, fun h ↦ ⟨.ofHomotopyCategory₂Fac h⟩⟩
+
+noncomputable
+instance : Category (HomotopyCategory₂ A) where
+  id_comp := by
+    rintro _ _ ⟨f⟩
+    exact ((compStruct _ f).comp_unique (idComp _) .refl .refl).congr_homotopyCategory₂HomMk
+  comp_id := by
+    rintro _ _ ⟨f⟩
+    exact ((compStruct _ _).comp_unique (compId _) .refl .refl).congr_homotopyCategory₂HomMk
+  assoc := by
+    rintro _ _ _ _ ⟨f⟩ ⟨g⟩ ⟨h⟩
+    exact (Quasicategory₂.fill31 (compStruct f g) (compStruct g h)
+      (compStruct _ _)).some.homotopyCategory₂_fac
+
+end homotopy_category
+
 end SSet.Truncated