Realization of strings as representations

[Jar19]'s mapping g: each symbol denotes a representation primitive and a string denotes their iterated tensor. 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: tier content of a realization is compositional.

@[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.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 ι τ

Realize a string as a representation: the iterated tensor of its symbols' primitives ([Jar19]'s g).

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)

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.

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)

tierProj packages tierWord: on a word it is the realized tier word.