The monoidal category of labeled finite tuples

[UPSTREAM] candidate for Mathlib/CategoryTheory/Monoidal/. A LabeledTuple α is a finite tuple of αs: a length n and a labeling Fin n → α. Morphisms are label-preserving position maps (f : Fin a.len → Fin b.len with b.label ∘ f = a.label); this is a skeleton of Over α (finite α-labeled sets) on Fin-objects.

Concatenation (Fin.append on labels, + on lengths) is the categorical coproduct and empty the initial object, so the category is cocartesian: its MonoidalCategory and SymmetricCategory are obtained for free from monoidalOfHasFiniteCoproducts/symmetricOfHasFiniteCoproducts (unlike AugmentedSimplexCategory, whose monotone maps make its ordinal sum not a coproduct, forcing a bespoke monoidal structure). The tensor is concat up to the chosen-coproduct isomorphism.

The concrete Fin-skeletal concat/Hom.concatMap defs (with their Fin.appendMap action) are kept alongside: downstream clients that need the literal Fin (a.len + b.len) carrier — e.g. autosegmental tiers with typed links — consume those directly rather than the opaque coproduct tensor.

Main definitions

• LabeledTuple α — a length-indexed labeled tuple; the object.
• LabeledTuple.Hom a b — a label-preserving position map.
• LabeledTuple.concat — concatenation; LabeledTuple.empty the unit.
• LabeledTuple.Hom.concatMap — the concatenation bifunctor on morphisms.
• MonoidalCategory/SymmetricCategory (LabeledTuple α) — the cocartesian structure: concat as ⊗ (up to coproduct iso), empty as 𝟙_.

structure LabeledTuple (α : Type u) : Type u

A finite tuple of αs: a length and a labeling.

• len : ℕ

  The length of the tuple.

• label : Fin self.len → α

  The labeling of the positions.

@[implicit_reducible]

instance LabeledTuple.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (LabeledTuple α)

Tuples are comparable when labels are: compare lengths, then the labelings (decidable as Fin len is a Fintype). Reduces under decide.

Equations

• One or more equations did not get rendered due to their size.

structure LabeledTuple.Hom {α : Type u} (a b : LabeledTuple α) : Type

A label-preserving position map.

• toFun : Fin a.len → Fin b.len

  The underlying position map.

• label_comp : b.label ∘ self.toFun = a.label

  The map preserves labels.

theorem LabeledTuple.Hom.ext_iff {α : Type u} {a b : LabeledTuple α} {x y : a.Hom b} : x = y ↔ x.toFun = y.toFun

theorem LabeledTuple.Hom.ext {α : Type u} {a b : LabeledTuple α} {x y : a.Hom b} (toFun : x.toFun = y.toFun) : x = y

def LabeledTuple.Hom.id {α : Type u} (a : LabeledTuple α) : a.Hom a

The identity morphism.

Equations

• LabeledTuple.Hom.id a = { toFun := id, label_comp := ⋯ }

def LabeledTuple.Hom.comp {α : Type u} {a b c : LabeledTuple α} (f : a.Hom b) (g : b.Hom c) : a.Hom c

Composition of morphisms (diagrammatic: f then g).

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, label_comp := ⋯ }

@[simp]

theorem LabeledTuple.Hom.id_toFun {α : Type u} (a : LabeledTuple α) : (id a).toFun = _root_.id

@[simp]

theorem LabeledTuple.Hom.comp_toFun {α : Type u} {a b c : LabeledTuple α} (f : a.Hom b) (g : b.Hom c) : (f.comp g).toFun = g.toFun ∘ f.toFun

@[implicit_reducible]

instance LabeledTuple.Hom.instFunLikeFinLen {α : Type u} {a b : LabeledTuple α} : FunLike (a.Hom b) (Fin a.len) (Fin b.len)

A Hom is a label-preserving position map; bundle it as FunLike so f i applies it and the mathlib hom machinery (DFunLike.ext, …) is available.

Equations

• LabeledTuple.Hom.instFunLikeFinLen = { coe := LabeledTuple.Hom.toFun, coe_injective := ⋯ }

@[simp]

theorem LabeledTuple.Hom.coe_toFun {α : Type u} {a b : LabeledTuple α} (f : a.Hom b) : ⇑f = f.toFun

@[implicit_reducible]

