Multiplicative bases

MultiplicativeBasisDeformations.Foundations.IntegralCoker

Lemma B.2: the derivative cokernels over โ„ค/4 are killed by two #

lem:integral-mesh-cokernels (characteristic-two-mesh-calculations.tex): "Each retained derivative cokernel is thus killed by two. โ€ฆ All other degree and weight components vanish by their zero reduction."

With ๐’ช = โ„ค/4 and unit coefficients ลฉ reducing to the coefficients c of a scalar mesh category over ๐”ฝโ‚‚: given rows spanning the cokernels over ๐”ฝโ‚‚ (CokerSpan; for Cโฝยฒโพ these are IndSkeleton.prime_cokerSpan) which are killed by two over every coefficient ring (TwoRows, from the trace calculations), and since reduction is right exact (ReductionMesh), every family of degree m + 1 โ‰ฅ 3 is, up to 2ยท(families), an ๐’ช-combination of these rows plus a derivative, so twice it is a derivative (two_smul_mem_imageD).

source
def MultiplicativeBasisDeformations.ScalarMeshCategory.half (a : ZMod 4) :
ZMod 4

Division by two on 2๐’ช.

Instances For
    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.half_zero :
    half 0 = 0
    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.two_mul_half {a : ZMod 4} (h : Z4.red a = 0) :
    2 * half a = a
    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.eq_two_smul_of_redP {V : Type v} [Quiver V] {x y : V} {ฮฆ : LinearPaths.obj x โŸถ LinearPaths.obj y} (h : (LinearPaths.redP Z4.red) ฮฆ = 0) :
    โˆƒ (H : LinearPaths.obj x โŸถ LinearPaths.obj y), ฮฆ = 2 โ€ข H

    The kernel of the reduction of path combinations is 2ยท(path combinations).

    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.eq_two_smul_of_redE {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)) {X Y : V} {ฯ† : obj u X โŸถ obj u Y} (h : redE Z4.red u c ฯ† = 0) :
    โˆƒ (ฯˆ : obj u X โŸถ obj u Y), ฯ† = 2 โ€ข ฯˆ
    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mk_mem_rowSpan {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} {S : RowSet Q} (hS : CokerSpan c S) {m : โ„•} (hm : 2 โ‰ค m) {g : MeshFamily c} (hg : โˆ€ (x : โ†‘Q.nonprojective), g x โˆˆ degreePart c (m + 1) โ†‘(Q.tau x) โ†‘x) :
    Submodule.Quotient.mk g โˆˆ rowSpan c m S

    A family of degree m + 1 has class in the span of rows spanning the cokernels.

    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.two_smul_mem_imageD {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)) {S : RowSet Q} (hspan : CokerSpan c S) (htwo : TwoRows Q S) {m : โ„•} (hm : 2 โ‰ค m) {g : MeshFamily u} (hg : โˆ€ (x : โ†‘Q.nonprojective), g x โˆˆ degreePart u (m + 1) โ†‘(Q.tau x) โ†‘x) :
    2 โ€ข g โˆˆ imageD u m

    Lemma B.2 (lem:integral-mesh-cokernels): over โ„ค/4, twice every family of mesh corrections of degree m + 1 โ‰ฅ 3 is a derivative.