Changing the root of a star model

periodic-mesh-calculations.tex: "for odd A, root it at its middle vertex". A covering π : ℤΔ → Q and its deck data transport along an isomorphism e : Δ ≃ Δ' of star models (any graph isomorphism; the heights shift by δ to match the two-colourings).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ReRoot.zE {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) : (starTree L).ZVert ≃ (starTree L').ZVert

The isomorphism of repetitions.

theorem MultiplicativeBasisDeformations.ReRoot.zE_hom {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (X Y : (starTree L).ZVert) : Nonempty ((zE e δ hδ) X ⟶ (zE e δ hδ) Y) ↔ Nonempty (X ⟶ Y)

theorem MultiplicativeBasisDeformations.ReRoot.zE_ztau {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (X : (starTree L).ZVert) : (zE e δ hδ) ((starTree L).ztau X) = (starTree L').ztau ((zE e δ hδ) X)

theorem MultiplicativeBasisDeformations.ReRoot.nonempty_map {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) {Y Y' : (starTree L').ZVert} (a : Y ⟶ Y') : Nonempty (π.obj ((zE e δ hδ).symm Y) ⟶ π.obj ((zE e δ hδ).symm Y'))

noncomputable def MultiplicativeBasisDeformations.ReRoot.π' {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) : (starTree L').ZVert ⥤q V

The transported covering.

theorem MultiplicativeBasisDeformations.ReRoot.π'_obj {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (Y : (starTree L').ZVert) : (π' e he δ hδ π).obj Y = π.obj ((zE e δ hδ).symm Y)

theorem MultiplicativeBasisDeformations.ReRoot.π'_isCovering {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hπ : π.IsCovering) : (π' e he δ hδ π).IsCovering

