Automorphisms on Hepp-tree data

The group PlaneTree.Aut t is defined graph-theoretically, as the vertex permutations commuting with the total parent map. This file derives the concrete consequences needed in Proposition 5.6: child counts, leaves, and branch vertices are invariant, and markings and multiplicities can be transported along automorphisms.

def Anderson4D.graphChildren {t : PlaneTree} (v : t.VPos) : Finset t.VPos

Children described purely through the total parent map. The inequality removes the root from its own parent fiber.

Equations

• Anderson4D.graphChildren v = {w : t.VPos | Anderson4D.PlaneTree.parentV w = v ∧ w ≠ v}

@[simp]

theorem Anderson4D.mem_graphChildren {t : PlaneTree} {v w : t.VPos} : w ∈ graphChildren v ↔ PlaneTree.parentV w = v ∧ w ≠ v

theorem Anderson4D.card_graphChildren_eq_childCount {t : PlaneTree} (v : t.VPos) : (graphChildren v).card = t.childCount ↑v

The graph-theoretic parent fiber has the recursive child count.

Invariance under automorphisms

theorem Anderson4D.image_graphChildren_aut {t : PlaneTree} (g : t.Aut) (v : t.VPos) : Finset.image (⇑↑g) (graphChildren v) = graphChildren (↑g v)

A parent-commuting automorphism maps the child fiber of v bijectively onto the child fiber of g v.

theorem Anderson4D.childCount_aut {t : PlaneTree} (g : t.Aut) (v : t.VPos) : t.childCount ↑(↑g v) = t.childCount ↑v

Automorphisms preserve the number of children at every vertex.

theorem Anderson4D.aut_mem_Leaves_iff {t : PlaneTree} (g : t.Aut) (v : t.VPos) : ↑g v ∈ t.Leaves ↔ v ∈ t.Leaves

theorem Anderson4D.aut_mem_BranchNodes_iff {t : PlaneTree} (g : t.Aut) (v : t.VPos) : ↑g v ∈ t.BranchNodes ↔ v ∈ t.BranchNodes

def Anderson4D.autLeavesEquiv {t : PlaneTree} (g : t.Aut) : ↥t.Leaves ≃ ↥t.Leaves

The permutation induced by a tree automorphism on its leaves.

Equations

• Anderson4D.autLeavesEquiv g = Equiv.subtypeEquiv ↑g ⋯

def Anderson4D.autBranchNodesEquiv {t : PlaneTree} (g : t.Aut) : ↥t.BranchNodes ≃ ↥t.BranchNodes

The permutation induced by a tree automorphism on branch vertices.

Equations

• Anderson4D.autBranchNodesEquiv g = Equiv.subtypeEquiv ↑g ⋯

@[simp]

theorem Anderson4D.autLeavesEquiv_apply_val {t : PlaneTree} (g : t.Aut) (l : ↥t.Leaves) : ↑((autLeavesEquiv g) l) = ↑g ↑l

@[simp]

theorem Anderson4D.autBranchNodesEquiv_apply_val {t : PlaneTree} (g : t.Aut) (v : ↥t.BranchNodes) : ↑((autBranchNodesEquiv g) v) = ↑g ↑v

Transporting the structured Hepp data

def Anderson4D.smulHeppMarking {t : PlaneTree} (g : t.Aut) (Nm : t.HeppMarking) : t.HeppMarking

Reindex a Hepp marking along a tree automorphism.

Equations

• Anderson4D.smulHeppMarking g Nm = { Nexp := g • Nm.Nexp, pos := ⋯, parent_gt := ⋯ }

def Anderson4D.smulMultiplicities {t : PlaneTree} (g : t.Aut) (mu : t.Multiplicities) : t.Multiplicities

Reindex leaf multiplicities along a tree automorphism.

Equations

• Anderson4D.smulMultiplicities g mu = { m := fun (v : t.VPos) => mu.m (↑g⁻¹ v), two_le := ⋯ }

@[simp]

theorem Anderson4D.smulHeppMarking_Nexp {t : PlaneTree} (g : t.Aut) (Nm : t.HeppMarking) (v : t.VPos) : (smulHeppMarking g Nm).Nexp v = Nm.Nexp (↑g⁻¹ v)

@[simp]

theorem Anderson4D.smulMultiplicities_m {t : PlaneTree} (g : t.Aut) (mu : t.Multiplicities) (v : t.VPos) : (smulMultiplicities g mu).m v = mu.m (↑g⁻¹ v)

theorem Anderson4D.smulHeppMarking_canonicalRaw {t : PlaneTree} (g : t.Aut) (Nm : t.HeppMarking) : (smulHeppMarking g Nm).canonicalRaw = g • Nm.canonicalRaw

Structured transport agrees exactly with the raw marking action after canonical zero extension.

theorem Anderson4D.smulMultiplicities_canonicalRaw {t : PlaneTree} (g : t.Aut) (mu : t.Multiplicities) : (smulMultiplicities g mu).canonicalRaw = g • mu.canonicalRaw

Canonical leaf-only multiplicity data is transported by the same raw function action.

@[simp]

theorem Anderson4D.scaleN_smulHeppMarking {t : PlaneTree} (g : t.Aut) (Nm : t.HeppMarking) (v : t.VPos) : scaleN (smulHeppMarking g Nm) v = scaleN Nm (↑g⁻¹ v)

theorem Anderson4D.sum_smulMultiplicities {t : PlaneTree} (g : t.Aut) (mu : t.Multiplicities) : ∑ l : ↥t.Leaves, (smulMultiplicities g mu).m ↑l = ∑ l : ↥t.Leaves, mu.m ↑l

Total multiplicity is invariant under reindexing by an automorphism.

theorem Anderson4D.smulMultiplicities_even_iff {t : PlaneTree} (g : t.Aut) (mu : t.Multiplicities) : (∀ (l : ↥t.Leaves), Even ((smulMultiplicities g mu).m ↑l)) ↔ ∀ (l : ↥t.Leaves), Even (mu.m ↑l)

Leafwise parity is invariant under automorphism transport.