feat(algebraic_topology): simplicial objects and simplicial types (#6195)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: 3 people

src/algebraic_topology/simplicial_object.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison
+-/
+import algebraic_topology.simplex_category
+
+/-!
+# Simplicial objects in a category.
+
+A simplicial object in a category `C` is a `C`-valued presheaf on `simplex_category`.
+-/
+
+open opposite
+open category_theory
+
+universes v u
+
+namespace category_theory
+
+variables (C : Type u) [category.{v} C]
+
+/-- The category of simplicial objects valued in a category `C`.
+This is the category of contravariant functors from `simplex_category` to `C`. -/
+@[derive category, nolint has_inhabited_instance]
+def simplicial_object := simplex_categoryᵒᵖ ⥤ C
+
+namespace simplicial_object
+variables {C} (X : simplicial_object C)
+
+/-- Face maps for a simplicial object. -/
+def δ {n} (i : fin (n+2)) : X.obj (op (n+1 : ℕ)) ⟶ X.obj (op n) :=
+X.map (simplex_category.δ i).op
+
+/-- Degeneracy maps for a simplicial object. -/
+def σ {n} (i : fin (n+1)) : X.obj (op n) ⟶ X.obj (op (n+1 : ℕ)) :=
+X.map (simplex_category.σ i).op
+
+
+/-- Isomorphisms from identities in ℕ. -/
+def eq_to_iso {n m : ℕ} (h : n = m) : X.obj (op n) ≅ X.obj (op m) :=
+X.map_iso (eq_to_iso (by rw h))
+
+@[simp] lemma eq_to_iso_refl {n : ℕ} (h : n = n) : X.eq_to_iso h = iso.refl _ :=
+by { ext, simp [eq_to_iso], }
+
+
+/-- The generic case of the first simplicial identity -/
+lemma δ_comp_δ {n} {i j : fin (n+2)} (H : i ≤ j) :
+  X.δ j.succ ≫ X.δ i = X.δ i.cast_succ ≫ X.δ j :=
+by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ H] }
+
+/-- The special case of the first simplicial identity -/
+lemma δ_comp_δ_self {n} {i : fin (n+2)} : X.δ i.cast_succ ≫ X.δ i = X.δ i.succ ≫ X.δ i :=
+by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ_self] }
+
+/-- The second simplicial identity -/
+lemma δ_comp_σ_of_le {n} {i : fin (n+2)} {j : fin (n+1)} (H : i ≤ j.cast_succ) :
+  X.σ j.succ ≫ X.δ i.cast_succ = X.δ i ≫ X.σ j :=
+by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_le H] }
+
+/-- The first part of the third simplicial identity -/
+lemma δ_comp_σ_self {n} {i : fin (n+1)} :
+  X.σ i ≫ X.δ i.cast_succ = 𝟙 _ :=
+begin
+  dsimp [δ, σ],
+  simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_self, op_id, X.map_id],
+end
+
+/-- The second part of the third simplicial identity -/
+lemma δ_comp_σ_succ {n} {i : fin (n+1)} :
+  X.σ i ≫ X.δ i.succ = 𝟙 _ :=
+begin
+  dsimp [δ, σ],
+  simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_succ, op_id, X.map_id],
+end
+
+/-- The fourth simplicial identity -/
+lemma δ_comp_σ_of_gt {n} {i : fin (n+2)} {j : fin (n+1)} (H : j.cast_succ < i) :
+  X.σ j.cast_succ ≫ X.δ i.succ = X.δ i ≫ X.σ j :=
+by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_gt H] }
+
+/-- The fifth simplicial identity -/
+lemma σ_comp_σ {n} {i j : fin (n+1)} (H : i ≤ j) :
+  X.σ j ≫ X.σ i.cast_succ = X.σ i ≫ X.σ j.succ :=
+by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.σ_comp_σ H] }
+
+end simplicial_object
+
+end category_theory