theorem MultiplicativeBasisDeformations.ReRoot.π'_tau {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : (starTree L).ZVert ⥤q V) (hτ : ∀ (Y : (starTree L).ZVert), π.obj ((starTree L).ztau Y) = hQ.tauE (π.obj Y)) (Y : (starTree L').ZVert) : (π' e he δ hδ π).obj ((starTree L').ztau Y) = hQ.tauE ((π' e he δ hδ π).obj Y)

theorem MultiplicativeBasisDeformations.ReRoot.π'_surj {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (hsurj : ∀ (x : V), ∃ (X : (starTree L).ZVert), π.obj X = x) (x : V) : ∃ (Y : (starTree L').ZVert), (π' e he δ hδ π).obj Y = x

Transport of the deck data

def MultiplicativeBasisDeformations.ReRoot.ρ' {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (ρ : StarV L ≃ StarV L) : StarV L' ≃ StarV L'

The transported deck automorphism e ρ e⁻¹.

theorem MultiplicativeBasisDeformations.ReRoot.ρ'_adj {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (a b : StarV L') : (starTree L').G.Adj ((ρ' e ρ) a) ((ρ' e ρ) b) ↔ (starTree L').G.Adj a b

theorem MultiplicativeBasisDeformations.ReRoot.ρ'_par {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (ρ : StarV L ≃ StarV L) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (v : StarV L') : (starTree L').par ((ρ' e ρ) v) = (starTree L').par v + ↑↑c0

theorem MultiplicativeBasisDeformations.ReRoot.zE_zAct {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (X : (starTree L).ZVert) : (zE e δ hδ) (((starTree L).zAct ρ hρ (↑c0) hρp).obj X) = ((starTree L').zAct (ρ' e ρ) ⋯ ↑c0 ⋯).obj ((zE e δ hδ) X)

theorem MultiplicativeBasisDeformations.ReRoot.zE_symm_zAct {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (Y : (starTree L').ZVert) : (zE e δ hδ).symm (((starTree L').zAct (ρ' e ρ) ⋯ ↑c0 ⋯).obj Y) = ((starTree L).zAct ρ hρ (↑c0) hρp).obj ((zE e δ hδ).symm Y)

theorem MultiplicativeBasisDeformations.ReRoot.π'_deck {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hdeck : ∀ (Z : (starTree L).ZVert), π.obj (((starTree L).zAct ρ hρ (↑c0) hρp).obj Z) = π.obj Z) (Y : (starTree L').ZVert) : (π' e he δ hδ π).obj (((starTree L').zAct (ρ' e ρ) ⋯ ↑c0 ⋯).obj Y) = (π' e he δ hδ π).obj Y

theorem MultiplicativeBasisDeformations.ReRoot.zE_iter {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (n : ℕ) (X : (starTree L).ZVert) : (zE e δ hδ) ((StarGauge.gZ ρ hρ c0 hρp)^[n] X) = (StarGauge.gZ (ρ' e ρ) ⋯ c0 ⋯)^[n] ((zE e δ hδ) X)

theorem MultiplicativeBasisDeformations.ReRoot.π'_fib {t t' : ℕ} {L : Fin t → ℕ} {L' : Fin t' → ℕ} (e : StarV L ≃ StarV L') (he : ∀ (a b : StarV L), (starTree L).G.Adj a b ↔ (starTree L').G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : StarV L), (starTree L').par (e d) = (starTree L).par d + ↑δ) {V : Type u} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] (π : (starTree L).ZVert ⥤q V) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), (starTree L).G.Adj (ρ a) (ρ b) ↔ (starTree L).G.Adj a b) (c0 : ℕ) (hρp : ∀ (v : StarV L), (starTree L).par (ρ v) = (starTree L).par v + ↑↑c0) (hfib : ∀ (X Y : (starTree L).ZVert), π.obj X = π.obj Y → ∃ (n : ℕ), Y = (StarGauge.gZ ρ hρ c0 hρp)^[n] X ∨ X = (StarGauge.gZ ρ hρ c0 hρp)^[n] Y) (X Y : (starTree L').ZVert) (h : (π' e he δ hδ π).obj X = (π' e he δ hδ π).obj Y) : ∃ (n : ℕ), Y = (StarGauge.gZ (ρ' e ρ) ⋯ c0 ⋯)^[n] X ∨ X = (StarGauge.gZ (ρ' e ρ) ⋯ c0 ⋯)^[n] Y

An odd path rooted at its middle vertex

def MultiplicativeBasisDeformations.ReRoot.pos {L' : Fin 2 → ℕ} : StarV L' → ℤ

The signed position on a two-armed star: arm 0 positive, arm 1 negative.

theorem MultiplicativeBasisDeformations.ReRoot.adj_two {L' : Fin 2 → ℕ} (a b : StarV L') : starAdj a b ↔ pos b = pos a + 1 ∨ pos a = pos b + 1

theorem MultiplicativeBasisDeformations.ReRoot.pos_injective {L' : Fin 2 → ℕ} : Function.Injective pos

theorem MultiplicativeBasisDeformations.ReRoot.adj_one {L : Fin 1 → ℕ} (a b : StarV L) : starAdj a b ↔ starDepth b = starDepth a + 1 ∨ starDepth a = starDepth b + 1

def MultiplicativeBasisDeformations.ReRoot.Lmid (h : ℕ) : Fin 2 → ℕ

The two arms of the re-rooted path.

def MultiplicativeBasisDeformations.ReRoot.ofPos (h : ℕ) (p : ℤ) (hp : -↑h ≤ p ∧ p ≤ ↑h) : StarV (Lmid h)

The vertex of the re-rooted path at a signed position.

theorem MultiplicativeBasisDeformations.ReRoot.pos_ofPos (h : ℕ) (p : ℤ) (hp : -↑h ≤ p ∧ p ≤ ↑h) : pos (ofPos h p hp) = p

theorem MultiplicativeBasisDeformations.ReRoot.pos_bound (h : ℕ) (hh : 1 ≤ h) (v : StarV (Lmid h)) : -↑h ≤ pos v ∧ pos v ≤ ↑h

def MultiplicativeBasisDeformations.ReRoot.midEquiv (h : ℕ) (hh : 1 ≤ h) (L : Fin 1 → ℕ) (hL : L 0 = 2 * h - 1) : StarV L ≃ StarV (Lmid h)

The re-rooting isomorphism: depth d goes to position d - h.

theorem MultiplicativeBasisDeformations.ReRoot.pos_midEquiv (h : ℕ) (hh : 1 ≤ h) (L : Fin 1 → ℕ) (hL : L 0 = 2 * h - 1) (v : StarV L) : pos ((midEquiv h hh L hL) v) = ↑(starDepth v) - ↑h

theorem MultiplicativeBasisDeformations.ReRoot.midEquiv_adj (h : ℕ) (hh : 1 ≤ h) (L : Fin 1 → ℕ) (hL : L 0 = 2 * h - 1) (a b : StarV L) : (starTree L).G.Adj a b ↔ (starTree (Lmid h)).G.Adj ((midEquiv h hh L hL) a) ((midEquiv h hh L hL) b)

theorem MultiplicativeBasisDeformations.ReRoot.depth_eq_abs_pos (h : ℕ) (w : StarV (Lmid h)) : ↑(starDepth w) = |pos w|

theorem MultiplicativeBasisDeformations.ReRoot.cast_abs (a : ℤ) : ↑|a| = ↑a

theorem MultiplicativeBasisDeformations.ReRoot.midEquiv_par (h : ℕ) (hh : 1 ≤ h) (L : Fin 1 → ℕ) (hL : L 0 = 2 * h - 1) (d : StarV L) : (starTree (Lmid h)).par ((midEquiv h hh L hL) d) = (starTree L).par d + ↑↑h