The prime-field model C⁽²⁾ of k(Γ_A) (Section 10)

integral-deformations.tex: "The all-one meshes of Section 7 define a graded category C⁽²⁾ with k ⊗_{𝔽₂} C⁽²⁾ = C. […] Evaluation identifies C⁽²⁾ with their full Hom category, since it does so after the faithful field extension to k. The same extension commutes with graded Ext […]. Lemma 6.3 therefore gives Ext^n_{A⁽²⁾}(M_i⁽²⁾, M_j⁽²⁾)_d = 0 (n ≥ 1, d ≥ 0)."

For char k = 2: the all-one scalar mesh category C⁽²⁾ = C(Γ_A, 1) over 𝔽₂ (prime2), the gauge of Lemma 4.4 (arGauge), the form functor to k(Γ_A) with equal Hom dimensions, and the mesh data of C⁽²⁾ (primeMeshData) obtained by descent of the exact meshes of k(Γ_A) (arMeshExact, Proposition 2.6), with injective labels (primeInjData) and degree-one arrows. Lemma 6.3 then holds for C⁽²⁾ (primeExtVanish): the same proof, for the descended mesh data, replaces the base change of Ext.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degOne_meshDataOf {k : Type w} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) (hE : MeshExact c) : MeshWalk.DegOne (meshDataOf hfin hE)

The arrows and scaled mates of meshDataOf have degree one.

theorem MultiplicativeBasisDeformations.IndSkeleton.arMeshExact {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : ScalarMeshCategory.MeshExact (S.arCoefficients b)

The meshes of k(Γ_A) are exact (Proposition 2.6(1)(2)).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.oneC {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (K : Type) [Field K] : MeshCoefficients K S.arTranslationQuiver

The all-one coefficients.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.oneK {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : MeshCoefficients k S.arTranslationQuiver

The all-one coefficients over k.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_arGauge {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : ∃ (μ : {x y : S.ARVertex} → (x ⟶ y) → kˣ) (η : ↑S.arTranslationQuiver.nonprojective → kˣ), ∀ (x : ↑S.arTranslationQuiver.nonprojective) (y : S.ARVertex) (a : y ⟶ ↑x), S.arCoefficients b x y a = η x * S.oneK x y a * μ ((S.arTranslationQuiver.mate x y) a) * μ a

The gauge of Lemma 4.4: c_{x,a} = η_x μ_{σa} μ_a.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arMu {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {x y : S.ARVertex} : (x ⟶ y) → kˣ

A chosen gauge.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arEta {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : ↑S.arTranslationQuiver.nonprojective → kˣ

A chosen gauge.

theorem MultiplicativeBasisDeformations.IndSkeleton.arGauge {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : ↑S.arTranslationQuiver.nonprojective) (y : S.ARVertex) (a : y ⟶ ↑x) : S.arCoefficients b x y a = S.arEta b x * S.oneK x y a * S.arMu b ((S.arTranslationQuiver.mate x y) a) * S.arMu b a

theorem MultiplicativeBasisDeformations.IndSkeleton.hredOne {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) [CharP k 2] (x : ↑S.arTranslationQuiver.nonprojective) (y : S.ARVertex) (a : y ⟶ ↑x) : (algebraMap (ZMod 2) k) ↑(S.oneC (ZMod 2) x y a) = ↑(S.oneK x y a)

theorem MultiplicativeBasisDeformations.IndSkeleton.prime_finrank {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] (x y : S.ARVertex) : FiniteDimensional (ZMod 2) (ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) ∧ Module.finrank (ZMod 2) (ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y) = Module.finrank k (S.meshObj b x ⟶ S.meshObj b y)

Equal dimensions of C⁽²⁾ and k(Γ_A).

theorem MultiplicativeBasisDeformations.IndSkeleton.prime_fd {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] (x y : S.ARVertex) : FiniteDimensional (ZMod 2) (ScalarMeshCategory.obj (S.oneC (ZMod 2)) x ⟶ ScalarMeshCategory.obj (S.oneC (ZMod 2)) y)

theorem MultiplicativeBasisDeformations.IndSkeleton.primeMeshExact {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] : ScalarMeshCategory.MeshExact (S.oneC (ZMod 2))

The exact meshes of C⁽²⁾.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.primeMeshData {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] : CatAlg.MeshData (fun (x : S.ARVertex) => ScalarMeshCategory.obj (S.oneC (ZMod 2)) x) (ScalarMeshCategory.localFamily (S.oneC (ZMod 2)) ⋯)

The mesh data of C⁽²⁾.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.primeInjData {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] : (S.primeMeshData b).InjData

The injective labels of C⁽²⁾, those of k(Γ_A).

theorem MultiplicativeBasisDeformations.IndSkeleton.primeDegOne {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] : MeshWalk.DegOne (S.primeMeshData b)