mathlib3 documentation

algebraic_topology.simplicial_set

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 call 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 simplicial.)

Future work #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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].

@[protected, instance]

def sSet.has_limits :

category_theory.limits.has_limits sSet

@[protected, instance]

def sSet.large_category :

category_theory.large_category sSet

@[protected, instance]

def sSet.has_colimits :

category_theory.limits.has_colimits sSet

def sSet :

Type (u+1)

The category of simplicial sets. This is the category of contravariant functors from simplex_category to Type u.

Equations

sSet = category_theory.simplicial_object (Type u)

Instances for sSet

def sSet.standard_simplex :

simplex_category ⥤ sSet

The n-th standard simplex Δ[n] associated with a nonempty finite linear order n is the Yoneda embedding of n.

Equations

sSet.standard_simplex = category_theory.yoneda

@[protected, instance]

def sSet.inhabited :

Equations

sSet.inhabited = {default := sSet.standard_simplex.obj (simplex_category.mk 0)}

def sSet.as_order_hom {n : ℕ} {m : simplex_category ᵒᵖ} (α : (sSet.standard_simplex.obj (simplex_category.mk n)).obj m) :

fin ((opposite.unop m).len + 1) →o fin (n + 1)

The m-simplices of the n-th standard simplex are the monotone maps from fin (m+1) to fin (n+1).

Equations

sSet.as_order_hom α = simplex_category.hom.to_order_hom α

def sSet.boundary (n : ℕ) :

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).

Equations

