Labeled mixed graphs

A labeled mixed graph ⟨V, E, A, ℓ⟩ has labeled vertices, undirected association edges, and directed order arcs — the autosegmental representation of [Jar19], with no further structure. Graph S carries the quadruple as fields: a vertex type, a SimpleGraph of association edges, a Digraph of order arcs, and a labeling ℓ : V → S. Tiers are not part of the object: a tier assignment t : S → ι on the labels induces a vertex coloring X.tier t, and the §4.2 well-formedness axioms (AR.lean) carve the representations out of the raw graphs relative to it.

Main definitions

• Graph S: the labeled mixed graph ([Jar19]'s GR(Γ)) and the category thereof, with HasInitial and HasBinaryCoproducts; Graph.Hom are label- and association-preserving maps, precPreserving marks the full-structure homomorphisms, Graph.Iso the full-structure equivalences.
• Graph.concat t: concatenation — the vertex sum with a same-tier bridge, [JH15] Definition 2 in the order signature, minus its R_ID merge (OCP.collapse); Graph.sum is the bridge-free coproduct.

Main results

• concatEmptyIso, emptyConcatIso, concatAssocIso: [JH15] Theorems 1 and 3 up to Iso, unconditional in the order signature.

Implementation notes

concat bridges every same-tier pair, so its arcs are order-closed representatives: [Jar19]'s operative concatenation bridges one partial (last, first) pair per tier, and the two forms are interconvertible as Hasse diagram ↔ transitive closure on the finite per-tier strict orders. The complete bridge is total and functorial where first/last are partial and not hom-preserved, and its monoid laws are unconditional where the successor form's associativity requires string-graph tier classes ([JH15]'s Lemma 1 remark). The choice is not free elsewhere: subgraph-based notions such as ASL.lean's forbidden factors are signature-sensitive ([Jar17a]).

Morphisms deliberately do not preserve precedence — reassociation analyses move material across the order — so Hom is the broad class where the coproduct and the OCP repair live; precPreserving marks the wide class of full-structure maps.

The category of labeled mixed graphs

structure Autosegmental.Graph (S : Type u_3) : Type (max u_3 (u_4 + 1))

An object of the category of labeled mixed graphs over S, the literature's labeled mixed graph ⟨V, E, A, ℓ⟩ ([Jar19]'s GR(Γ)) carried fieldwise.

• V : Type u_4

  The vertex type.

• edges : SimpleGraph self.V

  The undirected association edges (E).

• arcs : Digraph self.V

  The directed order arcs (A).

• label : self.V → S

  The labeling (ℓ).

def Autosegmental.Graph.tier {S : Type u_1} {ι : Type u_2} (t : S → ι) (X : Graph S) : X.V → ι

The tier of a vertex under a tier assignment on the alphabet.

Equations

• Autosegmental.Graph.tier t X = t ∘ X.label

Morphisms

structure Autosegmental.Graph.Hom {S : Type u_1} (X : Graph S) (Y : Graph S) : Type (max u_3 u_4)

A label- and association-preserving map of labeled mixed graphs.

• toFun : X.V → Y.V

  The vertex map.

• edge_map ⦃v w : X.V⦄ : X.edges.Adj v w → Y.edges.Adj (self.toFun v) (self.toFun w)

  Association edges are preserved.

• label_comp (v : X.V) : Y.label (self.toFun v) = X.label v

  Labels are preserved.

theorem Autosegmental.Graph.Hom.ext {S : Type u_1} {X : Graph S} {Y : Graph S} {x y : X.Hom Y} (toFun : x.toFun = y.toFun) : x = y

theorem Autosegmental.Graph.Hom.ext_iff {S : Type u_1} {X : Graph S} {Y : Graph S} {x y : X.Hom Y} : x = y ↔ x.toFun = y.toFun

def Autosegmental.Graph.Hom.id {S : Type u_1} (X : Graph S) : X.Hom X

The identity morphism.

Equations

• Autosegmental.Graph.Hom.id X = { toFun := id, edge_map := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.Hom.comp {S : Type u_1} {X : Graph S} {Y : Graph S} {Z : Graph S} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms.

Equations

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

Isomorphism

structure Autosegmental.Graph.Iso {S : Type u_1} (X : Graph S) (Y : Graph S) extends X.V ≃ Y.V : Type (max u_3 u_4)

A label- and relation-preserving equivalence of labeled mixed graphs.

• toFun : X.V → Y.V
• invFun : Y.V → X.V
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• edges_iff (v w : X.V) : Y.edges.Adj (self.toEquiv v) (self.toEquiv w) ↔ X.edges.Adj v w

  Association edges correspond.

• arcs_iff (v w : X.V) : Y.arcs.Adj (self.toEquiv v) (self.toEquiv w) ↔ X.arcs.Adj v w

  Order arcs correspond.

• label_comp (v : X.V) : Y.label (self.toEquiv v) = X.label v

  Labels are preserved.

def Autosegmental.Graph.Iso.toHom {S : Type u_1} {X : Graph S} {Y : Graph S} (e : X.Iso Y) : X.Hom Y

An isomorphism as a morphism.

Equations

• e.toHom = { toFun := ⇑e.toEquiv, edge_map := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.Iso.refl {S : Type u_1} (X : Graph S) : X.Iso X

The identity isomorphism.

Equations

• Autosegmental.Graph.Iso.refl X = { toEquiv := Equiv.refl X.V, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.Iso.symm {S : Type u_1} {X : Graph S} {Y : Graph S} (e : X.Iso Y) : Y.Iso X

Inverse isomorphism.

Equations

• e.symm = { toEquiv := e.symm, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.Iso.trans {S : Type u_1} {X : Graph S} {Y : Graph S} {Z : Graph S} (e : X.Iso Y) (f : Y.Iso Z) : X.Iso Z

Composition of isomorphisms.

Equations

• e.trans f = { toEquiv := e.trans f.toEquiv, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

The empty graph

def Autosegmental.Graph.empty (S : Type u_3) : Graph S

The empty labeled mixed graph, on the empty vertex type.

Equations

• Autosegmental.Graph.empty S = { V := PEmpty.{?u.1 + 1}, edges := ⊥, arcs := ⊥, label := PEmpty.elim }

Tier-bridging concatenation

Per tier class, concatenation is the ordinal sum: blockwise arcs plus a bridge from every X-vertex to every same-tier Y-vertex. On the choice of the complete bridge over [Jar19]'s partial (last, first) pair, see the implementation notes above.

def Autosegmental.Graph.concat {S : Type u_1} {ι : Type u_2} (t : S → ι) (X : Graph S) (Y : Graph S) : Graph S

The concatenation of two labeled mixed graphs, the disjoint edge sum with per-tier ordinal-sum arcs ([JH15] Definition 2 minus its R_ID melody merge).

Equations

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

@[simp]

theorem Autosegmental.Graph.concat_label_inl {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) (v : X.V) : (concat t X Y).label (Sum.inl v) = X.label v

@[simp]

theorem Autosegmental.Graph.concat_label_inr {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) (v : Y.V) : (concat t X Y).label (Sum.inr v) = Y.label v

@[simp]

theorem Autosegmental.Graph.concat_edges {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) : (concat t X Y).edges = X.edges ⊕g Y.edges

@[simp]

theorem Autosegmental.Graph.concat_arcs_inl_inl {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) {v w : X.V} : (concat t X Y).arcs.Adj (Sum.inl v) (Sum.inl w) ↔ X.arcs.Adj v w

@[simp]

theorem Autosegmental.Graph.concat_arcs_inr_inr {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) {v w : Y.V} : (concat t X Y).arcs.Adj (Sum.inr v) (Sum.inr w) ↔ Y.arcs.Adj v w

@[simp]

theorem Autosegmental.Graph.concat_arcs_inl_inr {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) {v : X.V} {w : Y.V} : (concat t X Y).arcs.Adj (Sum.inl v) (Sum.inr w) ↔ tier t X v = tier t Y w

@[simp]

theorem Autosegmental.Graph.not_concat_arcs_inr_inl {S : Type u_1} {ι : Type u_2} {X : Graph S} {Y : Graph S} (t : S → ι) {v : Y.V} {w : X.V} : ¬(concat t X Y).arcs.Adj (Sum.inr v) (Sum.inl w)

Unit laws ([JH15] Theorem 1)

def Autosegmental.Graph.concatEmptyIso {S : Type u_1} {ι : Type u_2} (t : S → ι) (X : Graph S) : (concat t X (empty S)).Iso X

Concatenation with the empty graph on the right, up to isomorphism.

Equations

• Autosegmental.Graph.concatEmptyIso t X = { toEquiv := Equiv.sumEmpty X.V PEmpty.{?u.1 + 1}, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.emptyConcatIso {S : Type u_1} {ι : Type u_2} (t : S → ι) (X : Graph S) : (concat t (empty S) X).Iso X

Concatenation with the empty graph on the left, up to isomorphism.

Equations

• Autosegmental.Graph.emptyConcatIso t X = { toEquiv := Equiv.emptySum PEmpty.{?u.1 + 1} X.V, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

Functoriality of concatenation

def Autosegmental.Graph.Hom.concatMap {S : Type u_1} {ι : Type u_2} {X₁ : Graph S} {Y₁ : Graph S} {X₂ : Graph S} {Y₂ : Graph S} (t : S → ι) (f : X₁.Hom Y₁) (g : X₂.Hom Y₂) : (concat t X₁ X₂).Hom (concat t Y₁ Y₂)

The concatenation of morphisms, Sum.map on vertices.

Equations

• Autosegmental.Graph.Hom.concatMap t f g = { toFun := Sum.map f.toFun g.toFun, edge_map := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.Iso.concatCongr {S : Type u_1} {ι : Type u_2} {X₁ : Graph S} {Y₁ : Graph S} {X₂ : Graph S} {Y₂ : Graph S} (t : S → ι) (e₁ : X₁.Iso Y₁) (e₂ : X₂.Iso Y₂) : (concat t X₁ X₂).Iso (concat t Y₁ Y₂)

The concatenation of isomorphisms.

Equations

• Autosegmental.Graph.Iso.concatCongr t e₁ e₂ = { toEquiv := e₁.sumCongr e₂.toEquiv, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

Associativity up to isomorphism ([JH15] Theorem 3)

def Autosegmental.Graph.concatAssocIso {S : Type u_1} {ι : Type u_2} (t : S → ι) (X : Graph S) (Y : Graph S) (Z : Graph S) : (concat t (concat t X Y) Z).Iso (concat t X (concat t Y Z))

Concatenation is associative up to isomorphism.

Equations

• Autosegmental.Graph.concatAssocIso t X Y Z = { toEquiv := Equiv.sumAssoc X.V Y.V Z.V, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

The bridge-free sum

The plain blockwise sum carries no bridging arcs and is the categorical coproduct of the broad category; not_isTierOrdered_sum (AR.lean) shows why concat bridges instead.

def Autosegmental.Graph.sum {S : Type u_1} (X : Graph S) (Y : Graph S) : Graph S

The bridge-free blockwise sum.

Equations

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

@[simp]

theorem Autosegmental.Graph.sum_edges {S : Type u_1} {X : Graph S} {Y : Graph S} : (X.sum Y).edges = X.edges ⊕g Y.edges

@[simp]

theorem Autosegmental.Graph.sum_label_inl {S : Type u_1} {X : Graph S} {Y : Graph S} (v : X.V) : (X.sum Y).label (Sum.inl v) = X.label v

@[simp]

theorem Autosegmental.Graph.sum_label_inr {S : Type u_1} {X : Graph S} {Y : Graph S} (v : Y.V) : (X.sum Y).label (Sum.inr v) = Y.label v

@[simp]

theorem Autosegmental.Graph.sum_arcs_inl_inl {S : Type u_1} {X : Graph S} {Y : Graph S} {v w : X.V} : (X.sum Y).arcs.Adj (Sum.inl v) (Sum.inl w) ↔ X.arcs.Adj v w

@[simp]

theorem Autosegmental.Graph.sum_arcs_inr_inr {S : Type u_1} {X : Graph S} {Y : Graph S} {v w : Y.V} : (X.sum Y).arcs.Adj (Sum.inr v) (Sum.inr w) ↔ Y.arcs.Adj v w

@[simp]

theorem Autosegmental.Graph.not_sum_arcs_inl_inr {S : Type u_1} {X : Graph S} {Y : Graph S} {v : X.V} {w : Y.V} : ¬(X.sum Y).arcs.Adj (Sum.inl v) (Sum.inr w)

@[simp]

theorem Autosegmental.Graph.not_sum_arcs_inr_inl {S : Type u_1} {X : Graph S} {Y : Graph S} {v : Y.V} {w : X.V} : ¬(X.sum Y).arcs.Adj (Sum.inr v) (Sum.inl w)

def Autosegmental.Graph.sumDesc {S : Type u_1} {X : Graph S} {Y : Graph S} {Z : Graph S} (f : X.Hom Z) (g : Y.Hom Z) : (X.sum Y).Hom Z

Copairing out of the bridge-free sum.

Equations

• Autosegmental.Graph.sumDesc f g = { toFun := Sum.elim f.toFun g.toFun, edge_map := ⋯, label_comp := ⋯ }

Category structure, initial object, and coproducts

@[implicit_reducible]

instance Autosegmental.Graph.instCategory {S : Type u_1} : CategoryTheory.Category.{u_3, max (u_3 + 1) u_1} (Graph S)

Equations

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

instance Autosegmental.Graph.instSubsingletonHomEmpty {S : Type u_1} (Y : Graph S) : Subsingleton (empty S ⟶ Y)

instance Autosegmental.Graph.instNonemptyHomEmpty {S : Type u_1} (Y : Graph S) : Nonempty (empty S ⟶ Y)

instance Autosegmental.Graph.instHasInitial {S : Type u_1} : CategoryTheory.Limits.HasInitial (Graph S)

def Autosegmental.Graph.inl {S : Type u_1} (X : Graph S) (Y : Graph S) : X ⟶ X.sum Y

Left coprojection.

Equations

• X.inl Y = { toFun := Sum.inl, edge_map := ⋯, label_comp := ⋯ }

def Autosegmental.Graph.inr {S : Type u_1} (X : Graph S) (Y : Graph S) : Y ⟶ X.sum Y

Right coprojection.

Equations

• X.inr Y = { toFun := Sum.inr, edge_map := ⋯, label_comp := ⋯ }

instance Autosegmental.Graph.instHasBinaryCoproduct {S : Type u_1} (X Y : Graph S) : CategoryTheory.Limits.HasBinaryCoproduct X Y

The bridge-free sum is the categorical coproduct of the broad category.

instance Autosegmental.Graph.instHasBinaryCoproducts {S : Type u_1} : CategoryTheory.Limits.HasBinaryCoproducts (Graph S)

def Autosegmental.Graph.precPreserving {S : Type u_1} : CategoryTheory.MorphismProperty (Graph S)

The property of morphisms that also preserve the order arcs; such maps are the model-theoretic full-structure homomorphisms.

Equations

• Autosegmental.Graph.precPreserving f = ∀ ⦃v w : X.V⦄, X.arcs.Adj v w → Y.arcs.Adj (f.toFun v) (f.toFun w)

instance Autosegmental.Graph.instIsMultiplicativePrecPreserving {S : Type u_1} : precPreserving.IsMultiplicative

theorem Autosegmental.Graph.Iso.toHom_precPreserving {S : Type u_1} {X Y : Graph S} (e : X.Iso Y) : precPreserving e.toHom

A full isomorphism's underlying morphism preserves precedence.

theorem Autosegmental.Graph.Hom.concatMap_precPreserving {S : Type u_1} {ι : Type u_2} {X₁ Y₁ : Graph S} {X₂ Y₂ : Graph S} (t : S → ι) {f : X₁.Hom Y₁} {g : X₂.Hom Y₂} (hf : precPreserving f) (hg : precPreserving g) : precPreserving (concatMap t f g)

The concatenation of precedence-preserving morphisms preserves precedence.