The spanning rows of C⁽²⁾ (Lemma B.2 over 𝔽₂) #
lem:integral-mesh-cokernels is applied in Section 10 to the prime-field model C⁽²⁾. The
rows of Proposition 6.1 span the derivative cokernels of k(Γ_A) (residual_cokerSpan); the
spanning property passes to the all-one presentation over k by the gauge of Lemma 4.4
(cokerSpan_gauge), and from there to 𝔽₂ by a coefficient retraction k → 𝔽₂
(cokerSpan_descend): applying the retraction to a relation
row = ∑ αᵢ rowᵢ + D f over k gives row = ∑ θ(αᵢ) rowᵢ + D(θ f) over 𝔽₂.
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.retE_degreePart
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients K Q}
{c : MeshCoefficients k Q}
(hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a))
(θ : k →ₗ[K] K)
{X Y : V}
{n : ℕ}
{φ : obj c X ⟶ obj c Y}
(hφ : φ ∈ degreePart c n X Y)
:
retE u θ φ ∈ degreePart u n X Y
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.retE_meshDerivative
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients K Q}
{c : MeshCoefficients k Q}
(hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a))
(θ : k →ₗ[K] K)
[DecidableEq V]
(f : ArrowFamily c)
(x : ↑Q.nonprojective)
:
retE u θ (meshDerivative c f x) = meshDerivative u (fun (a : (x : V) × (y : V) × (x ⟶ y)) => retE u θ (f a)) x
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.retE_row
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients K Q}
{c : MeshCoefficients k Q}
(hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a))
(θ : k →ₗ[K] K)
[DecidableEq V]
(h1 : θ 1 = 1)
(t : k)
(x x' : ↑Q.nonprojective)
(w : Quiver.Path ↑(Q.tau x) ↑x)
:
theorem
MultiplicativeBasisDeformations.ScalarMeshCategory.cokerSpan_descend
{K : Type}
[Field K]
{k : Type u}
[Field k]
[Algebra K k]
{V : Type v}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{u : MeshCoefficients K Q}
{c : MeshCoefficients k Q}
(hred : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), (algebraMap K k) ↑(u x y a) = ↑(c x y a))
(θ : k →ₗ[K] K)
[DecidableEq V]
[Fintype ↑Q.nonprojective]
(h1 : θ 1 = 1)
{S : RowSet Q}
(hS : CokerSpan c S)
:
CokerSpan u S
Spanning rows descend along a field extension.
theorem
MultiplicativeBasisDeformations.IndSkeleton.prime_cokerSpan
{k A : Type u}
[Field k]
[IsAlgClosed k]
[CharP k 2]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
:
∃ (R : ScalarMeshCategory.RowSet S.arTranslationQuiver),
ScalarMeshCategory.CokerSpan (S.oneC (ZMod 2)) R ∧ ScalarMeshCategory.TwoRows S.arTranslationQuiver R
The rows of Proposition 6.1 span the derivative cokernels of C⁽²⁾, and are killed by
two over every coefficient ring.