Documentation

Linglib.Phonology.Autosegmental.MultiAR

The multi-tier autosegmental category `MultiAR τ` #

MultiAR τ is the category of in-bounds multi-tier autosegmental graphs: the general-arity counterpart of the bipartite AR α β (AR.lean). An object is a MultiGraph τ whose links are in bounds; a morphism is a family of per-tier label-preserving position maps (fT i : LabeledTuple.Hom (A.tiers i) (B.tiers i)) that preserves association lines.

The monoidal product is morpheme concatenation (MultiGraph.concat, [JH15]), built via MonoidalCategory.ofTensorHom exactly as AR's is — the dependent tiers add only a funext i to each coherence proof. The planar full monoidal subcategory (Goldsmith's NCC, [Gol76]) would follow WellFormedAR.lean's IsPlanar.FullSubcategory pattern.

The bipartite AR α β includes into MultiAR ![α,β] by a monoidal functor (the object coherence is Inclusion.lean's toMultiGraph_concat/toMultiGraph_empty).

structure Autosegmental.MultiAR {n : ℕ} (τ : Fin n → Type u) extends Autosegmental.MultiGraph τ :

An in-bounds multi-tier autosegmental graph — the base object.

tiers (i : Fin n) : LabeledTuple (τ i)
links (i j : Fin n) : Finset (ℕ × ℕ)
inBounds : self.InBounds

Instances For

Morphisms #

structure Autosegmental.MultiAR.Hom {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

A label- and link-preserving morphism: a family of LabeledTuple.Homs, one per tier, plus link preservation routing each link's endpoints through the maps for its two tiers.

fT (i : Fin n) : (A.tiers i).Hom (B.tiers i)
Per-tier vertex maps.
links_preserve (i j : Fin n) {p q : ℕ} (hp : p < (A.tiers i).len) (hq : q < (A.tiers j).len) : (p, q) ∈ A.links i j → (↑((self.fT i).toFun ⟨p, hp⟩), ↑((self.fT j).toFun ⟨q, hq⟩)) ∈ B.links i j
Association lines are preserved (per tier-pair).

Instances For

theorem Autosegmental.MultiAR.Hom.ext_iff {n : ℕ} {τ : Fin n → Type u} {A B : MultiAR τ} {x y : A.Hom B} :

x = y ↔ x.fT = y.fT

theorem Autosegmental.MultiAR.Hom.ext {n : ℕ} {τ : Fin n → Type u} {A B : MultiAR τ} {x y : A.Hom B} (fT : x.fT = y.fT) :

x = y

def Autosegmental.MultiAR.Hom.id {n : ℕ} {τ : Fin n → Type u} (A : MultiAR τ) :

A.Hom A

The identity morphism.

Equations

Autosegmental.MultiAR.Hom.id A = { fT := fun (i : Fin n) => LabeledTuple.Hom.id (A.tiers i), links_preserve := ⋯ }

Instances For

def Autosegmental.MultiAR.Hom.comp {n : ℕ} {τ : Fin n → Type u} {A B C : MultiAR τ} (f : A.Hom B) (g : B.Hom C) :

A.Hom C

Composition (per tier).

Equations

f.comp g = { fT := fun (i : Fin n) => (f.fT i).comp (g.fT i), links_preserve := ⋯ }

Instances For

@[simp]

theorem Autosegmental.MultiAR.Hom.id_fT {n : ℕ} {τ : Fin n → Type u} (A : MultiAR τ) (i : Fin n) :

(id A).fT i = LabeledTuple.Hom.id (A.tiers i)

@[simp]

theorem Autosegmental.MultiAR.Hom.comp_fT {n : ℕ} {τ : Fin n → Type u} {A B C : MultiAR τ} (f : A.Hom B) (g : B.Hom C) (i : Fin n) :

(f.comp g).fT i = (f.fT i).comp (g.fT i)

@[implicit_reducible]

instance Autosegmental.MultiAR.instCategoryStruct {n : ℕ} {τ : Fin n → Type u} :

CategoryTheory.CategoryStruct.{0, u} (MultiAR τ)

Equations

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

@[implicit_reducible]

instance Autosegmental.MultiAR.instCategory {n : ℕ} {τ : Fin n → Type u} :

CategoryTheory.Category.{0, u} (MultiAR τ)

Equations

Autosegmental.MultiAR.instCategory = { toCategoryStruct := Autosegmental.MultiAR.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[simp]

theorem Autosegmental.MultiAR.id_fT' {n : ℕ} {τ : Fin n → Type u} (A : MultiAR τ) (i : Fin n) :

(CategoryTheory.CategoryStruct.id A).fT i = CategoryTheory.CategoryStruct.id (A.tiers i)

@[simp]

theorem Autosegmental.MultiAR.comp_fT' {n : ℕ} {τ : Fin n → Type u} {A B C : MultiAR τ} (f : A ⟶ B) (g : B ⟶ C) (i : Fin n) :

(CategoryTheory.CategoryStruct.comp f g).fT i = (f.fT i).comp (g.fT i)

Concatenation: the tensor object #

def Autosegmental.MultiAR.concat {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

The monoidal product: tier-wise concatenation, preserving in-bounds.

Equations

A.concat B = { toMultiGraph := A.concat B.toMultiGraph, inBounds := ⋯ }

Instances For

@[simp]

theorem Autosegmental.MultiAR.concat_toMultiGraph {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

(A.concat B).toMultiGraph = A.concat B.toMultiGraph

@[simp]

theorem Autosegmental.MultiAR.concat_tiers {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) (i : Fin n) :

(A.concat B).tiers i = (A.tiers i).concat (B.tiers i)

@[simp]

theorem Autosegmental.MultiAR.concat_links {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) (i j : Fin n) :

(A.concat B).links i j = A.links i j ∪ Finset.image (shiftLink (A.tiers i).len (A.tiers j).len) (B.links i j)

def Autosegmental.MultiAR.empty {n : ℕ} {τ : Fin n → Type u} :

The tensor unit.

Equations

Autosegmental.MultiAR.empty = { toMultiGraph := Autosegmental.MultiGraph.empty, inBounds := ⋯ }

Instances For

theorem Autosegmental.MultiAR.ext_toMultiGraph {n : ℕ} {τ : Fin n → Type u} {A B : MultiAR τ} (h : A.toMultiGraph = B.toMultiGraph) :

A = B

An in-bounds graph is determined by its underlying MultiGraph.

@[implicit_reducible]

instance Autosegmental.MultiAR.instMonoid {n : ℕ} {τ : Fin n → Type u} :

Monoid (MultiAR τ)

Equations

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

@[simp]

theorem Autosegmental.MultiAR.mul_eq_concat {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

A * B = A.concat B

@[simp]

theorem Autosegmental.MultiAR.one_eq_empty {n : ℕ} {τ : Fin n → Type u} :

`tensorHom`: the concatenation bifunctor on morphisms #

def Autosegmental.MultiAR.Hom.concatMap {n : ℕ} {τ : Fin n → Type u} {A A' B B' : MultiAR τ} (f : A.Hom A') (g : B.Hom B') :

(A.concat B).Hom (A'.concat B')

tensorHom: per-tier LabeledTuple.Hom.concatMap. A link on (i,j) routes its first endpoint through tier i's map, its second through tier j's map.

Equations

f.concatMap g = { fT := fun (i : Fin n) => (f.fT i).concatMap (g.fT i), links_preserve := ⋯ }

Instances For

@[simp]

theorem Autosegmental.MultiAR.Hom.concatMap_fT {n : ℕ} {τ : Fin n → Type u} {A A' B B' : MultiAR τ} (f : A.Hom A') (g : B.Hom B') (i : Fin n) :

(f.concatMap g).fT i = (f.fT i).concatMap (g.fT i)

theorem Autosegmental.MultiAR.Hom.concatMap_id {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

(id A).concatMap (id B) = id (A.concat B)

theorem Autosegmental.MultiAR.Hom.concatMap_comp {n : ℕ} {τ : Fin n → Type u} {A A' A'' B B' B'' : MultiAR τ} (f : A.Hom A') (f' : A'.Hom A'') (g : B.Hom B') (g' : B'.Hom B'') :

(f.concatMap g).comp (f'.concatMap g') = (f.comp f').concatMap (g.comp g')

`eqToHom` algebra #

@[simp]

theorem Autosegmental.MultiAR.eqToHom_fT_toFun {n : ℕ} {τ : Fin n → Type u} {A B : MultiAR τ} (h : A = B) (i : Fin n) :

((CategoryTheory.eqToHom h).fT i).toFun = Fin.cast ⋯

The i-th tier map of an eqToHom, as a function: a length-cast Fin.cast.

@[simp]

theorem Autosegmental.MultiAR.concatMap_id_eqToHom {n : ℕ} {τ : Fin n → Type u} {W X Y : MultiAR τ} (h : X = Y) :

Hom.concatMap (CategoryTheory.CategoryStruct.id W) (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯

@[simp]

theorem Autosegmental.MultiAR.concatMap_eqToHom_id {n : ℕ} {τ : Fin n → Type u} {W X Y : MultiAR τ} (h : X = Y) :

Hom.concatMap (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.eqToHom ⋯

Monoidal category #

@[implicit_reducible]

instance Autosegmental.MultiAR.instMonoidalStruct {n : ℕ} {τ : Fin n → Type u} :

CategoryTheory.MonoidalCategoryStruct (MultiAR τ)

Equations

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

@[simp]

theorem Autosegmental.MultiAR.associator_def {n : ℕ} {τ : Fin n → Type u} (A B C : MultiAR τ) :

CategoryTheory.MonoidalCategoryStruct.associator A B C = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.MultiAR.whiskerLeft_def {n : ℕ} {τ : Fin n → Type u} (X x✝ x✝¹ : MultiAR τ) (f : x✝ ⟶ x✝¹) :

CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = (Hom.id X).concatMap f

@[simp]

theorem Autosegmental.MultiAR.whiskerRight_def {n : ℕ} {τ : Fin n → Type u} {X₁✝ X₂✝ : MultiAR τ} (f : X₁✝ ⟶ X₂✝) (Y : MultiAR τ) :

CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = Hom.concatMap f (Hom.id Y)

@[simp]

theorem Autosegmental.MultiAR.leftUnitor_def {n : ℕ} {τ : Fin n → Type u} (X : MultiAR τ) :

CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.MultiAR.rightUnitor_def {n : ℕ} {τ : Fin n → Type u} (X : MultiAR τ) :

CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.MultiAR.tensorObj_def {n : ℕ} {τ : Fin n → Type u} (A B : MultiAR τ) :

CategoryTheory.MonoidalCategoryStruct.tensorObj A B = A.concat B

@[simp]

theorem Autosegmental.MultiAR.tensorUnit_def {n : ℕ} {τ : Fin n → Type u} :

CategoryTheory.MonoidalCategoryStruct.tensorUnit (MultiAR τ) = empty

@[simp]

theorem Autosegmental.MultiAR.tensorHom_def {n : ℕ} {τ : Fin n → Type u} {X₁✝ Y₁✝ X₂✝ Y₂✝ : MultiAR τ} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :

CategoryTheory.MonoidalCategoryStruct.tensorHom f g = Hom.concatMap f g

@[implicit_reducible]

instance Autosegmental.MultiAR.instMonoidalCategory {n : ℕ} {τ : Fin n → Type u} :

CategoryTheory.MonoidalCategory (MultiAR τ)

Equations

Autosegmental.MultiAR.instMonoidalCategory = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