Lemma 12.6: mesh normal forms with the same support

deformation-refinements.tex (lem:same-support-forms). Let C(λ) be the mesh normal forms kQ/(𝔪^{N+1}, r_v − Σ_i λ_i (p_i)_v) of Proposition 12.2, with the residual paths p_i, each internal to its own periodic component. If λ_i = 0 exactly when λ'_i = 0, then C(λ) ≅ C(λ') by an object-preserving isomorphism.

The proof is the source's. Choose a_i ∈ kˣ; prescribe μ_a = a_i on the internal arrows of the ith residual component and the row scale a_i² on its vertices, scale one on the other periodic components. The mate map σ on arrows has chains and cycles; its cycles lie in the periodic part (σ² translates both endpoints), so the scale equations μ_{σa} μ_a = η_v (eq:global-mesh-scales) can be solved successively along every chain, with no closing condition (exists_chain_solution). The diagonal map sends r_v ↦ η_v r_v and p_i ↦ a_i^{d_i} p_i, so it changes λ_i to λ_i a_i^{d_i-2}; take a_i a root of λ'_i/λ_i.

Generalizations: any characteristic, any mesh coefficients (the same on both sides), any finite translation quiver; the residual rows are any rows of length at least three, internal to pairwise distinct periodic components.

Solving scale equations along chains

def MultiplicativeBasisDeformations.SameSupport.oiter {X : Type u_1} (σ : X → Option X) : ℕ → X → Option X

Iterates of a partial map.

theorem MultiplicativeBasisDeformations.SameSupport.oiter_add {X : Type u_1} (σ : X → Option X) (m n : ℕ) (a : X) : oiter σ (m + n) a = (oiter σ n a).bind (oiter σ m)

theorem MultiplicativeBasisDeformations.SameSupport.oiter_one {X : Type u_1} (σ : X → Option X) (a : X) : oiter σ 1 a = σ a

noncomputable def MultiplicativeBasisDeformations.SameSupport.back {X : Type u_1} (σ : X → Option X) [Fintype X] (b : X) : Finset X

The strict backward orbit of b.

theorem MultiplicativeBasisDeformations.SameSupport.back_eq {X : Type u_1} (σ : X → Option X) [Fintype X] [DecidableEq X] (hinj : ∀ (a b c : X), σ a = some c → σ b = some c → a = b) {a b : X} (hab : σ a = some b) (hcyc : ∀ (n : ℕ), 1 ≤ n → oiter σ n a ≠ some a) : back σ b = insert a (back σ a) ∧ a ∉ back σ a

def MultiplicativeBasisDeformations.SameSupport.chainF {X : Type u_1} {M : Type u_2} [CommGroup M] (pred : X → Option X) (e : X → M) : ℕ → X → M

The alternating products along a chain.

theorem MultiplicativeBasisDeformations.SameSupport.exists_chain_solution {X : Type u_1} (σ : X → Option X) [Fintype X] {M : Type u_2} [CommGroup M] (hinj : ∀ (a b c : X), σ a = some c → σ b = some c → a = b) (P : X → Prop) (hP : ∀ (a b : X), σ a = some b → (P a ↔ P b)) (hcyc : ∀ (a : X), ¬P a → ∀ (n : ℕ), 1 ≤ n → oiter σ n a ≠ some a) (e μ₀ : X → M) (h₀ : ∀ (a b : X), σ a = some b → P a → μ₀ b * μ₀ a = e a) : ∃ (μ : X → M), (∀ (a : X), P a → μ a = μ₀ a) ∧ ∀ (a b : X), σ a = some b → μ b * μ a = e a

Solving μ(σ a) μ(a) = e(a) along chains: on a finite set, a partial injective map σ without cycles outside a σ-closed set P allows any solution on P to be extended.

The mate map on arrows

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.SameSupport.Arr (V : Type) [Quiver V] : Type

The arrows of the quiver.

noncomputable def MultiplicativeBasisDeformations.SameSupport.mateMap {V : Type} [Quiver V] (Q : TranslationQuiver V) (a : Arr V) : Option (Arr V)

