Lemma B.2 as a linear isomorphism

lem:integral-mesh-cokernels: "⊕_{m≥2} coker D_m(E₄) ≅ ⊕_{i∈I} (𝒪/(2))_{χ_i}. The summand indexed by i belongs to coker D_{d_i−1}, where d_i = 2s_i + 2 is its mesh path degree."

integralMeshCokernels proves that the rows of Proposition 6.1 generate each cokernel over 𝒪 = ℤ/4, that twice each is a derivative, and that a combination is a derivative exactly when all coefficients are even. Here this is assembled into an explicit isomorphism of 𝒪-modules in each degree: coker D_m(E₄) = F_{m+1}/(im D_m ∩ F_{m+1}) ≅ ⊕_{R} 𝒪/(2), the sum over the rows R of degree m + 1, sending the class of the row R to the generator of its summand (integralMeshCokernels_equiv). Summing over m ≥ 2 gives the displayed isomorphism, the row i lying in degree m = d_i − 1. The weight labels χ_i are integralMeshCokernels_weights.

def MultiplicativeBasisDeformations.ScalarMeshCategory.famDegR {k : Type u_1} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (n : ℕ) : Submodule k (MeshFamily c)

The mesh families of degree n.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.comp_mem_degreePartR {k : Type u_1} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {d e : ℕ} {x y z : V} {f : obj c x ⟶ obj c y} {g : obj c y ⟶ obj c z} (hf : f ∈ degreePart c d x y) (hg : g ∈ degreePart c e y z) : CategoryTheory.CategoryStruct.comp f g ∈ degreePart c (d + e) x z

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.imageD_le_famDegR {k : Type u_1} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : imageD c m ≤ famDegR c (m + 1)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.CokerDegR {k : Type u_1} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Type (max (max u_1 v) w)

The cokernel of D_m on the degree-(m+1) mesh families.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.row_mem_famDegR {k : Type u_1} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [DecidableEq V] {m : ℕ} (x : ↑Q.nonprojective) (p : Quiver.Path ↑(Q.tau x) ↑x) (hp : p.length = m + 1) : row c x p ∈ famDegR c (m + 1)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mem_span_two_iff (a : ZMod 4) : a ∈ Ideal.span {2} ↔ Z4.red a = 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.RowsDeg {V : Type v} [Quiver V] {Q : TranslationQuiver V} (S : RowSet Q) (m : ℕ) : Type (max 0 v w)

The rows of S of degree m + 1.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.integralMeshCokernels_equiv {V : Type v} [Quiver V] [Fintype V] [DecidableEq V] [(x y : V) → Fintype (x ⟶ y)] [(x y : V) → DecidableEq (x ⟶ y)] [(x : V) → Fintype ((y : V) × (y ⟶ x))] {Q : TranslationQuiver V} [DecidablePred fun (x : V) => x ∈ Q.nonprojective] [Fintype ↑Q.nonprojective] {c : MeshCoefficients (ZMod 2) Q} {u : MeshCoefficients (ZMod 4) Q} (hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), Z4.red ↑(u x y a) = ↑(c x y a)) (hQ : HasAtMostOneArrow V) [DecidablePred fun (x : V) => x ∈ Q.periodic] (hfin : ∀ (x y : V), FiniteDimensional (ZMod 2) (obj c x ⟶ obj c y)) (hbrick : BrickHypothesis c) : ∃ (S : RowSet Q), (∀ R ∈ S, ↑R.fst ∈ Q.periodic) ∧ (∀ R ∈ S, ∀ R' ∈ S, ↑R'.fst ∈ Q.component ↑R.fst → R = R') ∧ (∀ r ∈ Q.periodic, Residual c r ↔ ∃ R ∈ S, ↑R.fst ∈ Q.component r) ∧ (∀ R ∈ S, ∃ x ∈ Q.periodic, ↑R.fst ∈ Q.component x ∧ ∃ (R₀ : (y : ↑(TranslationQuiver.restrict ⋯).nonprojective) × Quiver.Path ↑((TranslationQuiver.restrict ⋯).tau y) ↑y), StarTrace.DEModel ⋯ R₀ ∧ R₀.snd.length = R.snd.length) ∧ ∀ (m : ℕ), 2 ≤ m → ∃ (x : Fintype (RowsDeg S m)) (e : CokerDegR u m ≃ₗ[ZMod 4] RowsDeg S m → ZMod 4 ⧸ Ideal.span {2}), ∀ (R : RowsDeg S m), e (Submodule.Quotient.mk ⟨row u (↑R).fst (↑R).snd, ⋯⟩) = Pi.single R (Submodule.Quotient.mk 1)

Lemma B.2 (lem:integral-mesh-cokernels) as an isomorphism: for E₄ (unit coefficients u over 𝒪 = ℤ/4 reducing to the coefficients of C⁽²⁾), there are rows S as in Proposition 6.1 (periodic, one per residual component, with the degrees d_i = 2s_i + 2 of the models) such that, in every degree m ≥ 2, coker D_m(E₄) ≅ ⊕_{R ∈ S, deg R = m + 1} 𝒪/(2), sending the class of each row R to the generator of its summand.