Lemma 12.6 for the residual paths of Proposition 6.1

lem:same-support-forms: "Let C(λ) and C(λ') be the mesh normal forms of Proposition 12.2, using the same normalized meshes and the residual paths of Proposition 6.1. If λ_i = 0 exactly when λ'_i = 0, there is an object-preserving isomorphism C(λ) ≅ C(λ')."

The rows of Proposition 6.1 (residualCorrectionSpaces) satisfy the hypotheses of the generic sameSupport: they lie at periodic vertices of pairwise distinct components, have length at least four (degree 2s + 2), and stay inside their component, since a row through a nonperiodic vertex has zero class (row_mem_imageD_of_not_periodic) while the classes of the rows are nonzero (pathIn_residual). The statement is sameSupport_residual.

theorem MultiplicativeBasisDeformations.SameSupport.pathIn_of_vertices {V : Type} [Quiver V] {C : Set V} {x y : V} (p : Quiver.Path x y) : (∀ v ∈ p.vertices, v ∈ C) → PathIn C p

theorem MultiplicativeBasisDeformations.SameSupport.sameSupport_residual {V : Type} [Quiver V] {k : Type} [Field k] [IsAlgClosed k] [Fintype V] [DecidableEq V] [(x y : V) → DecidableEq (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} (c : MeshCoefficients k Q) (hQ : HasAtMostOneArrow V) (hchar : 2 = 0) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) (hbrick : ScalarMeshCategory.BrickHypothesis c) : ∃ (n : ℕ) (v₀ : Fin n → ↑Q.nonprojective) (p : (i : Fin n) → Quiver.Path ↑(Q.tau (v₀ i)) ↑(v₀ i)), (Function.Injective fun (i : Fin n) => ⟨v₀ i, p i⟩) ∧ (∀ (i : Fin n), ↑(v₀ i) ∈ Q.periodic) ∧ (∀ (i j : Fin n), ↑(v₀ j) ∈ Q.component ↑(v₀ i) → i = j) ∧ ScalarMeshCategory.CokerSpan c (Set.range fun (i : Fin n) => ⟨v₀ i, p i⟩) ∧ (∀ (i : Fin n), ScalarMeshCategory.row c (v₀ i) (p i) ∉ ScalarMeshCategory.imageD c ((p i).length - 1)) ∧ ∃ (_ : ∀ (i : Fin n), PathIn (Q.component ↑(v₀ i)) (p i)) (hlen : ∀ (i : Fin n), 3 ≤ (p i).length), ∀ (N : ℕ) (lam lam' : Fin n → k), (∀ (i : Fin n), 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) for the residual paths of Proposition 6.1: in characteristic two, for a finite-dimensional scalar mesh category with the brick hypothesis, there are rows p_i : τ v_i → v_i as in Proposition 6.1 (at periodic vertices of pairwise distinct components, with nonzero classes spanning the cokernels) such that for every N and parameters λ, λ' with the same zeros, a diagonal automorphism of kQ maps the ideal (𝔪^{N+1}, r_v − Σ_i λ_i (p_i)_v) of C(λ) onto that of C(λ').