Commit 2021-03-08 11:35 b6ed62ca

View on Github →

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

Estimated changes

Created src/algebraic_topology/simplicial_object.lean

added def category_theory.simplicial_object.eq_to_iso

added theorem category_theory.simplicial_object.eq_to_iso_refl

added def category_theory.simplicial_object.δ

added theorem category_theory.simplicial_object.δ_comp_δ

added theorem category_theory.simplicial_object.δ_comp_δ_self

added theorem category_theory.simplicial_object.δ_comp_σ_of_gt

added theorem category_theory.simplicial_object.δ_comp_σ_of_le

added theorem category_theory.simplicial_object.δ_comp_σ_self

added theorem category_theory.simplicial_object.δ_comp_σ_succ

added def category_theory.simplicial_object.σ

added theorem category_theory.simplicial_object.σ_comp_σ

added def category_theory.simplicial_object

Created src/algebraic_topology/simplicial_set.lean

added def sSet.as_preorder_hom

added def sSet.boundary

added def sSet.boundary_inclusion

added def sSet.horn

added def sSet.horn_inclusion

added def sSet.standard_simplex

added def sSet