Realization of strings as representations

Each symbol denotes a representation primitive, and a string denotes the iterated tensor of its symbols' primitives. This is Jardine's mapping g without the melody merge, which AR.mergeRealize adds. The monoid-homomorphism content lives on the skeleton of the precedence-preserving wide subcategory PrecAR, where concatenation is strictly associative; broad categorical isomorphism forgets the arcs and is too coarse to preserve tier words.

Main definitions

• PrecAR, AR.cls: representations with the classical precedence-preserving morphisms, and the monoid of their isomorphism classes.
• AR.realize, AR.tierProj: the realization as iterated tensor, and its per-tier projections as free-monoid homomorphisms.

Main results

• AR.cls_normalize: normal forms represent their class.
• AR.tierWord_realize, AR.link_realize: tier content and links of a realization are compositional — each link lives inside one symbol's primitive at that symbol's tier offsets (AR.tierOffset).
• AR.noCrossing_realize: realization preserves the NCC of its primitives.

References

• [Jar19]
• [Jar16b]

@[reducible, inline]

abbrev Autosegmental.PrecAR (ι : Type u_3) (τ : ι → Type u_4) : Type (max (max u_3 u_4) (u_5 + 1))

Representations with the classical precedence-preserving morphisms.

Equations

• Autosegmental.PrecAR ι τ = CategoryTheory.WideSubcategory Autosegmental.AR.precPreserving

The monoid of representations up to isomorphism

noncomputable def Autosegmental.AR.fullIsoToWideIso {ι : Type u_1} {τ : ι → Type u_2} {A B : TieredAR ι τ} (e : A.obj.Iso B.obj) : { obj := A } ≅ { obj := B }

A full isomorphism is an isomorphism of the precedence-preserving category; both directions preserve arcs.

Equations

• Autosegmental.AR.fullIsoToWideIso e = CategoryTheory.WideSubcategory.isoMk (Autosegmental.AR.mkIso e) ⋯ ⋯

noncomputable def Autosegmental.AR.cls {ι : Type u_1} {τ : ι → Type u_2} (A : TieredAR ι τ) : CategoryTheory.Skeleton (PrecAR ι τ)

The class of a representation, its isomorphism class in the skeleton of the precedence-preserving category.

Equations

• Autosegmental.AR.cls A = CategoryTheory.toSkeleton { obj := A }

theorem Autosegmental.AR.cls_tensor {ι : Type u_1} {τ : ι → Type u_2} (A B : TieredAR ι τ) : cls (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) = cls A * cls B

Concatenation of classes is the class of the tensor.

theorem Autosegmental.AR.cls_normalize {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] : cls (normalize X) = cls X

Normal forms represent their class.

Realization of strings

noncomputable def Autosegmental.AR.realize {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) (w : List S) : TieredAR ι τ

The realization of a string is the iterated tensor of its symbols' primitives, unmerged.

Equations

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

@[simp]

theorem Autosegmental.AR.realize_nil {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) : realize g₀ [] = CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR ι τ)

@[simp]

theorem Autosegmental.AR.realize_cons {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) (a : S) (w : List S) : realize g₀ (a :: w) = CategoryTheory.MonoidalCategoryStruct.tensorObj (g₀ a) (realize g₀ w)

theorem Autosegmental.AR.noCrossing_realize {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) (hg : ∀ (s : S), NoCrossing (g₀ s).obj.edges (g₀ s).obj.arcs) (w : List S) : NoCrossing (realize g₀ w).obj.edges (realize g₀ w).obj.arcs

A string of primitives obeying the NCC realizes a representation obeying it ([Jar16b] Theorem 4).

Tier content of realizations

instance Autosegmental.AR.realize.instFinite {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) : Finite (realize g₀ w).obj.V

theorem Autosegmental.AR.tierWord_realize {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (w : List S) : tierWord i = (List.map (fun (s : S) => tierWord i) w).flatten

The tier word of a realized string is the concatenation of its symbols' tier words.

@[simp]

theorem Autosegmental.AR.tierLength_realize {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (w : List S) : tierLength (realize g₀ w) i = (List.map (fun (s : S) => tierLength (g₀ s) i) w).sum

Links of realizations

noncomputable def Autosegmental.AR.tierOffset {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (w : List S) (k : ℕ) : ℕ

The tier-i offset of the k-th symbol of w is the tier-i content of the prefix before it.

Equations

• Autosegmental.AR.tierOffset g₀ i w k = Autosegmental.AR.tierLength (Autosegmental.AR.realize g₀ (List.take k w)) i

@[simp]

theorem Autosegmental.AR.tierOffset_zero {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (w : List S) : tierOffset g₀ i w 0 = 0

@[simp]

theorem Autosegmental.AR.tierOffset_cons_succ {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (a : S) (w : List S) (k : ℕ) : tierOffset g₀ i (a :: w) (k + 1) = tierLength (g₀ a) i + tierOffset g₀ i w k

theorem Autosegmental.AR.link_realize {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i j : ι) (w : List S) (p q : ℕ) : link (realize g₀ w) i j p q ↔ ∃ (k : ℕ) (hk : k < w.length), tierOffset g₀ i w k ≤ p ∧ tierOffset g₀ j w k ≤ q ∧ link (g₀ w[k]) i j (p - tierOffset g₀ i w k) (q - tierOffset g₀ j w k)

A link of a realization lives inside one symbol's primitive, at that symbol's tier offsets.

theorem Autosegmental.AR.link_realize_of_tierLength_eq_one {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] {j : ι} (hj : ∀ (s : S), tierLength (g₀ s) j = 1) (i : ι) (w : List S) (p q : ℕ) : link (realize g₀ w) i j p q ↔ ∃ (hq : q < w.length), tierOffset g₀ i w q ≤ p ∧ link (g₀ w[q]) i j (p - tierOffset g₀ i w q) 0

With one tier-j position per symbol, tier-j positions of the realization are the string's positions: a link at position q is a link inside the q-th symbol's primitive.

noncomputable def Autosegmental.AR.tierProj {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) : FreeMonoid S →* FreeMonoid (τ i)

The tier-i projection of a realization, as a free-monoid homomorphism: each symbol contributes its primitive's tier word.

Equations

• Autosegmental.AR.tierProj g₀ i = FreeMonoid.lift fun (s : S) => FreeMonoid.ofList (Autosegmental.AR.tierWord i)

@[simp]

theorem Autosegmental.AR.tierProj_of {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (a : S) : (tierProj g₀ i) (FreeMonoid.of a) = FreeMonoid.ofList (tierWord i)

theorem Autosegmental.AR.tierProj_ofList {ι : Type u_1} {τ : ι → Type u_2} {S : Type u_3} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (i : ι) (w : List S) : (tierProj g₀ i) (FreeMonoid.ofList w) = FreeMonoid.ofList (tierWord i)

On a word, tierProj is the realized tier word.