The mate map σ: a : u → v with v nonprojective goes to σ a : τ v → u.

theorem MultiplicativeBasisDeformations.SameSupport.mateMap_of_mem {V : Type} [Quiver V] (Q : TranslationQuiver V) {u v : V} (α : u ⟶ v) (h : v ∈ Q.nonprojective) : mateMap Q ⟨u, ⟨v, α⟩⟩ = some ⟨↑(Q.tau ⟨v, h⟩), ⟨u, (Q.mate ⟨v, h⟩ u) α⟩⟩

theorem MultiplicativeBasisDeformations.SameSupport.mateMap_eq_some {V : Type} [Quiver V] (Q : TranslationQuiver V) {a b : Arr V} (h : mateMap Q a = some b) : ∃ (h : a.snd.fst ∈ Q.nonprojective), b = ⟨↑(Q.tau ⟨a.snd.fst, h⟩), ⟨a.fst, (Q.mate ⟨a.snd.fst, h⟩ a.fst) a.snd.snd⟩⟩

theorem MultiplicativeBasisDeformations.SameSupport.mateMap_inj {V : Type} [Quiver V] (Q : TranslationQuiver V) (a b c : Arr V) (ha : mateMap Q a = some c) (hb : mateMap Q b = some c) : a = b

def MultiplicativeBasisDeformations.SameSupport.PerArr {V : Type} [Quiver V] (Q : TranslationQuiver V) (a : Arr V) : Prop

The arrows with both endpoints periodic.

theorem MultiplicativeBasisDeformations.SameSupport.mem_periodic_tau_iff {V : Type} [Quiver V] (Q : TranslationQuiver V) {v : V} (h : v ∈ Q.nonprojective) : ↑(Q.tau ⟨v, h⟩) ∈ Q.periodic ↔ v ∈ Q.periodic

theorem MultiplicativeBasisDeformations.SameSupport.perArr_iff {V : Type} [Quiver V] (Q : TranslationQuiver V) {a b : Arr V} (h : mateMap Q a = some b) : PerArr Q a ↔ PerArr Q b

theorem MultiplicativeBasisDeformations.SameSupport.tauChain_of_oiter {V : Type} [Quiver V] (Q : TranslationQuiver V) (m : ℕ) (a : Arr V) : oiter (mateMap Q) (2 * m) a ≠ none → Q.TauChain a.snd.fst m

σ² translates the target: if 2m iterates are defined, τ^j of the target is defined for j < m.

theorem MultiplicativeBasisDeformations.SameSupport.perArr_of_oiter {V : Type} [Quiver V] (Q : TranslationQuiver V) {a : Arr V} (ha : ∀ (m : ℕ), oiter (mateMap Q) m a ≠ none) : PerArr Q a

theorem MultiplicativeBasisDeformations.SameSupport.perArr_of_cycle {V : Type} [Quiver V] (Q : TranslationQuiver V) {a : Arr V} {n : ℕ} (hn : 1 ≤ n) (ha : oiter (mateMap Q) n a = some a) : PerArr Q a

The cycles of the mate map lie in the periodic part.

Scales on periodic components

noncomputable def MultiplicativeBasisDeformations.SameSupport.compScale {V : Type} [Quiver V] (Q : TranslationQuiver V) {M : Type u_1} [CommGroup M] {I : Type u_2} (v₀ : I → V) (s : I → M) (v : V) : M

The component scale: s_i on the ith component, one elsewhere.

