Proposition 10.3 in coefficients

integral-deformations.tex (prop:integral-bockstein): "In Lemma 10.2, the map j is zero by (mod-four-mesh-annihilator). Injectivity of Ψ₄ gives i_* = 0."

In coefficients (RaySys.Sys.IStar): for a cochain z of character χ over 𝒪 = ℤ/4 with d₂z ∈ 2C³, the cochain 2z is d₁ of a cochain. Its reduction z̄ is a cocycle over 𝔽₂; the cocycle Φ₂(2z) = 2Φ₂(z) of A⁽⁴⁾ = 𝒪P is twice the cocycle Φ₂(z̄) of A⁽²⁾ ≅ 𝔽₂P, a coboundary by MeshWalk.exists_hcobdry_twice, and the coefficients of a coboundary are d₁ of coefficients (coef_of_hcobdry). For A this runs in the prime-field model C⁽²⁾ with Θ₂ : 𝔽₂P ≅ A⁽²⁾ (IndSkeleton.tab₂) and the rows of IndSkeleton.prime_cokerSpan. This proves IStarHyp, hence Cor105Hyp (cor105Hyp).

Reduction of the realization

theorem MultiplicativeBasisDeformations.RaySys.Sys.redLin_vecW {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (o : Option R) : (S.P.redLin red) (S.vecW O o) = S.vecW K o

theorem MultiplicativeBasisDeformations.RaySys.Sys.redLin_Φ2_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (c : S.C2 χ O) (u v : R) : (S.P.redLin red) (((S.Φ2 χ O c) (S.P.b O u)) (S.P.b O v)) = ((S.Φ2 χ K (⇑red ∘ c)) (S.P.b K u)) (S.P.b K v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.redLin_eq_sum {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (a : ↥(S.P.Lin O)) : (S.P.redLin red) a = ∑ u : R, red (((S.P.basis O).repr a) u) • S.P.b K u

theorem MultiplicativeBasisDeformations.RaySys.Sys.redLin_Φ2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {O K : Type u} [CommRing O] [Nontrivial O] [CommRing K] [Nontrivial K] (red : O →+* K) (c : S.C2 χ O) (a b : ↥(S.P.Lin O)) : (S.P.redLin red) (((S.Φ2 χ O c) a) b) = ((S.Φ2 χ K (⇑red ∘ c)) ((S.P.redLin red) a)) ((S.P.redLin red) b)

Reduction of coefficients commutes with Φ₂.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Φ2_smul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (t : O) (c : S.C2 χ O) : S.Φ2 χ O (t • c) = t • S.Φ2 χ O c

theorem MultiplicativeBasisDeformations.RaySys.Sys.isHCocycle_transp {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {μ : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)} (hμ : GExt.IsHCocycle μ) : GExt.IsHCocycle (S.transp k Θ μ)

theorem MultiplicativeBasisDeformations.MeshWalk.Φ2_b_isHom {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R LL : Type} [AddCommGroup LL] [DecidableEq LL] [Fintype R] [DecidableEq R] (S : RaySys.Sys D.PV R LL) (T : TabIso D S.P.toMult) (hT : ∀ (r : R), T.d r = S.P.deg (S.P.wt r)) (χ : LL) (hχ : 0 ≤ S.P.deg χ) (z : S.C2 χ (ZMod 2)) (u v : R) : (galgA0 D ⋯).gr.IsHom (T.d u + T.d v + S.P.deg χ) (T.Θ (((S.Φ2 χ (ZMod 2) z) (S.P.b (ZMod 2) u)) (S.P.b (ZMod 2) v)))

theorem MultiplicativeBasisDeformations.MeshWalk.hdeg_transp_Φ2 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R LL : Type} [AddCommGroup LL] [DecidableEq LL] [Fintype R] [DecidableEq R] (S : RaySys.Sys D.PV R LL) (T : TabIso D S.P.toMult) (hT : ∀ (r : R), T.d r = S.P.deg (S.P.wt r)) (χ : LL) (hχ : 0 ≤ S.P.deg χ) (z : S.C2 χ (ZMod 2)) : GExt.HDeg (galgA0 D ⋯) (S.transp (ZMod 2) T.Θ (S.Φ2 χ (ZMod 2) z)) (S.P.deg χ)

The cocycle Φ₂(z) on A⁽²⁾ has degree deg χ.

theorem MultiplicativeBasisDeformations.MeshWalk.πO_Φ2 {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R LL : Type} [AddCommGroup LL] [DecidableEq LL] [Fintype R] [DecidableEq R] (S : RaySys.Sys D.PV R LL) (T : TabIso D S.P.toMult) (χ : LL) (z : S.C2 χ (ZMod 4)) (a b : ↥(S.P.Lin (ZMod 4))) : (πO T) (((S.Φ2 χ (ZMod 4) z) a) b) = ((S.transp (ZMod 2) T.Θ (S.Φ2 χ (ZMod 2) (⇑Z4.red ∘ z))) ((πO T) a)) ((πO T) b)

theorem MultiplicativeBasisDeformations.MeshWalk.istar {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients (ZMod 2) Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional (ZMod 2) (meshFam Q c x ⟶ meshFam Q c y)] {R LL : Type} [AddCommGroup LL] [DecidableEq LL] [Fintype R] [DecidableEq R] (S : RaySys.Sys D.PV R LL) (T : TabIso D S.P.toMult) (hT : ∀ (r : R), T.d r = S.P.deg (S.P.wt r)) (J : D.InjData) (h1 : DegOne D) {RS : ScalarMeshCategory.RowSet Q} (hspan : ScalarMeshCategory.CokerSpan c RS) (htwo : ScalarMeshCategory.TwoRows Q RS) (χ : LL) (hχ : 0 < S.P.deg χ) : S.IStar χ

Proposition 10.3 in coefficients (prop:integral-bockstein).

theorem MultiplicativeBasisDeformations.istarHyp (k : Type u') [Field k] [IsAlgClosed k] [CharP k 2] : IStarHyp k

Proposition 10.3 for every basic representation-finite algebra (in coefficients).

theorem MultiplicativeBasisDeformations.integralBockstein (k : Type u') [Field k] [IsAlgClosed k] [CharP k 2] (A : Type u') [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (hbasic : IsBasicAlgebra A) (hA : IsRepresentationFinite k A) (S : IndSkeleton k A) (b : S.ArrowBases) (v₀ : S.ARVertex) (hF : IsRepresentationFinite k (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWalk.MeshWt S.arTranslationQuiver ℤ) (Rw : ι → (x : ↑S.arTranslationQuiver.nonprojective) × Quiver.Path ↑(S.arTranslationQuiver.tau x) ↑x) (i : ι) : 0 < (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).P.deg (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) → ∀ (c : (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).C2 (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) (ZMod 2)), ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).d2L (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) (ZMod 2)) c = 0 → ∃ (δ : (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).C1 (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) (ZMod 4)), ((MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).d1L (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) (ZMod 4)) δ = 2 • Z4.lift ∘ c ∧ (MeshWalk.SysD (S.arMeshData b) v₀ hF Wd).d1 (MeshWalk.rowWt (MeshWalk.dualWt Wd) (Rw i)) (ZMod 2) (⇑Z4.red ∘ δ) = 0

Proposition 10.3 (prop:integral-bockstein), as stated: for every basic representation-finite algebra in characteristic two and every positive character χ of the dual weights, the connecting map is surjective — every two-cocycle c over 𝔽₂ of character χ (of A⁽²⁾ ≅ 𝔽₂P) is (dδ)/2 for a one-cochain δ over ℤ/4 whose reduction is a derivation.

theorem MultiplicativeBasisDeformations.cor105Hyp (k : Type u') [Field k] [IsAlgClosed k] [CharP k 2] : Cor105Hyp k

Corollary 10.5 under the induction hypothesis (cor:zero-supported-coverage).