Documentation

BGW.StableTrees.MarchalLawInverse

Recovering parent graphs from Marchal grafts #

An isomorphism of grafts that preserves the new leaf restricts to the old vertices. In an edge graft it also preserves the new leaf's unique neighbour, the midpoint, and the missing edge can be recovered from its neighbours.

source
def BGW.StableTrees.Marchal.removeLastEquiv {m m' : ℕ} (e : Fin (m + 1) ≃ Fin (m' + 1)) (he : e (Fin.last m) = Fin.last m') :
Fin m ≃ Fin m'

Restrict an equivalence preserving the last element to the preceding elements.

Equations
Instances For
    source
    @[simp]
    theorem BGW.StableTrees.Marchal.removeLastEquiv_castSucc {m m' : ℕ} (e : Fin (m + 1) ≃ Fin (m' + 1)) (he : e (Fin.last m) = Fin.last m') (x : Fin m) :
    ((removeLastEquiv e he) x).castSucc = e x.castSucc
    source
    def BGW.StableTrees.Marchal.ungraftVertexIso {n : ℕ} {T T' : LTree n} {v : { v : Fin T.m // 3 ≤ T.G.degree v }} {v' : { v : Fin T'.m // 3 ≤ T'.G.degree v }} (e : graftGraph T.G (Sum.inr v) ≃g graftGraph T'.G (Sum.inr v')) (he : e (Fin.last T.m) = Fin.last T'.m) :
    T.G ≃g T'.G

    An isomorphism of vertex grafts preserving the new leaf recovers their parents.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.Marchal.ungraftVertexIso_position {n : ℕ} {T T' : LTree n} {v : { v : Fin T.m // 3 ≤ T.G.degree v }} {v' : { v : Fin T'.m // 3 ≤ T'.G.degree v }} (e : graftGraph T.G (Sum.inr v) ≃g graftGraph T'.G (Sum.inr v')) (he : e (Fin.last T.m) = Fin.last T'.m) :
      (ungraftVertexIso e he) ↑v = ↑v'

      The parent isomorphism of vertex grafts takes the selected vertex to its counterpart.

      source
      theorem BGW.StableTrees.Marchal.graftEdge_new_adj_iff {m : ℕ} (G : SimpleGraph (Fin m)) (a : ↑G.edgeSet) (x : Fin (m + 2)) :
      (graftGraph G (Sum.inl a)).Adj (Fin.last (m + 1)) x ↔ x = (Fin.last m).castSucc

      A new leaf in an edge graft has the midpoint as its unique neighbour.

      source
      theorem BGW.StableTrees.Marchal.graftEdgeIso_midpoint {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) :
      e (Fin.last T.m).castSucc = (Fin.last T'.m).castSucc

      A graft isomorphism preserving the new leaf also preserves the midpoint.

      source
      def BGW.StableTrees.Marchal.ungraftEdgeEquiv {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) :
      Fin T.m ≃ Fin T'.m

      Restriction of an edge-graft isomorphism to the original vertices.

      Equations
      Instances For
        source
        @[simp]
        theorem BGW.StableTrees.Marchal.ungraftEdgeEquiv_cast {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) (x : Fin T.m) :
        ((ungraftEdgeEquiv e he) x).castSucc.castSucc = e x.castSucc.castSucc
        source
        theorem BGW.StableTrees.Marchal.ungraftEdgeEquiv_mem {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) (x : Fin T.m) :
        (ungraftEdgeEquiv e he) x ∈ ↑a' ↔ x ∈ ↑a

        The endpoints of the removed edge are recovered as old neighbours of the midpoint.

        source
        theorem BGW.StableTrees.Marchal.ungraftEdgeEquiv_edge {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) :
        Sym2.map ⇑(ungraftEdgeEquiv e he) ↑a = ↑a'

        The parent equivalence recovers the edge that was subdivided.

        source
        def BGW.StableTrees.Marchal.ungraftEdgeIso {n : ℕ} {T T' : LTree n} {a : ↑T.G.edgeSet} {a' : ↑T'.G.edgeSet} (e : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl a')) (he : e (Fin.last (T.m + 1)) = Fin.last (T'.m + 1)) :
        T.G ≃g T'.G

        Removing the leaf and suppressing the midpoint recovers an edge-graft parent.

        Equations
        Instances For
          source
          theorem BGW.StableTrees.Marchal.graftVertex_ne_edge {n : ℕ} {T T' : LTree n} (v : { v : Fin T.m // 3 ≤ T.G.degree v }) (a : ↑T'.G.edgeSet) (e : graftGraph T.G (Sum.inr v) ≃g graftGraph T'.G (Sum.inl a)) (he : e (Fin.last T.m) = Fin.last (T'.m + 1)) :
          False

          A vertex graft cannot be isomorphic to an edge graft while preserving the new leaf.

          source
          theorem BGW.StableTrees.Marchal.graft_parent_eq {n : ℕ} {T T' : LTree n} (p : Position T.G) (q : Position T'.G) (h : ⟦graft T p⟧ = ⟦graft T' q⟧) :
          ⟦T⟧ = ⟦T'⟧

          Equality of graft states determines the parent state, for either kind of position.