Geometric invariance under Hepp-tree automorphisms

This file proves that the path-based notions used by admissibility are intrinsic to the parent graph. In particular automorphisms preserve the ancestor relation and least common ancestors. These are the nontrivial transport facts behind paper Proposition 5.6, Step 1.

def Anderson4D.IsAncestor {t : PlaneTree} (v w : t.VPos) : Prop

Graph-theoretic ancestry: travel through zero or more child edges.

Equations

• Anderson4D.IsAncestor v w = Relation.ReflTransGen (fun (a b : t.VPos) => b ∈ Anderson4D.graphChildren a) v w

theorem Anderson4D.IsAncestor.refl {t : PlaneTree} (v : t.VPos) : IsAncestor v v

theorem Anderson4D.IsAncestor.prefix {t : PlaneTree} {v w : t.VPos} (h : IsAncestor v w) : ↑v <+: ↑w

Graph ancestry is the same as prefix ancestry of position paths.

theorem Anderson4D.isAncestor_of_prefix {t : PlaneTree} (v w : t.VPos) (hpre : ↑v <+: ↑w) : IsAncestor v w

Conversely, every path prefix is a chain of graph-child edges.

theorem Anderson4D.isAncestor_iff_prefix {t : PlaneTree} (v w : t.VPos) : IsAncestor v w ↔ ↑v <+: ↑w

theorem Anderson4D.IsAncestor.map_aut {t : PlaneTree} {v w : t.VPos} (h : IsAncestor v w) (g : t.Aut) : IsAncestor (↑g v) (↑g w)

Automorphisms preserve graph ancestry.

theorem Anderson4D.isAncestor_aut_iff {t : PlaneTree} (g : t.Aut) (v w : t.VPos) : IsAncestor (↑g v) (↑g w) ↔ IsAncestor v w

Least common ancestors

theorem Anderson4D.lcaV_ancestor_left {t : PlaneTree} (v w : t.VPos) : IsAncestor (lcaV v w) v

theorem Anderson4D.lcaV_ancestor_right {t : PlaneTree} (v w : t.VPos) : IsAncestor (lcaV v w) w

theorem Anderson4D.IsAncestor.to_lcaV {t : PlaneTree} {u v w : t.VPos} (huv : IsAncestor u v) (huw : IsAncestor u w) : IsAncestor u (lcaV v w)

Universal property of the least common ancestor.

theorem Anderson4D.lcaV_aut {t : PlaneTree} (g : t.Aut) (v w : t.VPos) : ↑g (lcaV v w) = lcaV (↑g v) (↑g w)

Tree automorphisms preserve least common ancestors.

Children and subtree leaves

theorem Anderson4D.childrenOf_eq_graphChildren {t : PlaneTree} (v : t.VPos) : childrenOf v = graphChildren v

The path-based childrenOf is exactly the graph parent fiber.

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

Automorphisms carry the children finset to the children finset.

theorem Anderson4D.image_leavesUnder_aut {t : PlaneTree} (g : t.Aut) (v : t.VPos) : Finset.image (⇑(autLeavesEquiv g)) (leavesUnder v) = leavesUnder (↑g v)

Automorphisms carry all leaves below a vertex to all leaves below its image.

Admissible embeddings

def Anderson4D.smulLeafEmbedding {t : PlaneTree} (g : t.Aut) (z : LeafEmbedding t) : LeafEmbedding t

Reindex a leaf embedding by the induced leaf permutation.

Equations

• Anderson4D.smulLeafEmbedding g z = Anderson4D.reindexLeafEmbedding (Anderson4D.autLeavesEquiv g) z

@[simp]

theorem Anderson4D.smulLeafEmbedding_apply_aut {t : PlaneTree} (g : t.Aut) (z : LeafEmbedding t) (l : ↥t.Leaves) : smulLeafEmbedding g z ((autLeavesEquiv g) l) = z l

theorem Anderson4D.IsLink.map_aut {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v c c' : t.VPos} (h : IsLink Nm z v c c') (g : t.Aut) : IsLink (smulHeppMarking g Nm) (smulLeafEmbedding g z) (↑g v) (↑g c) (↑g c')

One child link is preserved by simultaneous transport of the marking, embedding, and vertices.

theorem Anderson4D.LinkedChildren.map_aut {t : PlaneTree} {Nm : t.HeppMarking} {z : LeafEmbedding t} {v : t.VPos} (h : LinkedChildren Nm z v) (g : t.Aut) : LinkedChildren (smulHeppMarking g Nm) (smulLeafEmbedding g z) (↑g v)

LinkedChildren is invariant in the forward direction under a tree automorphism.

theorem Anderson4D.IsAdmissible.map_aut {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : LeafEmbedding t} (h : IsAdmissible Nm M z) (g : t.Aut) : IsAdmissible (smulHeppMarking g Nm) M (smulLeafEmbedding g z)

Admissibility is preserved by simultaneous automorphism transport.