sSet.boundary n = {obj := λ (m : simplex_category ᵒᵖ), {α // ¬function.surjective ⇑(sSet.as_order_hom α)}, map := λ (m₁ m₂ : simplex_category ᵒᵖ) (f : m₁ ⟶ m₂) (α : {α // ¬function.surjective ⇑(sSet.as_order_hom α)}), ⟨f.unop ≫ ↑α, _⟩, map_id' := _, map_comp' := _}

def sSet.boundary_inclusion (n : ℕ) :

sSet.boundary n ⟶ sSet.standard_simplex.obj (simplex_category.mk n)

The inclusion of the boundary of the n-th standard simplex into that standard simplex.

Equations

sSet.boundary_inclusion n = {app := λ (m : simplex_category ᵒᵖ) (α : {α // ¬function.surjective ⇑(sSet.as_order_hom α)}), ↑α, naturality' := _}

def sSet.horn (n : ℕ) (i : fin (n + 1)) :

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).

Equations

sSet.horn n i = {obj := λ (m : simplex_category ᵒᵖ), {α // set.range ⇑(sSet.as_order_hom α) ∪ {i} ≠ set.univ}, map := λ (m₁ m₂ : simplex_category ᵒᵖ) (f : m₁ ⟶ m₂) (α : {α // set.range ⇑(sSet.as_order_hom α) ∪ {i} ≠ set.univ}), ⟨f.unop ≫ ↑α, _⟩, map_id' := _, map_comp' := _}

def sSet.horn_inclusion (n : ℕ) (i : fin (n + 1)) :

sSet.horn n i ⟶ sSet.standard_simplex.obj (simplex_category.mk n)

The inclusion of the i-th horn of the n-th standard simplex into that standard simplex.

Equations

sSet.horn_inclusion n i = {app := λ (m : simplex_category ᵒᵖ) (α : {α // set.range ⇑(sSet.as_order_hom α) ∪ {i} ≠ set.univ}), ↑α, naturality' := _}

noncomputable def sSet.S1 :

The simplicial circle.

Equations

sSet.S1 = category_theory.limits.colimit (category_theory.limits.parallel_pair (sSet.standard_simplex.map (simplex_category.δ 0)) (sSet.standard_simplex.map (simplex_category.δ 1)))

@[protected, instance]

def sSet.truncated.large_category (n : ℕ) :

category_theory.large_category (sSet.truncated n)

def sSet.truncated (n : ℕ) :

Type (u+1)

Truncated simplicial sets.

Equations

sSet.truncated n = category_theory.simplicial_object.truncated (Type u) n

Instances for sSet.truncated

@[protected, instance]

def sSet.truncated.has_colimits (n : ℕ) :

category_theory.limits.has_colimits (sSet.truncated n)

@[protected, instance]

def sSet.truncated.has_limits (n : ℕ) :

category_theory.limits.has_limits (sSet.truncated n)

def sSet.sk (n : ℕ) :

sSet ⥤ sSet.truncated n

The skeleton functor on simplicial sets.

Equations

sSet.sk n = category_theory.simplicial_object.sk n

@[protected, instance]

def sSet.truncated.inhabited {n : ℕ} :

inhabited (sSet.truncated n)

Equations

sSet.truncated.inhabited = {default := (sSet.sk n).obj (sSet.standard_simplex.obj (simplex_category.mk 0))}

@[reducible]

def sSet.augmented :

Type (u+1)

The category of augmented simplicial sets, as a particular case of augmented simplicial objects.

@[simp]

theorem sSet.augmented.standard_simplex_obj_left (Δ : simplex_category) :

(sSet.augmented.standard_simplex.obj Δ).left = sSet.standard_simplex.obj Δ

@[simp]

theorem sSet.augmented.standard_simplex_obj_right (Δ : simplex_category) :

(sSet.augmented.standard_simplex.obj Δ).right = ⊤_ Type

@[simp]

theorem sSet.augmented.standard_simplex_map_right (Δ₁ Δ₂ : simplex_category) (θ : Δ₁ ⟶ Δ₂) (ᾰ : {left := sSet.standard_simplex.obj Δ₁, right := ⊤_ Type, hom := {app := λ (Δ' : simplex_category ᵒᵖ), category_theory.limits.terminal.from (((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ₁)).obj Δ'), naturality' := _}}.right) :

(sSet.augmented.standard_simplex.map θ).right ᾰ = category_theory.limits.terminal.from {left := sSet.standard_simplex.obj Δ₁, right := ⊤_ Type, hom := {app := λ (Δ' : simplex_category ᵒᵖ), category_theory.limits.terminal.from (((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ₁)).obj Δ'), naturality' := _}}.right ᾰ

@[simp]

theorem sSet.augmented.standard_simplex_map_left (Δ₁ Δ₂ : simplex_category) (θ : Δ₁ ⟶ Δ₂) :

(sSet.augmented.standard_simplex.map θ).left = sSet.standard_simplex.map θ

noncomputable def sSet.augmented.standard_simplex :

simplex_category ⥤ sSet.augmented

The functor which sends [n] to the simplicial set Δ[n] equipped by the obvious augmentation towards the terminal object of the category of sets.

Equations

sSet.augmented.standard_simplex = {obj := λ (Δ : simplex_category), {left := sSet.standard_simplex.obj Δ, right := ⊤_ Type, hom := {app := λ (Δ' : simplex_category ᵒᵖ), category_theory.limits.terminal.from (((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ)).obj Δ'), naturality' := _}}, map := λ (Δ₁ Δ₂ : simplex_category) (θ : Δ₁ ⟶ Δ₂), {left := sSet.standard_simplex.map θ, right := category_theory.limits.terminal.from {left := sSet.standard_simplex.obj Δ₁, right := ⊤_ Type, hom := {app := λ (Δ' : simplex_category ᵒᵖ), category_theory.limits.terminal.from (((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ₁)).obj Δ'), naturality' := _}}.right, w' := _}, map_id' := sSet.augmented.standard_simplex._proof_10, map_comp' := sSet.augmented.standard_simplex._proof_11}

@[simp]

theorem sSet.augmented.standard_simplex_obj_hom_app (Δ : simplex_category) (Δ' : simplex_category ᵒᵖ) (ᾰ : ((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ)).obj Δ') :

(sSet.augmented.standard_simplex.obj Δ).hom.app Δ' ᾰ = category_theory.limits.terminal.from (((𝟭 (category_theory.simplicial_object Type)).obj (sSet.standard_simplex.obj Δ)).obj Δ') ᾰ

def Top.to_sSet :

The functor associating the singular simplicial set to a topological space.

Equations

Top.to_sSet = category_theory.colimit_adj.restricted_yoneda simplex_category.to_Top

noncomputable def sSet.to_Top :

The geometric realization functor.

Equations

sSet.to_Top = category_theory.colimit_adj.extend_along_yoneda simplex_category.to_Top

noncomputable def sSet_Top_adj :

sSet.to_Top ⊣ Top.to_sSet

Geometric realization is left adjoint to the singular simplicial set construction.

Equations

sSet_Top_adj = category_theory.colimit_adj.yoneda_adjunction simplex_category.to_Top

noncomputable def sSet.to_Top_simplex :

category_theory.yoneda ⋙ sSet.to_Top ≅ simplex_category.to_Top

The geometric realization of the representable simplicial sets agree with the usual topological simplices.

Equations

sSet.to_Top_simplex = category_theory.colimit_adj.is_extension_along_yoneda simplex_category.to_Top