Automorphism cardinality for rooted nonplanar trees

For a rooted nonplanar tree whose children form the multiset M = {c₁ × k₁, …, cₙ × kₙ} (distinct subtrees cᵢ with multiplicity kᵢ), the automorphism group has cardinality ∏ᵢ kᵢ! · |Aut(cᵢ)| ^ kᵢ; the same formula applied to the top-level multiset counts the automorphisms of a forest.

Main definitions

• UnorderedTree.autCard: the automorphism count |Aut(t)| of a rooted nonplanar tree.
• UnorderedTree.forestAutCard: the automorphism count of a forest (multiset of rooted nonplanar trees).

Main results

• UnorderedTree.autCard_node: the recursion autCard (node a M) = forestAutCard M.
• UnorderedTree.forestAutCard_add: the multinomial split identity forestAutCard (F + G) = (antidiagonal (F + G)).count (F, G) * (forestAutCard F * forestAutCard G), the combinatorial core of the pairing's product-coproduct adjunction.

def UnorderedTree.multinomialFactor {α : Type u_1} [DecidableEq α] (M : Multiset (UnorderedTree α)) : ℕ

Symmetry-factor at one node: ∏_{distinct c ∈ M} (M.count c)!.

Equations

• UnorderedTree.multinomialFactor M = ∏ t ∈ M.toFinset, (Multiset.count t M).factorial

def UnorderedTree.autCard {α : Type u_1} [DecidableEq α] : UnorderedTree α → ℕ

The cardinality |Aut(t)| of the automorphism group of a rooted nonplanar tree: the product of the children's counts times the symmetry factor of the children (autCard_node).

Equations

• UnorderedTree.autCard = UnorderedTree.para fun (x : α) (ps : Multiset (UnorderedTree α × ℕ)) => (Multiset.map Prod.snd ps).prod * UnorderedTree.multinomialFactor (Multiset.map Prod.fst ps)

def UnorderedTree.forestAutCard {α : Type u_1} [DecidableEq α] (F : Multiset (UnorderedTree α)) : ℕ

The automorphism count |Aut(F)| of a forest of nonplanar trees, ∏_{distinct T ∈ F} (F.count T)! · autCard T ^ F.count T.

Equations

• UnorderedTree.forestAutCard F = ∏ t ∈ F.toFinset, (Multiset.count t F).factorial * t.autCard ^ Multiset.count t F

@[simp]

theorem UnorderedTree.forestAutCard_zero {α : Type u_1} [DecidableEq α] : forestAutCard 0 = 1

The empty forest has trivial aut group.

@[simp]

theorem UnorderedTree.forestAutCard_singleton {α : Type u_1} [DecidableEq α] (T : UnorderedTree α) : forestAutCard {T} = T.autCard

A singleton forest has the aut group of its tree.

theorem UnorderedTree.forestAutCard_eq_prod_mul_multinomialFactor {α : Type u_1} [DecidableEq α] (F : Multiset (UnorderedTree α)) : forestAutCard F = (Multiset.map autCard F).prod * multinomialFactor F

forestAutCard as the autCard-product over all members times the symmetry factor.

@[simp]

theorem UnorderedTree.autCard_node {α : Type u_1} [DecidableEq α] (a : α) (F : Multiset (UnorderedTree α)) : (node a F).autCard = forestAutCard F

autCard at a node is forestAutCard of the children: the recursive formula.

@[simp]

theorem UnorderedTree.autCard_leaf {α : Type u_1} [DecidableEq α] (a : α) : (leaf a).autCard = 1

A leaf has trivial aut group.

theorem UnorderedTree.autCard_pos {α : Type u_1} [DecidableEq α] (t : UnorderedTree α) : 0 < t.autCard

autCard is positive: the automorphism group contains the identity.

theorem UnorderedTree.forestAutCard_pos {α : Type u_1} [DecidableEq α] (F : Multiset (UnorderedTree α)) : 0 < forestAutCard F

forestAutCard is positive.

Multinomial split identity

Multiset.count_antidiagonal_eq_count_powerset and Multiset.count_powerset_of_le compute the split multiplicity; Nat.add_choose_mul_factorial_mul_factorial recombines it with the factorials per distinct tree. This identity is the combinatorial core of the pairing's product-coproduct adjunction (GrossmanLarson.pairing_of'_mul_of').

theorem UnorderedTree.forestAutCard_add {α : Type u_1} [DecidableEq α] (F G : Multiset (UnorderedTree α)) : forestAutCard (F + G) = Multiset.count (F, G) (F + G).antidiagonal * (forestAutCard F * forestAutCard G)

Multinomial split identity for forestAutCard: |Aut (F+G)| = count (F,G) (antidiagonal (F+G)) · |Aut F| · |Aut G|.