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

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

Main results

• RootedTree.Nonplanar.autCard_node: the recursion autCard (node a M) = forestAutCard M.
• RootedTree.Nonplanar.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.

RoseTree-representative substrate

treeAutCard computes |Aut(mk t)| on a planar RoseTree representative t; Perm-invariance (below) lets it descend to Nonplanar.autCard through the quotient.

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

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

Equations

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

@[irreducible]

def RootedTree.Nonplanar.treeAutCard {α : Type u_1} [DecidableEq α] : RoseTree α → ℕ

The automorphism count |Aut(mk t)| of the nonplanar tree represented by a planar RoseTree t; substrate for Nonplanar.autCard.

Equations

• RootedTree.Nonplanar.treeAutCard (RoseTree.node value cs) = (List.map RootedTree.Nonplanar.treeAutCard cs).prod * RootedTree.Nonplanar.multinomialFactor ↑(List.map RootedTree.Nonplanar.mk cs)

theorem RootedTree.Nonplanar.treeAutCard_node {α : Type u_1} [DecidableEq α] (a : α) (cs : List (RoseTree α)) : treeAutCard (RoseTree.node a cs) = (List.map treeAutCard cs).prod * multinomialFactor ↑(List.map mk cs)

treeAutCard is Perm-invariant

theorem RootedTree.Nonplanar.treeAutCard_perm {α : Type u_1} [DecidableEq α] {t s : RoseTree α} : t.Perm s → treeAutCard t = treeAutCard s

treeAutCard is invariant under RoseTree.Perm.

theorem RootedTree.Nonplanar.treeAutCard_permList {α : Type u_1} [DecidableEq α] {cs ds : List (RoseTree α)} : RoseTree.PermList cs ds → (List.map treeAutCard cs).prod = (List.map treeAutCard ds).prod ∧ ↑(List.map mk cs) = ↑(List.map mk ds)

The child-treeAutCard product and the mk-multiset are PermList-invariant.

Positivity of treeAutCard

theorem RootedTree.Nonplanar.treeAutCard_pos {α : Type u_1} [DecidableEq α] (t : RoseTree α) : 0 < treeAutCard t

treeAutCard is positive.

Nonplanar automorphism count via lift

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

The cardinality |Aut(t)| of the automorphism group of a rooted nonplanar tree: ∏_{distinct c ∈ M} (M.count c)! · autCard c ^ M.count c at node a M (autCard_node), 1 at a leaf (autCard_leaf).

Equations

• RootedTree.Nonplanar.autCard = RootedTree.Nonplanar.lift RootedTree.Nonplanar.treeAutCard ⋯

@[simp]

theorem RootedTree.Nonplanar.autCard_mk {α : Type u_1} [DecidableEq α] (t : RoseTree α) : (mk t).autCard = treeAutCard t

@[simp]

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

A leaf has trivial aut group.

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

autCard is positive: the automorphism group contains the identity.

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

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

Equations

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

@[simp]

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

The empty forest has trivial aut group.

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

forestAutCard is positive.

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

forestAutCard as the autCard-product over all members times the symmetry factor: the forest analogue of treeAutCard_node's shape.

@[simp]

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

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

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 (GrossmanLarsonPairing.pairing_of'_mul_of').

theorem RootedTree.Nonplanar.forestAutCard_add {α : Type u_1} [DecidableEq α] (F G : Multiset (Nonplanar α)) : 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|.