The simplex category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We construct a skeletal model of the simplex category, with objects ℕ and the
morphism n ⟶ m being the monotone maps from fin (n+1) to fin (m+1).
We show that this category is equivalent to NonemptyFinLinOrd.
Remarks #
The definitions simplex_category and simplex_category.hom are marked as irreducible.
We provide the following functions to work with these objects:
simplex_category.mkcreates an object ofsimplex_categoryout of a natural number. Use the notation[n]in thesimpliciallocale.simplex_category.lengives the "length" of an object ofsimplex_category, as a natural.simplex_category.hom.mkmakes a morphism out of a monotone map betweenfin's.simplex_category.hom.to_order_homgives the underlying monotone map associated to a term ofsimplex_category.hom.
Interpet a natural number as an object of the simplex category.
Equations
- simplex_category.mk n = n
The length of an object of simplex_category.
@[simp]
@[protected]
def
simplex_category.rec
{F : simplex_category → Sort u_1}
(h : Π (n : ℕ), F (simplex_category.mk n))
(X : simplex_category) :
F X
A recursor for simplex_category. Use it as induction Δ using simplex_category.rec.
Equations
- simplex_category.rec h = λ (n : simplex_category), h n.len
def
simplex_category.hom.mk
{a b : simplex_category}
(f : fin (a.len + 1) →o fin (b.len + 1)) :
a.hom b
Make a moprhism in simplex_category from a monotone map of fin's.
Equations
Recover the monotone map from a morphism in the simplex category.
Equations
- f.to_order_hom = f
@[ext]
theorem
simplex_category.hom.ext
{a b : simplex_category}
(f g : a.hom b) :
f.to_order_hom = g.to_order_hom → f = g
@[simp]
@[simp]
theorem
simplex_category.hom.to_order_hom_mk
{a b : simplex_category}
(f : fin (a.len + 1) →o fin (b.len + 1)) :
theorem
simplex_category.hom.mk_to_order_hom_apply
{a b : simplex_category}
(f : fin (a.len + 1) →o fin (b.len + 1))
(i : fin (a.len + 1)) :
⇑((simplex_category.hom.mk f).to_order_hom) i = ⇑f i
@[simp]
Composition of morphisms of simplex_category.
Equations
- f.comp g = simplex_category.hom.mk (f.to_order_hom.comp g.to_order_hom)
@[protected, instance]
Equations
- simplex_category.small_category = {to_category_struct := {to_quiver := {hom := λ (n m : simplex_category), n.hom m}, id := λ (m : simplex_category), simplex_category.hom.id m, comp := λ (_x _x_1 _x_2 : simplex_category) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), simplex_category.hom.comp g f}, id_comp' := simplex_category.small_category._proof_1, comp_id' := simplex_category.small_category._proof_2, assoc' := simplex_category.small_category._proof_3}
@[simp]
theorem
simplex_category.small_category_comp
(_x _x_1 _x_2 : simplex_category)
(f : _x ⟶ _x_1)
(g : _x_1 ⟶ _x_2) :
f ≫ g = simplex_category.hom.comp g f
@[simp]
The constant morphism from [0].
Equations
- x.const i = simplex_category.hom.mk {to_fun := λ (_x : fin ((simplex_category.mk 0).len + 1)), i, monotone' := _}
@[simp]
theorem
simplex_category.hom_zero_zero
(f : simplex_category.mk 0 ⟶ simplex_category.mk 0) :
f = 𝟙 (simplex_category.mk 0)
Generating maps for the simplex category #
TODO: prove that the simplex category is equivalent to one given by the following generators and relations.
def
simplex_category.δ
{n : ℕ}
(i : fin (n + 2)) :
simplex_category.mk n ⟶ simplex_category.mk (n + 1)
The i-th face map from [n] to [n+1]
Equations
Instances for simplex_category.δ
def
simplex_category.σ
{n : ℕ}
(i : fin (n + 1)) :
simplex_category.mk (n + 1) ⟶ simplex_category.mk n
The i-th degeneracy map from [n+1] to [n]
Equations
- simplex_category.σ i = simplex_category.mk_hom {to_fun := i.pred_above, monotone' := _}
Instances for simplex_category.σ
The generic case of the first simplicial identity
theorem
simplex_category.δ_comp_δ'
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : ⇑fin.cast_succ i < j) :
theorem
simplex_category.δ_comp_δ''
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : i ≤ ⇑fin.cast_succ j) :
The special case of the first simplicial identity
theorem
simplex_category.δ_comp_δ_self_assoc
{n : ℕ}
{i : fin (n + 2)}
{X' : simplex_category}
(f' : simplex_category.mk (n + 1 + 1) ⟶ X') :
simplex_category.δ i ≫ simplex_category.δ (⇑fin.cast_succ i) ≫ f' = simplex_category.δ i ≫ simplex_category.δ i.succ ≫ f'
theorem
simplex_category.δ_comp_δ_self'
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : j = ⇑fin.cast_succ i) :
theorem
simplex_category.δ_comp_δ_self'_assoc
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 3)}
(H : j = ⇑fin.cast_succ i)
{X' : simplex_category}
(f' : simplex_category.mk (n + 1 + 1) ⟶ X') :
simplex_category.δ i ≫ simplex_category.δ j ≫ f' = simplex_category.δ i ≫ simplex_category.δ i.succ ≫ f'
theorem
simplex_category.δ_comp_σ_of_le
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j) :
The second simplicial identity
theorem
simplex_category.δ_comp_σ_of_le_assoc
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : i ≤ ⇑fin.cast_succ j)
{X' : simplex_category}
(f' : simplex_category.mk (n + 1) ⟶ X') :
simplex_category.δ (⇑fin.cast_succ i) ≫ simplex_category.σ j.succ ≫ f' = simplex_category.σ j ≫ simplex_category.δ i ≫ f'
theorem
simplex_category.δ_comp_σ_self_assoc
{n : ℕ}
{i : fin (n + 1)}
{X' : simplex_category}
(f' : simplex_category.mk n ⟶ X') :
simplex_category.δ (⇑fin.cast_succ i) ≫ simplex_category.σ i ≫ f' = f'
The first part of the third simplicial identity
theorem
simplex_category.δ_comp_σ_self'
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i) :
theorem
simplex_category.δ_comp_σ_self'_assoc
{n : ℕ}
{j : fin (n + 2)}
{i : fin (n + 1)}
(H : j = ⇑fin.cast_succ i)
{X' : simplex_category}
(f' : simplex_category.mk n ⟶ X') :
simplex_category.δ j ≫ simplex_category.σ i ≫ f' = f'
theorem
simplex_category.δ_comp_σ_succ_assoc
{n : ℕ}
{i : fin (n + 1)}
{X' : simplex_category}
(f' : simplex_category.mk n ⟶ X') :
simplex_category.δ i.succ ≫ simplex_category.σ i ≫ f' = f'
The second part of the third simplicial identity
theorem
simplex_category.δ_comp_σ_succ'_assoc
{n : ℕ}
(j : fin (n + 2))
(i : fin (n + 1))
(H : j = i.succ)
{X' : simplex_category}
(f' : simplex_category.mk n ⟶ X') :
simplex_category.δ j ≫ simplex_category.σ i ≫ f' = f'
theorem
simplex_category.δ_comp_σ_of_gt_assoc
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i)
{X' : simplex_category}
(f' : simplex_category.mk (n + 1) ⟶ X') :
simplex_category.δ i.succ ≫ simplex_category.σ (⇑fin.cast_succ j) ≫ f' = simplex_category.σ j ≫ simplex_category.δ i ≫ f'
theorem
simplex_category.δ_comp_σ_of_gt
{n : ℕ}
{i : fin (n + 2)}
{j : fin (n + 1)}
(H : ⇑fin.cast_succ j < i) :
The fourth simplicial identity
theorem
simplex_category.δ_comp_σ_of_gt'
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : j.succ < i) :
simplex_category.δ i ≫ simplex_category.σ j = simplex_category.σ (j.cast_lt _) ≫ simplex_category.δ (i.pred _)
theorem
simplex_category.δ_comp_σ_of_gt'_assoc
{n : ℕ}
{i : fin (n + 3)}
{j : fin (n + 2)}
(H : j.succ < i)
{X' : simplex_category}
(f' : simplex_category.mk (n + 1) ⟶ X') :
simplex_category.δ i ≫ simplex_category.σ j ≫ f' = simplex_category.σ (j.cast_lt _) ≫ simplex_category.δ (i.pred _) ≫ f'
The fifth simplicial identity
theorem
simplex_category.σ_comp_σ_assoc
{n : ℕ}
{i j : fin (n + 1)}
(H : i ≤ j)
{X' : simplex_category}
(f' : simplex_category.mk n ⟶ X') :
simplex_category.σ (⇑fin.cast_succ i) ≫ simplex_category.σ j ≫ f' = simplex_category.σ j.succ ≫ simplex_category.σ i ≫ f'
@[simp]
The functor that exhibits simplex_category as skeleton
of NonemptyFinLinOrd
Equations
- simplex_category.skeletal_functor = {obj := λ (a : simplex_category), NonemptyFinLinOrd.of (ulift (fin (a.len + 1))), map := λ (a b : simplex_category) (f : a ⟶ b), {to_fun := λ (i : ↥(NonemptyFinLinOrd.of (ulift (fin (a.len + 1))))), {down := ⇑(simplex_category.hom.to_order_hom f) i.down}, monotone' := _}, map_id' := simplex_category.skeletal_functor._proof_2, map_comp' := simplex_category.skeletal_functor._proof_3}
@[simp]
theorem
simplex_category.skeletal_functor_obj
(a : simplex_category) :
simplex_category.skeletal_functor.obj a = NonemptyFinLinOrd.of (ulift (fin (a.len + 1)))
theorem
simplex_category.skeletal_functor.coe_map
{Δ₁ Δ₂ : simplex_category}
(f : Δ₁ ⟶ Δ₂) :
⇑(simplex_category.skeletal_functor.map f) = ulift.up ∘ ⇑(simplex_category.hom.to_order_hom f) ∘ ulift.down
@[protected, instance]
Equations
- simplex_category.skeletal_functor.category_theory.full = {preimage := λ (a b : simplex_category) (f : simplex_category.skeletal_functor.obj a ⟶ simplex_category.skeletal_functor.obj b), simplex_category.hom.mk {to_fun := λ (i : fin (a.len + 1)), (⇑f {down := i}).down, monotone' := _}, witness' := simplex_category.skeletal_functor.category_theory.full._proof_2}
@[protected, instance]
@[protected, instance]
@[protected, instance]
The equivalence that exhibits simplex_category as skeleton
of NonemptyFinLinOrd
simplex_category is a skeleton of NonemptyFinLinOrd.
@[protected, instance]
The truncated simplex category.
Equations
- simplex_category.truncated n = category_theory.full_subcategory (λ (a : simplex_category), a.len ≤ n)
Instances for simplex_category.truncated
@[protected, instance]
Equations
- simplex_category.truncated.inhabited = {default := {obj := simplex_category.mk 0, property := _}}
@[protected, instance]
@[protected, instance]
The fully faithful inclusion of the truncated simplex category into the usual simplex category.
Equations
Instances for simplex_category.truncated.inclusion
@[protected, instance]
Equations
- simplex_category.category_theory.concrete_category = category_theory.concrete_category.mk {obj := λ (i : simplex_category), fin (i.len + 1), map := λ (i j : simplex_category) (f : i ⟶ j), ⇑(simplex_category.hom.to_order_hom f), map_id' := simplex_category.category_theory.concrete_category._proof_1, map_comp' := simplex_category.category_theory.concrete_category._proof_2}
A morphism in simplex_category is a monomorphism precisely when it is an injective function
A morphism in simplex_category is an epimorphism if and only if it is a surjective function
theorem
simplex_category.len_le_of_mono
{x y : simplex_category}
{f : x ⟶ y} :
category_theory.mono f → x.len ≤ y.len
A monomorphism in simplex_category must increase lengths
theorem
simplex_category.le_of_mono
{n m : ℕ}
{f : simplex_category.mk n ⟶ simplex_category.mk m} :
category_theory.mono f → n ≤ m
theorem
simplex_category.len_le_of_epi
{x y : simplex_category}
{f : x ⟶ y} :
category_theory.epi f → y.len ≤ x.len
An epimorphism in simplex_category must decrease lengths
theorem
simplex_category.le_of_epi
{n m : ℕ}
{f : simplex_category.mk n ⟶ simplex_category.mk m} :
category_theory.epi f → m ≤ n
@[protected, instance]
@[protected, instance]
theorem
simplex_category.is_iso_of_bijective
{x y : simplex_category}
{f : x ⟶ y}
(hf : function.bijective (simplex_category.hom.to_order_hom f).to_fun) :
@[simp]
An isomorphism in simplex_category induces an order_iso.
Equations
- simplex_category.order_iso_of_iso e = {to_fun := ⇑(simplex_category.hom.to_order_hom e.hom), inv_fun := ⇑(simplex_category.hom.to_order_hom e.inv), left_inv := _, right_inv := _}.to_order_iso _ _
theorem
simplex_category.eq_id_of_is_iso
{x : simplex_category}
(f : x ⟶ x)
[hf : category_theory.is_iso f] :
theorem
simplex_category.eq_σ_comp_of_not_injective'
{n : ℕ}
{Δ' : simplex_category}
(θ : simplex_category.mk (n + 1) ⟶ Δ')
(i : fin (n + 1))
(hi : ⇑(simplex_category.hom.to_order_hom θ) (⇑fin.cast_succ i) = ⇑(simplex_category.hom.to_order_hom θ) i.succ) :
∃ (θ' : simplex_category.mk n ⟶ Δ'), θ = simplex_category.σ i ≫ θ'
theorem
simplex_category.eq_σ_comp_of_not_injective
{n : ℕ}
{Δ' : simplex_category}
(θ : simplex_category.mk (n + 1) ⟶ Δ')
(hθ : ¬function.injective ⇑(simplex_category.hom.to_order_hom θ)) :
∃ (i : fin (n + 1)) (θ' : simplex_category.mk n ⟶ Δ'), θ = simplex_category.σ i ≫ θ'
theorem
simplex_category.eq_comp_δ_of_not_surjective'
{n : ℕ}
{Δ : simplex_category}
(θ : Δ ⟶ simplex_category.mk (n + 1))
(i : fin (n + 2))
(hi : ∀ (x : fin (Δ.len + 1)), ⇑(simplex_category.hom.to_order_hom θ) x ≠ i) :
∃ (θ' : Δ ⟶ simplex_category.mk n), θ = θ' ≫ simplex_category.δ i
theorem
simplex_category.eq_comp_δ_of_not_surjective
{n : ℕ}
{Δ : simplex_category}
(θ : Δ ⟶ simplex_category.mk (n + 1))
(hθ : ¬function.surjective ⇑(simplex_category.hom.to_order_hom θ)) :
∃ (i : fin (n + 2)) (θ' : Δ ⟶ simplex_category.mk n), θ = θ' ≫ simplex_category.δ i
theorem
simplex_category.eq_id_of_mono
{x : simplex_category}
(i : x ⟶ x)
[category_theory.mono i] :
theorem
simplex_category.eq_σ_of_epi
{n : ℕ}
(θ : simplex_category.mk (n + 1) ⟶ simplex_category.mk n)
[category_theory.epi θ] :
theorem
simplex_category.eq_δ_of_mono
{n : ℕ}
(θ : simplex_category.mk n ⟶ simplex_category.mk (n + 1))
[category_theory.mono θ] :
theorem
simplex_category.len_lt_of_mono
{Δ' Δ : simplex_category}
(i : Δ' ⟶ Δ)
[hi : category_theory.mono i]
(hi' : Δ ≠ Δ') :
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem
simplex_category.image_eq
{Δ Δ' Δ'' : simplex_category}
{φ : Δ ⟶ Δ''}
{e : Δ ⟶ Δ'}
[category_theory.epi e]
{i : Δ' ⟶ Δ''}
[category_theory.mono i]
(fac : e ≫ i = φ) :
theorem
simplex_category.image_ι_eq
{Δ Δ'' : simplex_category}
{φ : Δ ⟶ Δ''}
{e : Δ ⟶ category_theory.limits.image φ}
[category_theory.epi e]
{i : category_theory.limits.image φ ⟶ Δ''}
[category_theory.mono i]
(fac : e ≫ i = φ) :
theorem
simplex_category.factor_thru_image_eq
{Δ Δ'' : simplex_category}
{φ : Δ ⟶ Δ''}
{e : Δ ⟶ category_theory.limits.image φ}
[category_theory.epi e]
{i : category_theory.limits.image φ ⟶ Δ''}
[category_theory.mono i]
(fac : e ≫ i = φ) :
@[simp]
@[simp]
This functor simplex_category ⥤ Cat sends [n] (for n : ℕ)
to the category attached to the ordered set {0, 1, ..., n}