The symmetry-weighted GL/CK pairing #
[foissy-typed-decorated-rooted-trees-2018] [grossman-larson-1989]
The pairing ⟨·, ·⟩ : H →ₗ H →ₗ R on H = ConnesKreimer R (Nonplanar α)
(Foissy 2018 §4.2), symmetry-weighted on the forest basis:
⟨of' F, of' G⟩ = if F = G then |Aut(F)| else 0
with the automorphism count Nonplanar.forestAutCard
(Core/Combinatorics/RootedTree/Aut.lean) as the weight. This is the
pairing under which the GL product and the pruning coproduct Δ^ρ are
adjoint (Coproduct/PruningDuality.lean).
Main results #
pairing_symm— symmetry.pairing_nondegenerate,ext_pairing_right— nondegeneracy and its separation form, over[CharZero R] [NoZeroDivisors R].pairing_of'_mul_of',pairing_of'_mul— the product rule: pairing against a CK product decomposes overantidiagonalsplits.pairing₂,pairing₃— the tensor-square and -cube extensions, with nondegeneracy lifted along the forest basis; the instruments through which the Δ^ρ duality is stated and transported.
[UPSTREAM] candidate. Sorry-free.
The bilinear pairing #
The symmetry-weighted pairing ⟨·, ·⟩ : H × H → R. On basis
elements, ⟨of' F, of' G⟩ = if F = G then forestAutCard F else 0
(in R, via Nat.cast). Bilinearly extended, transported from the
forest-basis pairingAux through ConnesKreimer.toFinsuppAlgEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pairing is symmetric. Reduces by bilinearity to the basis case,
where pairing_of'_of' shows both sides are if F = G then forestAutCard F else 0 — same value (the F = G case forces it).
The pairing vanishes on 0. Free from linearity.
The pairing vanishes on 0 (right).
Pairing against the unit extracts the counit (the coefficient of the
empty forest): ⟨w, 1⟩ = ε w.
Each pairing against a basis element of' G extracts the coefficient
of G in x, weighted by forestAutCard G. Proof: reduce to basis
via Finsupp.induction_linear on x, then pairing_of'_of'.
Non-degeneracy of the pairing over CharZero R with no zero
divisors. If pairing x y = 0 for all y, then x = 0. Uses
pairing_apply_of' (coefficient extraction) + forestAutCard_pos
(positivity) + Nat.cast_ne_zero (CharZero R has no Nat-cast torsion)
mul_eq_zero(NoZeroDivisors R).
Holds for any commutative ring with characteristic 0 and no zero
divisors (e.g. ℤ, ℚ, ℝ, ℂ, any field of char 0).
Separation form of pairing_nondegenerate: elements pairing equally
against everything are equal.
Product rule #
Pairing against a CK product decomposes over the two-sided sub-multiset
splits of the first argument (Multiset.antidiagonal) — the
symmetry-weighted pairing turns CK multiplication into the split
coproduct. The combinatorial heart is the multinomial identity
Nonplanar.forestAutCard_add (Aut.lean). Computationally validated
(scratch/validate_duality.lean, V2 battery).
Pairing product rule (basis form):
⟨W, C₁ · C₂⟩ = Σ_{W = W₁ + W₂} ⟨W₁, C₁⟩ · ⟨W₂, C₂⟩.
Only the split (C₁, C₂) survives the diagonal pairing, with
multiplicity count (C₁,C₂) (antidiagonal W); the autCard weights
recombine via Nonplanar.forestAutCard_add.
Pairing product rule (bilinear form): pairing a basis vector
against a product decomposes over the antidiagonal splits of the
basis forest. Bilinear extension of pairing_of'_mul_of'.
Tensor-extended pairings #
The pairing ⟨·, ·⟩ above extends to the
tensor square (pairing₂) and cube (pairing₃). These power the GL/CK
duality for the deletion coproduct Δ^ρ (Coproduct/PruningDuality.lean:
⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z)). For the trace variant Δ^c no
such duality holds — the trunk of a proper cut contains trace-marker
leaves that GL grafting can never produce — so Δ^c coassociativity
(comulCN_coassoc, Coproduct/Trace.lean) is a separate
combinatorial statement.
The tensor-extended pairing H ⊗ H →ₗ H ⊗ H →ₗ R, defined by
pairing₂ (x ⊗ y) (w ⊗ z) = pairing x w * pairing y z and extended
bilinearly.
Implementation: reshuffle (x⊗y)⊗(w⊗z) to (x⊗w)⊗(y⊗z) via
tensorTensorTensorComm; apply TP.map pair pair where
pair = TP.lift pairing : H ⊗ H →ₗ R; contract via mul' R R;
curry the result.
Decoration-free: works on ConnesKreimer R (Nonplanar α) for any
α. Consumed by the Δ^ρ duality (Coproduct/PruningDuality.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation of pairing₂ on pure tensors: pairing₂ (x ⊗ y) (w ⊗ z) = pairing x w * pairing y z.
The triple-tensor pairing H ⊗ (H ⊗ H) →ₗ H ⊗ (H ⊗ H) →ₗ R,
defined on pure tensors by
pairing₃ (a ⊗ (b ⊗ c)) (x ⊗ (y ⊗ z)) = pairing a x · pairing b y · pairing c z.
Consumed by the Δ^ρ duality chain (Coproduct/PruningDuality.lean):
coassociativity is transported through pairing₃_unique by pairing
against arbitrary x ⊗ (y ⊗ z) triple tensors.
Implementation: pairing on the first factor times pairing₂ on the
second factor; both extended bilinearly.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluation of pairing₃ on pure tensors.
Reduction helpers: pairing₃ on shifted-tensor forms #
Two reduction lemmas that express pairing₃ (x ⊗ (y ⊗ z')) evaluated on
shifted tensor forms in terms of pairing₂ and binary pairing,
consumed by the Δ^ρ duality chain in Coproduct/PruningDuality.lean.
Both are proved by TensorProduct.induction_on, reducing to the
pure-tensor case where pairing₃_tmul_tmul_tmul and
pairing₂_tmul_tmul agree.
pairing₃ (x ⊗ (y ⊗ z')) ∘ assoc on a (U ⊗ c)-shape tensor:
factors as pairing₂ (x ⊗ y) U * pairing z' c. Generic in α
(the trace decoration is irrelevant).
pairing₃ (x ⊗ (y ⊗ z')) on a (a ⊗ S)-shape tensor: factors as
pairing x a * pairing₂ (y ⊗ z') S. Generic in α.
Nondegeneracy of pairing₂ and pairing₃ (lifted from binary) #
pairing₂ and pairing₃ are nondegenerate over [CharZero R] [NoZeroDivisors R], lifted from binary pairing_nondegenerate via the
natural basis of CK = (Forest T) →₀ R.
Nondegeneracy of pairing₃, lifted from pairing₂_nondegenerate
along the basis of the outer tensor factor.