Mathlib Map

Theorems · Definition · category theory

SimplexCategoryGenRel.generators

CategoryTheory.MorphismProperty SimplexCategoryGenRel

A morphism is a generator if it is either a face or a degeneracy.

Defined in
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
Cited by
5 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimplexCategoryGenRel.multiplicativeClosure_isGenerator_eq_top · cited by 2SimplexCategoryGenRel.mul…SimplexCategoryGenRel.hom_induction · cited by 1SimplexCategoryGenRel.hom…SimplexCategoryGenRel.generators.δ · cited by 1generators.δSimplexCategoryGenRel.generators.σ · cited by 1generators.σSimplexCategoryGenRel.hom_induction' · cited by 0SimplexCategoryGenRel.hom…CategoryTheory.MorphismProperty · cited by 2179CategoryTheory.MorphismPr…SimplexCategoryGenRel · cited by 39SimplexCategoryGenRelSimplexCategoryGenRel.faces · cited by 5SimplexCategoryGenRel.fac…SimplexCategoryGenRel.degeneracies · cited by 4SimplexCategoryGenRel.deg…SimplexCategoryGenRel.generat…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.