Normal forms for morphisms in SimplexCategoryGenRel
. #
In this file, we establish that P_δ
and P_σ
morphisms in SimplexCategoryGenRel
each admits a normal form.
In both cases, the normal forms are encoded as an integer m
, and a strictly increasing
lists of integers [i₀,…,iₙ]
such that iₖ ≤ m + k
for all k
. We define a predicate
isAdmissible m : List ℕ → Prop
encoding this property. And provide some lemmas to help
work with such lists.
Normal forms for P_σ
morphisms are encoded by m
-admissible lists, in which case the list
[i₀,…,iₙ]
represents the morphism σ iₙ ≫ ⋯ ≫ σ i₀ : .mk (m + n) ⟶ .mk n
.
Normal forms for P_δ
morphisms are encoded by (m + 1)
-admissible lists, in which case the list
[i₀,…,iₙ]
represents the morphism δ i₀ ≫ ⋯ ≫ δ iₙ : .mk n ⟶ .mk (m + n)
.
The results in this file are to be treated as implementation-only, and they only serve as stepping
stones towards proving that the canonical functor
toSimplexCategory : SimplexCategoryGenRel ⥤ SimplexCategory
is an equivalence.
References: #
TODOs: #
- Show that every
P_σ
admits a unique normal form. - Show that every
P_δ
admits a unique normal form.
A list of natural numbers [i₀, ⋯, iₙ]) is said to be m
-admissible (for m : ℕ
) if
i₀ < ⋯ < iₙ
and iₖ ≤ m + k
for all k
.
Equations
Instances For
If L
is a (m + 1)
-admissible list, and a
is natural number such that a ≤ m and a < L[0],
then a::L
is m
-admissible
The tail of an m
-admissible list is (m+1)-admissible.
The head of an m
-admissible list.
Equations
- SimplexCategoryGenRel.IsAdmissible.head a L hl = hl.getElemAsFin 0 ⋯
Instances For
The construction simplicialInsert
describes inserting an element in a list of integer and
moving it to its "right place" according to the simplicial relations. Somewhat miraculously,
the algorithm is the same for the first or the fifth simplicial relations, making it "valid"
when we treat the list as a normal form for a morphism satisfying P_δ
, or for a morphism
satisfying P_σ
!
This is similar in nature to List.orderedInsert
, but note that we increment one of the element
every time we perform an exchange, making it a different construction.
Equations
Instances For
simplicialInsert
just adds one to the length.
simplicialInsert
preserves admissibility