The bipartite-to-multi-tier inclusion functor

The strong monoidal functor ι : AR α β ⥤ MultiAR (biTier α β) realising the bipartite autosegmental category as the n = 2 case: a bipartite graph is the 2-tier multigraph associating only the (0,1) melody↔skeleton pair. Unit and tensor coherences are the object equalities toMultiGraph_empty/toMultiGraph_concat as eqToIso. ([Gol76], [JH15])

Main definitions

• Graph.toMultiGraph, AR.toMultiAR — the inclusion on objects.
• ι — the inclusion functor; the ι.Monoidal instance makes it strong monoidal.

@[reducible, inline]

abbrev Autosegmental.biTier (α β : Type u) : Fin 2 → Type u

The two-tier family ![α, β] indexing the bipartite case.

Equations

• Autosegmental.biTier α β = ![α, β]

def Autosegmental.Graph.toMultiGraph {α β : Type u} (G : Graph α β) : MultiGraph (biTier α β)

The inclusion on objects: a bipartite Graph α β as the 2-tier MultiGraph ![α,β] that associates only the (0,1) tier-pair (melody↔skeleton). The dependent Fin 2 tier-tuple is built with Fin.cons (![·,·] is non-dependent and cannot host the heterogeneous LabeledTuple α/LabeledTuple β).

Equations

• G.toMultiGraph = { tiers := Fin.cons G.upper (Fin.cons G.lower finZeroElim), links := fun (i j : Fin 2) => if i = 0 ∧ j = 1 then G.links else ∅ }

@[simp]

theorem Autosegmental.toMultiGraph_tiers_zero {α β : Type u} (G : Graph α β) : G.toMultiGraph.tiers 0 = G.upper

@[simp]

theorem Autosegmental.toMultiGraph_tiers_one {α β : Type u} (G : Graph α β) : G.toMultiGraph.tiers 1 = G.lower

@[simp]

theorem Autosegmental.toMultiGraph_links_01 {α β : Type u} (G : Graph α β) : G.toMultiGraph.links 0 1 = G.links

@[simp]

theorem Autosegmental.toMultiGraph_isPlanar {α β : Type u} (G : Graph α β) : G.toMultiGraph.IsPlanar ↔ G.IsPlanar

The inclusion sends a planar bipartite graph to a planar multigraph (and back): the only nonempty pair is (0,1), carrying G.links.

theorem Autosegmental.toMultiGraph_empty {α β : Type u} : Graph.empty.toMultiGraph = MultiGraph.empty

The inclusion preserves the empty graph (monoidal unit coherence).

theorem Autosegmental.toMultiGraph_concat {α β : Type u} (A B : Graph α β) : (A.concat B).toMultiGraph = A.toMultiGraph.concat B.toMultiGraph

The inclusion preserves concatenation — the monoidal-functor coherence on objects: (A ⋆ B) maps to (toMultiGraph A) ⋆ (toMultiGraph B).

The inclusion functor on objects (in-bounds lift)

theorem Autosegmental.toMultiGraph_inBounds {α β : Type u} {A : AR α β} : A.toMultiGraph.InBounds

The bipartite InBounds lifts to the multigraph: the only nonempty link-pair of toMultiGraph is (0,1), where it carries G.links and the tier lengths are upper/lower.

def Autosegmental.AR.toMultiAR {α β : Type u} (A : AR α β) : MultiAR (biTier α β)

The inclusion on objects.

Equations

• A.toMultiAR = { toMultiGraph := A.toMultiGraph, inBounds := ⋯ }

@[simp]

theorem Autosegmental.AR.toMultiAR_toMultiGraph {α β : Type u} (A : AR α β) : A.toMultiAR.toMultiGraph = A.toMultiGraph

The inclusion on morphisms

def Autosegmental.AR.Hom.toMultiFT {α β : Type u} {A B : AR α β} (f : A.Hom B) (i : Fin 2) : (A.toMultiAR.tiers i).Hom (B.toMultiAR.tiers i)

The Fin 2-tuple of tier maps mirroring how toMultiGraph.tiers is built.

Equations

• f.toMultiFT = Fin.cons f.fU (Fin.cons f.fL finZeroElim)

@[simp]

theorem Autosegmental.AR.Hom.toMultiFT_zero {α β : Type u} {A B : AR α β} (f : A.Hom B) : f.toMultiFT 0 = f.fU

@[simp]

theorem Autosegmental.AR.Hom.toMultiFT_one {α β : Type u} {A B : AR α β} (f : A.Hom B) : f.toMultiFT 1 = f.fL

def Autosegmental.AR.Hom.toMultiAR {α β : Type u} {A B : AR α β} (f : A.Hom B) : A.toMultiAR.Hom B.toMultiAR

The inclusion on morphisms.

Equations

• f.toMultiAR = { fT := f.toMultiFT, links_preserve := ⋯ }

The plain functor

def Autosegmental.ι {α β : Type u} : CategoryTheory.Functor (AR α β) (MultiAR (biTier α β))

The inclusion functor AR α β ⥤ MultiAR (biTier α β).

Equations

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

@[simp]

theorem Autosegmental.ι_obj {α β : Type u} (A : AR α β) : ι.obj A = A.toMultiAR

@[simp]

theorem Autosegmental.ι_map {α β : Type u} {A B : AR α β} (f : A ⟶ B) : ι.map f = AR.Hom.toMultiAR f

Monoidal coherence on objects (lifting to in-bounds MultiAR)

theorem Autosegmental.toMultiAR_empty {α β : Type u} : AR.empty.toMultiAR = MultiAR.empty

The inclusion preserves the tensor unit (monoidal unit object coherence).

@[simp]

theorem Autosegmental.toMultiAR_empty_tiers_len {α β : Type u} (i : Fin 2) : (AR.empty.toMultiAR.tiers i).len = 0

Every tier of the included unit is empty (length 0).

theorem Autosegmental.toMultiAR_concat {α β : Type u} (A B : AR α β) : (A.concat B).toMultiAR = A.toMultiAR.concat B.toMultiAR

The inclusion preserves the tensor (monoidal tensor object coherence).

@[simp]

theorem Autosegmental.toMultiAR_fT {α β : Type u} {A B : AR α β} (f : A.Hom B) : f.toMultiAR.fT = f.toMultiFT

The strong monoidal upgrade

Via Functor.CoreMonoidal — εIso/μIso are the eqToIso of the object coherences — and CoreMonoidal.toMonoidal.

theorem Autosegmental.toMultiAR_concatMap {α β : Type u} {A A' B B' : AR α β} (f : A.Hom A') (g : B.Hom B') : (f.concatMap g).toMultiAR = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f.toMultiAR.concatMap g.toMultiAR) (CategoryTheory.eqToHom ⋯))

The monoidal-functoriality bridge (the μ-naturality crux): ι of a tensor of morphisms is the tensor of the ι-images, conjugated by the object coherence eqToHoms.

def Autosegmental.ι.coreMonoidal {α β : Type u} : ι.CoreMonoidal

The Functor.CoreMonoidal data for the inclusion: εIso/μIso are the eqToIsos of the object coherences.

Equations

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

@[implicit_reducible]

instance Autosegmental.instMonoidalARMultiARBiTierι {α β : Type u} : ι.Monoidal

The strong monoidal functor AR α β ⥤ MultiAR (biTier α β).

Equations

• Autosegmental.instMonoidalARMultiARBiTierι = Autosegmental.ι.coreMonoidal.toMonoidal