src/algebraic_topology/simplicial_set.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Scott Morrison
+-/
+import algebraic_topology.simplicial_object
+import category_theory.yoneda
+
+/-!
+A simplicial set is just a simplicial object in `Type`,
+i.e. a `Type`-valued presheaf on the simplex category.
+
+(One might be tempted to all these "simplicial types" when working in type-theoretic foundations,
+but this would be unnecessarily confusing given the existing notion of a simplicial type in
+homotopy type theory.)
+
+We define the standard simplices `Δ[n]` as simplicial sets,
+and their boundaries `∂Δ[n]` and horns `Λ[n, i]`.
+(The notations are available via `open_locale sSet`.)
+
+## Future work
+
+There isn't yet a complete API for simplices, boundaries, and horns.
+As an example, we should have a function that constructs
+from a non-surjective order preserving function `fin n → fin n`
+a morphism `Δ[n] ⟶ ∂Δ[n]`.
+-/
+
+universes v u
+
+open category_theory
+
+/-- The category of simplicial sets.
+This is the category of contravariant functors from
+`simplex_category` to `Type u`. -/
+@[derive large_category]
+def sSet : Type (u+1) := simplicial_object (Type u)
+
+namespace sSet
+
+/-- The `n`-th standard simplex `Δ[n]` associated with a nonempty finite linear order `n`
+is the Yoneda embedding of `n`. -/
+def standard_simplex : simplex_category ⥤ sSet := yoneda
+
+localized "notation `Δ[`n`]` := standard_simplex.obj n" in sSet
+
+instance : inhabited sSet := ⟨standard_simplex.obj (0 : ℕ)⟩
+
+/-- The `m`-simplices of the `n`-th standard simplex are
+the monotone maps from `fin (m+1)` to `fin (n+1)`. -/
+def as_preorder_hom {n} {m} (α : Δ[n].obj m) :
+  preorder_hom (fin (m.unop+1)) (fin (n+1)) := α
+
+/-- The boundary `∂Δ[n]` of the `n`-th standard simplex consists of
+all `m`-simplices of `standard_simplex n` that are not surjective
+(when viewed as monotone function `m → n`). -/
+def boundary (n : ℕ) : sSet :=
+{ obj := λ m, {α : Δ[n].obj m // ¬ function.surjective (as_preorder_hom α)},
+  map := λ m₁ m₂ f α, ⟨f.unop ≫ (α : Δ[n].obj m₁),
+  by { intro h, apply α.property, exact function.surjective.of_comp h }⟩ }
+
+localized "notation `∂Δ[`n`]` := boundary n" in sSet
+
+/-- The inclusion of the boundary of the `n`-th standard simplex into that standard simplex. -/
+def boundary_inclusion (n : ℕ) :
+  ∂Δ[n] ⟶ Δ[n] :=
+{ app := λ m (α : {α : Δ[n].obj m // _}), α }
+
+/-- `horn n i` (or `Λ[n, i]`) is the `i`-th horn of the `n`-th standard simplex, where `i : n`.
+It consists of all `m`-simplices `α` of `Δ[n]`
+for which the union of `{i}` and the range of `α` is not all of `n`
+(when viewing `α` as monotone function `m → n`). -/
+def horn (n : ℕ) (i : fin (n+1)) : sSet :=
+{ obj := λ m,
+  { α : Δ[n].obj m // set.range (as_preorder_hom α) ∪ {i} ≠ set.univ },
+  map := λ m₁ m₂ f α, ⟨f.unop ≫ (α : Δ[n].obj m₁),
+  begin
+    intro h, apply α.property,
+    rw set.eq_univ_iff_forall at h ⊢, intro j,
+    apply or.imp _ id (h j),
+    intro hj,
+    exact set.range_comp_subset_range _ _ hj,
+  end⟩ }
+
+localized "notation `Λ[`n`, `i`]` := horn n i" in sSet
+
+/-- The inclusion of the `i`-th horn of the `n`-th standard simplex into that standard simplex. -/
+def horn_inclusion (n : ℕ) (i : fin (n+1)) :
+  Λ[n, i] ⟶ Δ[n] :=
+{ app := λ m (α : {α : Δ[n].obj m // _}), α }
+
+end sSet