Documentation

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

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: #

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
    theorem SimplexCategoryGenRel.IsAdmissible.sorted {m : } {L : List } (hL : IsAdmissible m L) :
    List.Sorted (fun (x1 x2 : ) => x1 < x2) L
    theorem SimplexCategoryGenRel.IsAdmissible.le {m : } {L : List } (hL : IsAdmissible m L) (k : ) (h : k < L.length) :
    L[k] m + k
    theorem SimplexCategoryGenRel.IsAdmissible.head_lt {m : } (a : ) (L : List ) (hl : IsAdmissible m (a :: L)) (a' : ) :
    a' La < a'

    If (a :: l) is m-admissible then a is less than all elements of l

    theorem SimplexCategoryGenRel.IsAdmissible.cons {m : } (L : List ) (hL : IsAdmissible (m + 1) L) (a : ) (ha : a m) (ha' : ∀ (x : 0 < L.length), a < L[0]) :

    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

    theorem SimplexCategoryGenRel.IsAdmissible.tail {m : } (a : ) (l : List ) (h : IsAdmissible m (a :: l)) :
    IsAdmissible (m + 1) l

    The tail of an m-admissible list is (m+1)-admissible.

    def SimplexCategoryGenRel.IsAdmissible.getElemAsFin {m : } {L : List } (hl : IsAdmissible m L) (k : ) (hK : k < L.length) :
    Fin (m + k + 1)

    An element of a m-admissible list, as an element of the appropriate Fin

    Equations
    Instances For
      @[simp]
      theorem SimplexCategoryGenRel.IsAdmissible.getElemAsFin_val {m : } {L : List } (hl : IsAdmissible m L) (k : ) (hK : k < L.length) :
      (hl.getElemAsFin k hK) = L[k]
      def SimplexCategoryGenRel.IsAdmissible.head {m : } (a : ) (L : List ) (hl : IsAdmissible m (a :: L)) :
      Fin (m + 1)

      The head of an m-admissible list.

      Equations
      Instances For
        @[simp]
        theorem SimplexCategoryGenRel.IsAdmissible.head_val {m : } (a : ) (L : List ) (hl : IsAdmissible m (a :: L)) :
        (head a L hl) = a

        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
          theorem SimplexCategoryGenRel.simplicialInsert_isAdmissible (m : ) (L : List ) (hL : IsAdmissible (m + 1) L) (j : ) (hj : j < m + 1) :

          simplicialInsert preserves admissibility