Transporting ℤΔ along a tree isomorphism

An isomorphism of trees e : Δ₁ ≃ Δ₂ induces an isomorphism of their repetitions in height coordinates, (v, t) ↦ (e v, t + δ), where the constant δ matches the two-colourings ("Changing the orientation of the tree changes its repetition quiver only by the corresponding vertex shifts", periodic-mesh-calculations.tex). It commutes with translation and transports coverings.

theorem MultiplicativeBasisDeformations.OrientedTree.exists_par_shift {D₁ : Type v} {D₂ : Type v'} (T₁ : OrientedTree D₁) (T₂ : OrientedTree D₂) (e : D₁ ≃ D₂) (he : ∀ (a b : D₁), T₁.G.Adj a b ↔ T₂.G.Adj (e a) (e b)) (hc : T₁.G.Connected) (d₀ d : D₁) : T₂.par (e d) - T₁.par d = T₂.par (e d₀) - T₁.par d₀

The two-colourings differ by a constant on a connected tree.

def MultiplicativeBasisDeformations.OrientedTree.zMap {D₁ : Type v} {D₂ : Type v'} (T₁ : OrientedTree D₁) (T₂ : OrientedTree D₂) (e : D₁ ≃ D₂) (δ : ℤ) (hδ : ∀ (d : D₁), T₂.par (e d) = T₁.par d + ↑δ) (X : T₁.ZVert) : T₂.ZVert

The induced map on ℤΔ, for a matching shift δ.

def MultiplicativeBasisDeformations.OrientedTree.zMapInv {D₁ : Type v} {D₂ : Type v'} (T₁ : OrientedTree D₁) (T₂ : OrientedTree D₂) (e : D₁ ≃ D₂) (δ : ℤ) (hδ : ∀ (d : D₁), T₂.par (e d) = T₁.par d + ↑δ) (Y : T₂.ZVert) : T₁.ZVert

The induced map on ℤΔ, inverse direction.

def MultiplicativeBasisDeformations.OrientedTree.zEquiv {D₁ : Type v} {D₂ : Type v'} (T₁ : OrientedTree D₁) (T₂ : OrientedTree D₂) (e : D₁ ≃ D₂) (δ : ℤ) (hδ : ∀ (d : D₁), T₂.par (e d) = T₁.par d + ↑δ) : T₁.ZVert ≃ T₂.ZVert

The isomorphism of repetitions.

theorem MultiplicativeBasisDeformations.OrientedTree.nonempty_hom_zMap_iff {D₁ : Type v} {D₂ : Type v'} (T₁ : OrientedTree D₁) (T₂ : OrientedTree D₂) (e : D₁ ≃ D₂) (he : ∀ (a b : D₁), T₁.G.Adj a b ↔ T₂.G.Adj (e a) (e b)) (δ : ℤ) (hδ : ∀ (d : D₁), T₂.par (e d) = T₁.par d + ↑δ) (X Y : T₁.ZVert) : Nonempty (T₁.zMap T₂ e δ hδ X ⟶ T₁.zMap T₂ e δ hδ Y) ↔ Nonempty (X ⟶ Y)

theorem MultiplicativeBasisDeformations.isCovering_transport {W₁ : Type u₁} [Quiver W₁] {W₂ : Type u₂} [Quiver W₂] {V : Type u₃} [Quiver V] [∀ (x y : W₁), Subsingleton (x ⟶ y)] [∀ (x y : W₂), Subsingleton (x ⟶ y)] [∀ (x y : V), Subsingleton (x ⟶ y)] (f : W₁ ≃ W₂) (hf : ∀ (X Y : W₁), Nonempty (f X ⟶ f Y) ↔ Nonempty (X ⟶ Y)) (π : W₁ ⥤q V) (hπ : π.IsCovering) (π' : W₂ ⥤q V) (hobj : ∀ (Y : W₂), π'.obj Y = π.obj (f.symm Y)) : π'.IsCovering

Coverings transport along isomorphisms of quivers with at most one arrow between two vertices.