instance LabeledTuple.instCategory {α : Type u} : CategoryTheory.Category.{0, u} (LabeledTuple α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LabeledTuple.id_toFun' {α : Type u} (a : LabeledTuple α) : (CategoryTheory.CategoryStruct.id a).toFun = id

@[simp]

theorem LabeledTuple.comp_toFun' {α : Type u} {a b c : LabeledTuple α} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun ∘ f.toFun

@[simp]

theorem LabeledTuple.eqToHom_toFun {α : Type u} {a b : LabeledTuple α} (h : a = b) : (CategoryTheory.eqToHom h).toFun = ⇑(finCongr ⋯)

The index map of an eqToHom is the length-cast finCongr.

Concatenation

def LabeledTuple.concat {α : Type u} (a b : LabeledTuple α) : LabeledTuple α

Concatenation of labeled tuples: lengths add, labels Fin.append.

Equations

• a.concat b = { len := a.len + b.len, label := Fin.append a.label b.label }

def LabeledTuple.empty {α : Type u} : LabeledTuple α

The empty tuple — the monoidal unit.

Equations

• LabeledTuple.empty = { len := 0, label := Fin.elim0 }

@[simp]

theorem LabeledTuple.empty_len {α : Type u} : empty.len = 0

def LabeledTuple.ofList {α : Type u} (l : List α) : LabeledTuple α

The labeled tuple of a list: its length, positionally labeled. The ergonomic bridge for clients that build tiers from List literals.

Equations

• LabeledTuple.ofList l = { len := l.length, label := l.get }

@[simp]

theorem LabeledTuple.ofList_len {α : Type u} (l : List α) : (ofList l).len = l.length

@[simp]

theorem LabeledTuple.ofList_label {α : Type u} (l : List α) : (ofList l).label = l.get

def LabeledTuple.toList {α : Type u} (a : LabeledTuple α) : List α

The underlying list of labels, in position order.

Equations

• a.toList = List.ofFn a.label

@[simp]

theorem LabeledTuple.toList_length {α : Type u} (a : LabeledTuple α) : a.toList.length = a.len

@[simp]

theorem LabeledTuple.toList_ofList {α : Type u} (l : List α) : (ofList l).toList = l

def LabeledTuple.get? {α : Type u} (a : LabeledTuple α) (i : ℕ) : Option α

Raw ℕ-indexed access, out-of-range to none: the positional view for clients that index tiers by ℕ (subgraph embedding, surface bookkeeping).

Equations

• a.get? i = if h : i < a.len then some (a.label ⟨i, h⟩) else none

@[simp]

theorem LabeledTuple.ofList_get? {α : Type u} (l : List α) (i : ℕ) : (ofList l).get? i = l[i]?

@[simp]

theorem LabeledTuple.get?_eq_getElem? {α : Type u} (a : LabeledTuple α) (i : ℕ) : a.get? i = a.toList[i]?

@[simp]

theorem LabeledTuple.concat_len {α : Type u} (a b : LabeledTuple α) : (a.concat b).len = a.len + b.len

@[simp]

theorem LabeledTuple.concat_label {α : Type u} (a b : LabeledTuple α) : (a.concat b).label = Fin.append a.label b.label

@[simp]

theorem LabeledTuple.toList_concat {α : Type u} (a b : LabeledTuple α) : (a.concat b).toList = a.toList ++ b.toList

theorem LabeledTuple.get?_concat_left {α : Type u} {a b : LabeledTuple α} {i : ℕ} (h : i < a.len) : (a.concat b).get? i = a.get? i

Raw access into a concatenation: left block through a, right through b.

theorem LabeledTuple.get?_concat_right {α : Type u} (a b : LabeledTuple α) (j : ℕ) : (a.concat b).get? (a.len + j) = b.get? j

def LabeledTuple.Hom.concatMap {α : Type u} {a a' b b' : LabeledTuple α} (f : a.Hom a') (g : b.Hom b') : (a.concat b).Hom (a'.concat b')

The concatenation bifunctor on morphisms: Fin.appendMap of the position maps. Label preservation is exactly Fin-append naturality.

Equations

• f.concatMap g = { toFun := Fin.appendMap f.toFun g.toFun, label_comp := ⋯ }

@[simp]

theorem LabeledTuple.Hom.concatMap_toFun {α : Type u} {a a' b b' : LabeledTuple α} (f : a.Hom a') (g : b.Hom b') : (f.concatMap g).toFun = Fin.appendMap f.toFun g.toFun

theorem LabeledTuple.Hom.concatMap_id {α : Type u} (a b : LabeledTuple α) : (id a).concatMap (id b) = id (a.concat b)

theorem LabeledTuple.Hom.concatMap_comp {α : Type u} {a a' a'' b b' b'' : LabeledTuple α} (f : a.Hom a') (f' : a'.Hom a'') (g : b.Hom b') (g' : b'.Hom b'') : (f.comp f').concatMap (g.comp g') = (f.concatMap g).comp (f'.concatMap g')

Monoid structure on objects

theorem LabeledTuple.ext {α : Type u} {a b : LabeledTuple α} (hlen : a.len = b.len) (hlabel : a.label = b.label ∘ Fin.cast hlen) : a = b

Extensionality via a length equality and a cast-compatible labeling. The auto-generated structure ext would demand an unusable HEq on label (which depends on len), and the cast dependency here defeats the @[ext] generator, so this is a plain extensionality lemma.

@[simp]

theorem LabeledTuple.ofList_toList {α : Type u} (a : LabeledTuple α) : ofList a.toList = a

theorem LabeledTuple.toList_injective {α : Type u} : Function.Injective toList

theorem LabeledTuple.concat_assoc {α : Type u} (a b c : LabeledTuple α) : (a.concat b).concat c = a.concat (b.concat c)

theorem LabeledTuple.empty_concat {α : Type u} (a : LabeledTuple α) : empty.concat a = a

theorem LabeledTuple.concat_empty {α : Type u} (a : LabeledTuple α) : a.concat empty = a

@[implicit_reducible]

instance LabeledTuple.instMonoid {α : Type u} : Monoid (LabeledTuple α)

Objects form a Monoid under concatenation, with empty as unit.

Equations

• LabeledTuple.instMonoid = { mul := LabeledTuple.concat, mul_assoc := ⋯, one := LabeledTuple.empty, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem LabeledTuple.mul_eq_concat {α : Type u} (a b : LabeledTuple α) : a * b = a.concat b

@[simp]

theorem LabeledTuple.one_eq_empty {α : Type u} : 1 = empty

Cocartesian monoidal structure

empty is the initial object and concat the categorical coproduct (with coprojections Fin.castAdd/Fin.natAdd), so the category is cocartesian and its MonoidalCategory/SymmetricCategory come for free.

instance LabeledTuple.instSubsingletonHomEmpty {α : Type u} (Y : LabeledTuple α) : Subsingleton (empty ⟶ Y)

instance LabeledTuple.instNonemptyHomEmpty {α : Type u} (Y : LabeledTuple α) : Nonempty (empty ⟶ Y)

instance LabeledTuple.instHasInitial {α : Type u} : CategoryTheory.Limits.HasInitial (LabeledTuple α)

def LabeledTuple.inl {α : Type u} (a b : LabeledTuple α) : a.Hom (a.concat b)

The left coprojection a ⟶ a.concat b.

Equations

• a.inl b = { toFun := Fin.castAdd b.len, label_comp := ⋯ }

def LabeledTuple.inr {α : Type u} (a b : LabeledTuple α) : b.Hom (a.concat b)

The right coprojection b ⟶ a.concat b.

Equations

• a.inr b = { toFun := Fin.natAdd a.len, label_comp := ⋯ }

@[simp]

theorem LabeledTuple.inl_toFun {α : Type u} (a b : LabeledTuple α) : (a.inl b).toFun = Fin.castAdd b.len

@[simp]

theorem LabeledTuple.inr_toFun {α : Type u} (a b : LabeledTuple α) : (a.inr b).toFun = Fin.natAdd a.len

def LabeledTuple.coprodDesc {α : Type u} {a b T : LabeledTuple α} (f : a.Hom T) (g : b.Hom T) : (a.concat b).Hom T

The copairing of f : a ⟶ T and g : b ⟶ T, glued by Fin.append.

Equations

• LabeledTuple.coprodDesc f g = { toFun := Fin.append f.toFun g.toFun, label_comp := ⋯ }

@[simp]

theorem LabeledTuple.coprodDesc_toFun {α : Type u} {a b T : LabeledTuple α} (f : a.Hom T) (g : b.Hom T) : (coprodDesc f g).toFun = Fin.append f.toFun g.toFun

instance LabeledTuple.instHasBinaryCoproduct {α : Type u} (a b : LabeledTuple α) : CategoryTheory.Limits.HasBinaryCoproduct a b

concat is the categorical coproduct, with inl/inr the coprojections.

instance LabeledTuple.instHasBinaryCoproducts {α : Type u} : CategoryTheory.Limits.HasBinaryCoproducts (LabeledTuple α)

@[implicit_reducible]

noncomputable instance LabeledTuple.instMonoidalCategory {α : Type u} : CategoryTheory.MonoidalCategory (LabeledTuple α)

Equations

• LabeledTuple.instMonoidalCategory = CategoryTheory.monoidalOfHasFiniteCoproducts (LabeledTuple α)

@[implicit_reducible]

noncomputable instance LabeledTuple.instSymmetricCategory {α : Type u} : CategoryTheory.SymmetricCategory (LabeledTuple α)

Equations

• LabeledTuple.instSymmetricCategory = CategoryTheory.symmetricOfHasFiniteCoproducts (LabeledTuple α)