theorem MultiplicativeBasisDeformations.SameSupport.compScale_of_mem {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {M : Type u_1} [CommGroup M] {I : Type u_2} {v₀ : I → V} (hper : ∀ (i : I), v₀ i ∈ Q.periodic) (hdisj : ∀ (i j : I), v₀ j ∈ Q.component (v₀ i) → i = j) (s : I → M) {v : V} {i : I} (hv : v ∈ Q.component (v₀ i)) : compScale Q v₀ s v = s i

theorem MultiplicativeBasisDeformations.SameSupport.mem_component_iff_of_arrow {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {u v : V} (α : u ⟶ v) (hu : u ∈ Q.periodic) (hv : v ∈ Q.periodic) (x : V) : u ∈ Q.component x ↔ v ∈ Q.component x

theorem MultiplicativeBasisDeformations.SameSupport.compScale_eq_of_arrow {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {M : Type u_1} [CommGroup M] {I : Type u_2} {v₀ : I → V} (hper : ∀ (i : I), v₀ i ∈ Q.periodic) (hdisj : ∀ (i j : I), v₀ j ∈ Q.component (v₀ i) → i = j) (s : I → M) {u v : V} (α : u ⟶ v) (hu : u ∈ Q.periodic) (hv : v ∈ Q.periodic) : compScale Q v₀ s u = compScale Q v₀ s v

theorem MultiplicativeBasisDeformations.SameSupport.exists_scales {V : Type} [Quiver V] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] {Q : TranslationQuiver V} {M : Type u_1} [CommGroup M] {I : Type u_2} {v₀ : I → V} (hper : ∀ (i : I), v₀ i ∈ Q.periodic) (hdisj : ∀ (i j : I), v₀ j ∈ Q.component (v₀ i) → i = j) (s : I → M) : ∃ (μ : Arr V → M), (∀ (x : ↑Q.nonprojective) (y : V) (α : y ⟶ ↑x), μ ⟨↑(Q.tau x), ⟨y, (Q.mate x y) α⟩⟩ * μ ⟨y, ⟨↑x, α⟩⟩ = compScale Q v₀ s ↑x ^ 2) ∧ ∀ (i : I) {u v : V} (α : u ⟶ v), u ∈ Q.component (v₀ i) → v ∈ Q.component (v₀ i) → μ ⟨u, ⟨v, α⟩⟩ = s i

The global mesh scales (eq:global-mesh-scales, with all c_{v,a} = 1): arrow scales μ with μ_{σa} μ_a = η_v, where η_v = s_i² on the ith component and η_v = 1 on the other periodic vertices, and μ_a = s_i on the internal arrows of the ith component.

Weights of internal paths

def MultiplicativeBasisDeformations.SameSupport.PathIn {V : Type} [Quiver V] (C : Set V) {x y : V} : Quiver.Path x y → Prop

A path all of whose arrows have both endpoints in C.

theorem MultiplicativeBasisDeformations.SameSupport.pathWt_of_pathIn {V : Type} [Quiver V] {k : Type u_1} [CommRing k] (μ : {x y : V} → (x ⟶ y) → kˣ) (C : Set V) (t : kˣ) (hμ : ∀ {u v : V} (α : u ⟶ v), u ∈ C → v ∈ C → μ α = t) {x : V} (hx : x ∈ C) {y : V} (p : Quiver.Path x y) : PathIn C p → y ∈ C → pathWt (fun {x y : V} => μ) p = t ^ p.length

The last vertex of a nonempty path in C lies in C.

theorem MultiplicativeBasisDeformations.SameSupport.pathWt_inv {V : Type} [Quiver V] {k : Type u_1} [CommRing k] (μ : {x y : V} → (x ⟶ y) → kˣ) {x y : V} (p : Quiver.Path x y) : pathWt (fun {x y : V} (α : x ⟶ y) => (μ α)⁻¹) p = (pathWt (fun {x y : V} => μ) p)⁻¹

theorem MultiplicativeBasisDeformations.SameSupport.gaugeMap_inv {V : Type} [Quiver V] {k : Type u_1} [CommRing k] (μ : {x y : V} → (x ⟶ y) → kˣ) (x y : V) (g : LinearPaths.obj x ⟶ LinearPaths.obj y) : (gaugeMap (fun {x y : V} (α : x ⟶ y) => (μ α)⁻¹) x y) ((gaugeMap (fun {x y : V} => μ) x y) g) = g

Diagonal maps of the perturbed presentations

noncomputable def MultiplicativeBasisDeformations.SameSupport.tpert {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {I : Type u_2} [Fintype I] (tup : I → (x : ↑Q.nonprojective) → FlatPert.Hm k ↑(Q.tau x) ↑x) (lam : I → k) (x : V) (t : (FlatPert.meshPres c).T x) : FlatPert.Hm k ((FlatPert.meshPres c).src x t) x

The perturbation Σ_i λ_i (p_i)_v of the mesh relations by tuples.

theorem MultiplicativeBasisDeformations.SameSupport.tpert_mem {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {I : Type u_2} [Fintype I] (tup : I → (x : ↑Q.nonprojective) → FlatPert.Hm k ↑(Q.tau x) ↑x) (htup : ∀ (i : I) (x : ↑Q.nonprojective), tup i x ∈ FlatPert.geSpan k 3 ↑(Q.tau x) ↑x) (lam : I → k) (x : V) (t : (FlatPert.meshPres c).T x) : tpert c tup lam x t ∈ FlatPert.geSpan k ((FlatPert.meshPres c).deg x t + 1) ((FlatPert.meshPres c).src x t) x

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.SameSupport.idealT {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {I : Type u_2} [Fintype I] (tup : I → (x : ↑Q.nonprojective) → FlatPert.Hm k ↑(Q.tau x) ↑x) (htup : ∀ (i : I) (x : ↑Q.nonprojective), tup i x ∈ FlatPert.geSpan k 3 ↑(Q.tau x) ↑x) (lam : I → k) (N : ℕ) : FlatPert.IdealFam k V

The ideal (𝔪^{N+1}, r_v − Σ_i λ_i (p_i)_v) of C(λ).

theorem MultiplicativeBasisDeformations.SameSupport.gauge_le {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) {I : Type u_2} [Fintype I] (tup : I → (x : ↑Q.nonprojective) → FlatPert.Hm k ↑(Q.tau x) ↑x) (htup : ∀ (i : I) (x : ↑Q.nonprojective), tup i x ∈ FlatPert.geSpan k 3 ↑(Q.tau x) ↑x) (μ : {x y : V} → (x ⟶ y) → kˣ) (E : V → kˣ) (κ : I → kˣ) (hscale : ∀ (x : ↑Q.nonprojective) (y : V) (α : y ⟶ ↑x), μ ((Q.mate x y) α) * μ α = E ↑x) (hg : ∀ (i : I) (x : ↑Q.nonprojective), (gaugeMap (fun {x y : V} => μ) ↑(Q.tau x) ↑x) (tup i x) = ↑(E ↑x * κ i) • tup i x) (lam : I → k) (N : ℕ) (w y : V) : (idealT c tup htup lam N).I w y ≤ Submodule.comap (gaugeMap (fun {x y : V} => μ) w y) ((idealT c tup htup (fun (i : I) => lam i * ↑(κ i)) N).I w y)

A diagonal map with μ_{σa} μ_a = η_v and p_i ↦ η_v κ_i p_i maps the ideal of C(λ) into that of C(λκ).

Lemma 12.6

noncomputable def MultiplicativeBasisDeformations.SameSupport.rowTup {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] {Q : TranslationQuiver V} {I : Type u_2} (v₀ : I → ↑Q.nonprojective) (p : (i : I) → Quiver.Path ↑(Q.tau (v₀ i)) ↑(v₀ i)) (i : I) (x : ↑Q.nonprojective) : FlatPert.Hm k ↑(Q.tau x) ↑x

The tuple of a row: the path p_i at the row v_i, zero at all other rows.

theorem MultiplicativeBasisDeformations.SameSupport.rowTup_mem {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} {I : Type u_2} (v₀ : I → ↑Q.nonprojective) (p : (i : I) → Quiver.Path ↑(Q.tau (v₀ i)) ↑(v₀ i)) (hlen : ∀ (i : I), 3 ≤ (p i).length) (i : I) (x : ↑Q.nonprojective) : rowTup v₀ p i x ∈ FlatPert.geSpan k 3 ↑(Q.tau x) ↑x

theorem MultiplicativeBasisDeformations.SameSupport.tau_mem_component {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} {v : ↑Q.nonprojective} (hv : ↑v ∈ Q.periodic) : ↑(Q.tau v) ∈ Q.component ↑v

theorem MultiplicativeBasisDeformations.SameSupport.gauge_rowTup {k : Type u_1} [CommRing k] {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} {I : Type u_2} (v₀ : I → ↑Q.nonprojective) (p : (i : I) → Quiver.Path ↑(Q.tau (v₀ i)) ↑(v₀ i)) (hper : ∀ (i : I), ↑(v₀ i) ∈ Q.periodic) (hint : ∀ (i : I), PathIn (Q.component ↑(v₀ i)) (p i)) (hlen : ∀ (i : I), 3 ≤ (p i).length) (μ : {x y : V} → (x ⟶ y) → kˣ) (E : V → kˣ) (κ t : I → kˣ) (hμ : ∀ (i : I) {u v : V} (α : u ⟶ v), u ∈ Q.component ↑(v₀ i) → v ∈ Q.component ↑(v₀ i) → μ α = t i) (hE : ∀ (i : I), E ↑(v₀ i) = t i ^ 2) (hκ : ∀ (i : I), κ i = t i ^ ((p i).length - 2)) (i : I) (x : ↑Q.nonprojective) : (gaugeMap (fun {x y : V} => μ) ↑(Q.tau x) ↑x) (rowTup v₀ p i x) = ↑(E ↑x * κ i) • rowTup v₀ p i x

theorem MultiplicativeBasisDeformations.SameSupport.sameSupport {V : Type} [Quiver V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} {I : Type u_2} (v₀ : I → ↑Q.nonprojective) (p : (i : I) → Quiver.Path ↑(Q.tau (v₀ i)) ↑(v₀ i)) [Fintype I] {k : Type u_3} [Field k] [IsAlgClosed k] [Fintype V] [(x y : V) → Fintype (x ⟶ y)] (c : MeshCoefficients k Q) (hper : ∀ (i : I), ↑(v₀ i) ∈ Q.periodic) (hdisj : ∀ (i j : I), ↑(v₀ j) ∈ Q.component ↑(v₀ i) → i = j) (hint : ∀ (i : I), PathIn (Q.component ↑(v₀ i)) (p i)) (hlen : ∀ (i : I), 3 ≤ (p i).length) (N : ℕ) (lam lam' : I → k) (hsupp : ∀ (i : I), lam i = 0 ↔ lam' i = 0) : ∃ (μ : {x y : V} → (x ⟶ y) → kˣ), (∀ (x y : V) (g : FlatPert.Hm k x y), (gaugeMap (fun {x y : V} (α : x ⟶ y) => (μ α)⁻¹) x y) ((gaugeMap (fun {x y : V} => μ) x y) g) = g) ∧ (∀ (x y : V) (g : FlatPert.Hm k x y), (gaugeMap (fun {x y : V} => μ) x y) ((gaugeMap (fun {x y : V} (α : x ⟶ y) => (μ α)⁻¹) x y) g) = g) ∧ ∀ (x y : V), Submodule.map (gaugeMap (fun {x y : V} => μ) x y) ((idealT c (rowTup v₀ p) ⋯ lam N).I x y) = (idealT c (rowTup v₀ p) ⋯ lam' N).I x y

Lemma 12.6 (lem:same-support-forms): let C(λ) = kQ/(𝔪^{N+1}, r_v − Σ_i λ_i (p_i)_v) with rows p_i : τ v_i → v_i of length at least three, internal to pairwise distinct periodic components. If λ_i = 0 exactly when λ'_i = 0, a diagonal automorphism a ↦ μ_a a of kQ (object-preserving, with inverse a ↦ μ_a⁻¹ a) maps the ideal of C(λ) onto that of C(λ'), so C(λ) ≅ C(λ').