The universal property of the syntactic-object carrier

Leaf data valued in a commutative magma with zero extends to a morphism of magmas out of SyntacticObject (lift, the FreeMagma.lift analogue), and two such morphisms agreeing on the leaves are equal (hom_ext). The zero absorbs the off-carrier arities, so one total algebra (mergeAlgebra) drives the fold, the quotient descent, and the subtype restriction once and for all: consumers supply a lexical-leaf value and a trace value, and inherit Perm-invariance from mul_comm via List.Perm.congr_arity₂ — no bespoke step induction.

Main declarations

• Minimalist.SyntacticObject.mergeAlgebra: the node algebra induced by a magma-with-zero — lexical leaf ↦ ℓ, trace leaf ↦ τ, bare binary node ↦ *, other arities ↦ 0.
• Minimalist.SyntacticObject.liftN: its evaluation on the nonplanar carrier.
• Minimalist.SyntacticObject.liftFun, Minimalist.SyntacticObject.lift: the induced map on syntactic objects, unbundled (computable) and as →ₙ*.

Main results

• Minimalist.SyntacticObject.hom_ext: morphisms of magmas out of SyntacticObject agreeing on lexical and trace leaves are equal.
• Minimalist.SyntacticObject.liftN_node: the nonplanar magma law.

def Minimalist.SyntacticObject.mergeAlgebra {β : Type u_1} [Mul β] [Zero β] (ℓ : LIToken → β) (τ : β) : SOLabel → List β → β

The node algebra of a magma-with-zero: lexical leaf ↦ ℓ, trace leaf ↦ τ, bare binary node ↦ *, off-carrier arities ↦ 0.

Equations

• Minimalist.SyntacticObject.mergeAlgebra ℓ τ (Sum.inl tok) x✝ = ℓ tok
• Minimalist.SyntacticObject.mergeAlgebra ℓ τ (Sum.inr PUnit.unit) [] = τ
• Minimalist.SyntacticObject.mergeAlgebra ℓ τ (Sum.inr PUnit.unit) [x_2, y] = x_2 * y
• Minimalist.SyntacticObject.mergeAlgebra ℓ τ (Sum.inr PUnit.unit) x✝ = 0

theorem Minimalist.SyntacticObject.mergeAlgebra_perm {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (a : SOLabel) {l₁ l₂ : List β} (h : l₁.Perm l₂) : mergeAlgebra ℓ τ a l₁ = mergeAlgebra ℓ τ a l₂

mergeAlgebra is invariant under permutation of the daughter values: only the binary shape is order-sensitive, and there mul_comm applies.

def Minimalist.SyntacticObject.liftN {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) : RootedTree.Nonplanar SOLabel → β

The induced algebra on the nonplanar carrier: the catamorphism descends by mergeAlgebra_perm.

Equations

• Minimalist.SyntacticObject.liftN ℓ τ = RootedTree.Nonplanar.lift (RoseTree.fold (Minimalist.SyntacticObject.mergeAlgebra ℓ τ)) ⋯

@[simp]

theorem Minimalist.SyntacticObject.liftN_mk {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (p : RoseTree SOLabel) : liftN ℓ τ (RootedTree.Nonplanar.mk p) = RoseTree.fold (mergeAlgebra ℓ τ) p

theorem Minimalist.SyntacticObject.liftN_node {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (a b : RootedTree.Nonplanar SOLabel) : liftN ℓ τ (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = liftN ℓ τ a * liftN ℓ τ b

The nonplanar magma law: Merge multiplies values.

def Minimalist.SyntacticObject.liftFun {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (s : SyntacticObject) : β

The induced map on syntactic objects, unbundled — computable, decide-friendly.

Equations

• Minimalist.SyntacticObject.liftFun ℓ τ s = Minimalist.SyntacticObject.liftN ℓ τ ↑s

@[simp]

theorem Minimalist.SyntacticObject.liftFun_lexLeaf {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (tok : LIToken) : liftFun ℓ τ (lexLeaf tok) = ℓ tok

@[simp]

theorem Minimalist.SyntacticObject.liftFun_traceLeaf {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) : liftFun ℓ τ traceLeaf = τ

@[simp]

theorem Minimalist.SyntacticObject.liftFun_node {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (l r : SyntacticObject) : liftFun ℓ τ (l.node r) = liftFun ℓ τ l * liftFun ℓ τ r

noncomputable def Minimalist.SyntacticObject.lift {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) : SyntacticObject →ₙ* β

The universal property, existence half (cf. FreeMagma.lift): leaf data extends to a morphism of magmas out of the carrier.

Equations

• Minimalist.SyntacticObject.lift ℓ τ = { toFun := Minimalist.SyntacticObject.liftFun ℓ τ, map_mul' := ⋯ }

@[simp]

theorem Minimalist.SyntacticObject.lift_apply {β : Type u_1} [CommMagma β] [Zero β] (ℓ : LIToken → β) (τ : β) (s : SyntacticObject) : (lift ℓ τ) s = liftFun ℓ τ s

theorem Minimalist.SyntacticObject.hom_ext {β : Type u_1} [Mul β] {f g : SyntacticObject →ₙ* β} (hlex : ∀ (tok : LIToken), f (lexLeaf tok) = g (lexLeaf tok)) (htrace : f traceLeaf = g traceLeaf) : f = g

The universal property, uniqueness half: morphisms agreeing on the leaves are equal.