Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.RankFunction.Cell.dim

{X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → {f : P.RankFunction ι} → {i : ι} → f.Cell i → ℕ

The dimension c.dim of a cell c of a rank function for a pairing P of a subcomplex of a simplicial set. This is defined as the dimension of the corresponding type (II) simplex. (In the case P is proper, the corresponding type (I) simplex will be of dimension c.dim + 1.)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Cited by

40 results in Mathlib

Foundations

Depth 37 from the axioms · uses propext, Quot.sound

Assumes

LinearOrder