Restricted Hepp data

HeppMarking.Nexp and Multiplicities.m are stored as total functions on vertices, although paper Definition 5.1 only gives them meaning on branching vertices and leaves, respectively. This file supplies canonical zero extensions and equality interfaces which forget the off-support junk.

In particular, AutHeppMarked t Nm is the stabilizer of the canonical raw marking, rather than of Nm.Nexp itself. Thus neither this group nor its orbit--stabilizer count can depend on values of Nexp away from BranchNodes t.

def Anderson4D.PlaneTree.HeppMarking.canonicalRaw {t : PlaneTree} (Nm : t.HeppMarking) : t.Marking

The marking data of Nm, extended by zero away from the branching vertices. This is the raw marking on which automorphisms should act.

Equations

• Nm.canonicalRaw v = if v ∈ t.BranchNodes then Nm.Nexp v else 0

@[simp]

theorem Anderson4D.PlaneTree.HeppMarking.canonicalRaw_apply_of_mem {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∈ t.BranchNodes) : Nm.canonicalRaw v = Nm.Nexp v

@[simp]

theorem Anderson4D.PlaneTree.HeppMarking.canonicalRaw_apply_of_not_mem {t : PlaneTree} (Nm : t.HeppMarking) {v : t.VPos} (hv : v ∉ t.BranchNodes) : Nm.canonicalRaw v = 0

def Anderson4D.PlaneTree.HeppMarking.EqOnBranch {t : PlaneTree} (Nm Nm' : t.HeppMarking) : Prop

Semantic equality of Hepp markings: equality only at branching vertices. The total-function fields may differ away from BranchNodes t.

Equations

• Nm.EqOnBranch Nm' = ∀ v ∈ t.BranchNodes, Nm.Nexp v = Nm'.Nexp v

theorem Anderson4D.PlaneTree.HeppMarking.eqOnBranch_refl {t : PlaneTree} (Nm : t.HeppMarking) : Nm.EqOnBranch Nm

theorem Anderson4D.PlaneTree.HeppMarking.eqOnBranch_symm {t : PlaneTree} {Nm Nm' : t.HeppMarking} (h : Nm.EqOnBranch Nm') : Nm'.EqOnBranch Nm

theorem Anderson4D.PlaneTree.HeppMarking.eqOnBranch_trans {t : PlaneTree} {Nm₁ Nm₂ Nm₃ : t.HeppMarking} (h₁₂ : Nm₁.EqOnBranch Nm₂) (h₂₃ : Nm₂.EqOnBranch Nm₃) : Nm₁.EqOnBranch Nm₃

theorem Anderson4D.PlaneTree.HeppMarking.canonicalRaw_eq_iff {t : PlaneTree} {Nm Nm' : t.HeppMarking} : Nm.canonicalRaw = Nm'.canonicalRaw ↔ Nm.EqOnBranch Nm'

Two Hepp markings have the same canonical raw marking exactly when their meaningful values agree on every branching vertex.

theorem Anderson4D.PlaneTree.HeppMarking.canonicalRaw_ext {t : PlaneTree} {Nm Nm' : t.HeppMarking} (h : ∀ v ∈ t.BranchNodes, Nm.Nexp v = Nm'.Nexp v) : Nm.canonicalRaw = Nm'.canonicalRaw

Extensionality for canonical raw markings: only branch values need be compared.

@[reducible, inline]

abbrev Anderson4D.PlaneTree.AutHeppMarked (t : PlaneTree) (Nm : t.HeppMarking) : Subgroup t.Aut

Automorphisms of the marked Hepp tree (t, Nm). The stabilizer is taken after zero-extending Nm away from the branching vertices, so it is independent of the junk values in the total field Nm.Nexp.

Equations

• t.AutHeppMarked Nm = t.AutMarked Nm.canonicalRaw

@[simp]

theorem Anderson4D.PlaneTree.mem_autHeppMarked_iff {t : PlaneTree} {Nm : t.HeppMarking} {g : t.Aut} : g ∈ t.AutHeppMarked Nm ↔ g • Nm.canonicalRaw = Nm.canonicalRaw

theorem Anderson4D.PlaneTree.autHeppMarked_congr {t : PlaneTree} {Nm Nm' : t.HeppMarking} (h : Nm.EqOnBranch Nm') : t.AutHeppMarked Nm = t.AutHeppMarked Nm'

Semantically equal markings have literally the same marked-tree automorphism subgroup.

theorem Anderson4D.PlaneTree.card_orbit_mul_card_autHeppMarked (t : PlaneTree) (Nm : t.HeppMarking) : (MulAction.orbit t.Aut Nm.canonicalRaw).toFinset.card * Fintype.card ↥(t.AutHeppMarked Nm) = Fintype.card t.Aut

Orbit--stabilizer for the paper-faithful marked-tree automorphism group. No value of Nm.Nexp away from BranchNodes t occurs in this statement.

def Anderson4D.PlaneTree.Multiplicities.canonicalRaw {t : PlaneTree} (mu : t.Multiplicities) : t.VPos → ℕ

The multiplicity data of mu, extended by zero away from the leaves.

Equations

• mu.canonicalRaw v = if v ∈ t.Leaves then mu.m v else 0

@[simp]

theorem Anderson4D.PlaneTree.Multiplicities.canonicalRaw_apply_of_mem {t : PlaneTree} (mu : t.Multiplicities) {v : t.VPos} (hv : v ∈ t.Leaves) : mu.canonicalRaw v = mu.m v

@[simp]

theorem Anderson4D.PlaneTree.Multiplicities.canonicalRaw_apply_of_not_mem {t : PlaneTree} (mu : t.Multiplicities) {v : t.VPos} (hv : v ∉ t.Leaves) : mu.canonicalRaw v = 0

def Anderson4D.PlaneTree.Multiplicities.EqOnLeaves {t : PlaneTree} (mu mu' : t.Multiplicities) : Prop

Semantic equality of multiplicities: equality only at leaves.

Equations

• mu.EqOnLeaves mu' = ∀ v ∈ t.Leaves, mu.m v = mu'.m v

theorem Anderson4D.PlaneTree.Multiplicities.eqOnLeaves_refl {t : PlaneTree} (mu : t.Multiplicities) : mu.EqOnLeaves mu

theorem Anderson4D.PlaneTree.Multiplicities.eqOnLeaves_symm {t : PlaneTree} {mu mu' : t.Multiplicities} (h : mu.EqOnLeaves mu') : mu'.EqOnLeaves mu

theorem Anderson4D.PlaneTree.Multiplicities.eqOnLeaves_trans {t : PlaneTree} {mu₁ mu₂ mu₃ : t.Multiplicities} (h₁₂ : mu₁.EqOnLeaves mu₂) (h₂₃ : mu₂.EqOnLeaves mu₃) : mu₁.EqOnLeaves mu₃

theorem Anderson4D.PlaneTree.Multiplicities.canonicalRaw_eq_iff {t : PlaneTree} {mu mu' : t.Multiplicities} : mu.canonicalRaw = mu'.canonicalRaw ↔ mu.EqOnLeaves mu'

Two multiplicity structures have the same canonical raw function exactly when their meaningful values agree at every leaf.

theorem Anderson4D.PlaneTree.Multiplicities.canonicalRaw_ext {t : PlaneTree} {mu mu' : t.Multiplicities} (h : ∀ v ∈ t.Leaves, mu.m v = mu'.m v) : mu.canonicalRaw = mu'.canonicalRaw

Extensionality for canonical multiplicity functions: only leaf values need be compared.