feat(AlgebraicTopology): definition of Kan complex and quasicategory (#9357)

Author: jcommelin

Mathlib.lean

@@ -547,8 +547,10 @@ import Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
 import Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
 import Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
 import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
+import Mathlib.AlgebraicTopology.KanComplex
 import Mathlib.AlgebraicTopology.MooreComplex
 import Mathlib.AlgebraicTopology.Nerve
+import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet

Mathlib/AlgebraicTopology/KanComplex.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Mathlib.AlgebraicTopology.SimplicialSet
+
+/-!
+# Kan complexes
+
+In this file we give the definition of Kan complexes.
+In `Mathlib/AlgebraicTopology/Quasicategory.lean`
+we show that every Kan complex is a quasicategory.
+
+## TODO
+
+- Show that the singular simplicial set of a topological space is a Kan complex.
+- Generalize the definition to higher universes.
+  Since `Λ[n, i]` is an object of `SSet.{0}`,
+  the current definition of a Kan complex `S`
+  requires `S : SSet.{0}`.
+
+-/
+
+namespace SSet
+
+open CategoryTheory Simplicial
+
+/-- A simplicial set `S` is a *Kan complex* if it satisfies the following horn-filling condition:
+for every `n : ℕ` and `0 ≤ i ≤ n`,
+every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`. -/
+class KanComplex (S : SSet) : Prop where
+  hornFilling : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄ (σ₀ : Λ[n, i] ⟶ S),
+    ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ
+
+end SSet

Mathlib/AlgebraicTopology/Quasicategory.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Mathlib.AlgebraicTopology.KanComplex
+
+/-!
+# Quasicategories
+
+In this file we define quasicategories,
+a common model of infinity categories.
+We show that every Kan complex is a quasicategory.
+
+In `Mathlib/AlgebraicTopology/Nerve.lean`
+we show (TODO) that the nerve of a category is a quasicategory.
+
+## TODO
+
+- Generalize the definition to higher universes.
+  See the corresponding TODO in `Mathlib/AlgebraicTopology/KanComplex.lean`.
+
+-/
+
+namespace SSet
+
+open CategoryTheory Simplicial
+
+/-- A simplicial set `S` is a *quasicategory* if it satisfies the following horn-filling condition:
+for every `n : ℕ` and `0 < i < n`,
+every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`.
+
+[Kerodon, 003A] -/
+class Quasicategory (S : SSet) : Prop where
+  hornFilling' : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n+3)⦄ (σ₀ : Λ[n+2, i] ⟶ S)
+     (_h0 : 0 < i) (_hn : i < Fin.last (n+2)),
+       ∃ σ : Δ[n+2] ⟶ S, σ₀ = hornInclusion (n+2) i ≫ σ
+
+lemma Quasicategory.hornFilling {S : SSet} [Quasicategory S] ⦃n : ℕ⦄ ⦃i : Fin (n+1)⦄
+    (h0 : 0 < i) (hn : i < Fin.last n)
+    (σ₀ : Λ[n, i] ⟶ S) : ∃ σ : Δ[n] ⟶ S, σ₀ = hornInclusion n i ≫ σ := by
+  cases n using Nat.casesAuxOn with
+  | zero => simp [Fin.lt_iff_val_lt_val] at hn
+  | succ n =>
+  cases n using Nat.casesAuxOn with
+  | zero =>
+    simp only [Fin.lt_iff_val_lt_val, Fin.val_zero, Fin.val_last, zero_add, Nat.lt_one_iff] at h0 hn
+    simp [hn] at h0
+  | succ n => exact Quasicategory.hornFilling' σ₀ h0 hn
+
+/-- Every Kan complex is a quasicategory.
+
+[Kerodon, 003C] -/
+instance (S : SSet) [KanComplex S] : Quasicategory S where
+  hornFilling' _ _ σ₀ _ _ := KanComplex.hornFilling σ₀
+
+end SSet