The symmetry-weighted pairing on forests

This file defines the pairing on H = ConnesKreimer R (UnorderedTree α) that makes the forests an orthogonal basis, each forest paired with itself to its number of symmetries: ⟨of' F, of' G⟩ = if F = G then |Aut F| else 0. Foissy uses this pairing in his dual construction of the Connes–Kreimer coproduct; here it makes the Grossman–Larson product dual to the pruning coproduct (Coproduct/PruningDuality.lean).

Main definitions

• GrossmanLarson.pairing: the symmetry-weighted pairing.
• GrossmanLarson.pairing₂: its extension to H ⊗ H.

Main results

• GrossmanLarson.pairing_symm: the pairing is symmetric.
• GrossmanLarson.pairing_of': pairing with a forest takes the coefficient of that forest, times its number of symmetries.
• GrossmanLarson.pairing_nondegenerate: the pairing is nondegenerate over a ring of characteristic zero without zero divisors.
• GrossmanLarson.pairing_of'_mul, GrossmanLarson.pairing_product_of'_mul_of': pairing against a Connes–Kreimer product splits a basis forest over its antidiagonal, and splits both factors of a Grossman–Larson product.

References

• [Foi21]
• [GL89]
• [OG08]

The bilinear pairing

noncomputable def GrossmanLarson.pairing {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α) →ₗ[R] R

pairing (of' F) (of' G) is the number of symmetries of F when F = G, and 0 otherwise.

Equations

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

@[simp]

theorem GrossmanLarson.pairing_of'_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F G : UnorderedTree.Forest (UnorderedTree α)) : (pairing (ConnesKreimer.of' F)) (ConnesKreimer.of' G) = if F = G then ↑(UnorderedTree.forestAutCard F) else 0

theorem GrossmanLarson.pairing_symm {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x y : ConnesKreimer R (UnorderedTree α)) : (pairing x) y = (pairing y) x

The pairing is symmetric.

@[simp]

theorem GrossmanLarson.pairing_zero_left {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (y : ConnesKreimer R (UnorderedTree α)) : (pairing 0) y = 0

@[simp]

theorem GrossmanLarson.pairing_zero_right {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x : ConnesKreimer R (UnorderedTree α)) : (pairing x) 0 = 0

theorem GrossmanLarson.pairing_one_right {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (w : ConnesKreimer R (UnorderedTree α)) : (pairing w) 1 = ConnesKreimer.counit w

Pairing against the unit gives the counit, the coefficient of the empty forest.

theorem GrossmanLarson.pairing_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (F : UnorderedTree.Forest (UnorderedTree α)) : pairing (ConnesKreimer.of' F) = ↑(UnorderedTree.forestAutCard F) • ConnesKreimer.lcoeff R F

Pairing with of' F takes the coefficient of F, weighted by the symmetries of F.

theorem GrossmanLarson.pairing_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x : ConnesKreimer R (UnorderedTree α)) (G : UnorderedTree.Forest (UnorderedTree α)) : (pairing x) (ConnesKreimer.of' G) = x.coeff G * ↑(UnorderedTree.forestAutCard G)

Pairing against of' G gives the coefficient of G, weighted by the symmetries of G.

theorem GrossmanLarson.pairing_nondegenerate {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] [CharZero R] [NoZeroDivisors R] (x : ConnesKreimer R (UnorderedTree α)) (h : ∀ (y : ConnesKreimer R (UnorderedTree α)), (pairing x) y = 0) : x = 0

Over a ring of characteristic zero without zero divisors, the pairing is nondegenerate.

theorem GrossmanLarson.ext_pairing_right {α : Type u_2} [DecidableEq α] {R : Type u_3} [CommRing R] [CharZero R] [NoZeroDivisors R] {x y : ConnesKreimer R (UnorderedTree α)} (h : ∀ (z : ConnesKreimer R (UnorderedTree α)), (pairing x) z = (pairing y) z) : x = y

Elements that pair equally against everything are equal.

Product rule

Pairing against a Connes–Kreimer product splits the basis forest over its antidiagonal; the weights recombine by UnorderedTree.forestAutCard_add.

theorem GrossmanLarson.pairing_of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (W C₁ C₂ : UnorderedTree.Forest (UnorderedTree α)) : (pairing (ConnesKreimer.of' W)) (ConnesKreimer.of' C₁ * ConnesKreimer.of' C₂) = (Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (pairing (ConnesKreimer.of' p.1)) (ConnesKreimer.of' C₁) * (pairing (ConnesKreimer.of' p.2)) (ConnesKreimer.of' C₂)) (Multiset.antidiagonal W)).sum

⟨W, C₁ · C₂⟩ is the sum, over the splittings W = W₁ + W₂, of ⟨W₁, C₁⟩ · ⟨W₂, C₂⟩.

theorem GrossmanLarson.pairing_of'_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (W : UnorderedTree.Forest (UnorderedTree α)) (z₁ z₂ : ConnesKreimer R (UnorderedTree α)) : (pairing (ConnesKreimer.of' W)) (z₁ * z₂) = (Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (pairing (ConnesKreimer.of' p.1)) z₁ * (pairing (ConnesKreimer.of' p.2)) z₂) (Multiset.antidiagonal W)).sum

Pairing a basis forest against a product splits the forest over its antidiagonal.

theorem GrossmanLarson.pairing_product_of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (A B C₁ C₂ : UnorderedTree.Forest (UnorderedTree α)) : (pairing ((product (ConnesKreimer.of' A)) (ConnesKreimer.of' B))) (ConnesKreimer.of' C₁ * ConnesKreimer.of' C₂) = (Multiset.map (fun (pq : (Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (pairing ((product (ConnesKreimer.of' pq.1.1)) (ConnesKreimer.of' pq.2.1))) (ConnesKreimer.of' C₁) * (pairing ((product (ConnesKreimer.of' pq.1.2)) (ConnesKreimer.of' pq.2.2))) (ConnesKreimer.of' C₂)) (Multiset.antidiagonal A ×ˢ Multiset.antidiagonal B)).sum

Pairing a Grossman–Larson product against a Connes–Kreimer product splits both of its factors, ⟨A ⋆ B, C₁ · C₂⟩ = Σ_{A = A₁ + A₂} Σ_{B = B₁ + B₂} ⟨A₁ ⋆ B₁, C₁⟩ ⟨A₂ ⋆ B₂, C₂⟩.

The pairing on H ⊗ H

The duality with the pruning coproduct is stated on H ⊗ H. No such duality holds for a coproduct that leaves marker leaves in the trunk, since grafting never produces them.

noncomputable def GrossmanLarson.pairing₂ {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)) →ₗ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)) →ₗ[R] R

pairing₂ is the pairing on H ⊗ H with pairing₂ (x ⊗ y) (w ⊗ z) = ⟨x, w⟩ * ⟨y, z⟩.

Equations

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

@[simp]

theorem GrossmanLarson.pairing₂_tmul_tmul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x y w z : ConnesKreimer R (UnorderedTree α)) : (pairing₂ (x ⊗ₜ[R] y)) (w ⊗ₜ[R] z) = (pairing x) w * (pairing y) z