Relative cochains of character χ and their coefficients

integral-deformations.tex: "all cochains are normalized relative to the vertex identities and respect the categorical grading and the integer ray weights." A normalized relative two-cochain of character χ on Λ ≅ kP is Φ₂ of its coefficients (realize); it is a coboundary exactly when its coefficients are d₁ of coefficients (coef_of_isCobdry, isCobdry_of_coef).

Coordinates of products

theorem MultiplicativeBasisDeformations.RaySys.Sys.repr_b_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [CommRing k] [Nontrivial k] (u : R) (y : ↥(S.P.Lin k)) (t : R) : ((S.P.basis k).repr (S.P.b k u * y)) t = ∑ s : R, ((S.P.basis k).repr y) s * if S.P.mul u s = some t then 1 else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.repr_mul_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [CommRing k] [Nontrivial k] (v : R) (y : ↥(S.P.Lin k)) (t : R) : ((S.P.basis k).repr (y * S.P.b k v)) t = ∑ s : R, ((S.P.basis k).repr y) s * if S.P.mul s v = some t then 1 else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.sum_single_of_unique {R : Type} [Fintype R] [DecidableEq R] (k : Type u) [CommRing k] [Nontrivial k] {f g : R → k} {s₀ : R} (h : ∀ (s : R), g s ≠ 0 → s = s₀) : ∑ s : R, f s * g s = f s₀ * g s₀

theorem MultiplicativeBasisDeformations.RaySys.Sys.repr_e_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [CommRing k] [Nontrivial k] (x : V) (y : ↥(S.P.Lin k)) (t : R) : ((S.P.basis k).repr (S.P.b k (S.P.e x) * y)) t = if S.P.src t = x then ((S.P.basis k).repr y) t else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.repr_mul_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [CommRing k] [Nontrivial k] (y : ↥(S.P.Lin k)) (x : V) (t : R) : ((S.P.basis k).repr (y * S.P.b k (S.P.e x))) t = if S.P.tgt t = x then ((S.P.basis k).repr y) t else 0

Coboundaries in coefficients

theorem MultiplicativeBasisDeformations.RaySys.Sys.coef_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [CommRing k] [Nontrivial k] (y : ↥(S.P.Lin k)) {u v t₀ : R} (hI : S.I2 χ (u, v)) (ht₀ : S.w2 χ u v = some t₀) : ((S.P.basis k).repr (S.P.b k u * y)) t₀ = if S.Shift χ v ∧ (S.P.mul u (S.succ χ v)).isSome = true then ((S.P.basis k).repr y) (S.succ χ v) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coef_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [CommRing k] [Nontrivial k] (y : ↥(S.P.Lin k)) {u v t₀ : R} (hI : S.I2 χ (u, v)) (ht₀ : S.w2 χ u v = some t₀) : ((S.P.basis k).repr (y * S.P.b k v)) t₀ = if S.Shift χ u ∧ (S.P.mul (S.succ χ u) v).isSome = true then ((S.P.basis k).repr y) (S.succ χ u) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coef_mid {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [CommRing k] [Nontrivial k] (H : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) {u v t₀ : R} (hI : S.I2 χ (u, v)) (ht₀ : S.w2 χ u v = some t₀) : ((S.P.basis k).repr (H (S.P.b k u * S.P.b k v))) t₀ = match S.P.mul u v with | some t => if S.Shift χ t then ((S.P.basis k).repr (H (S.P.b k t))) (S.succ χ t) else 0 | none => 0

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.coef1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [CommRing k] [Nontrivial k] (H : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) : S.C1 χ k

The coefficients of a linear map on the shiftable rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coef_of_hcobdry {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [CommRing k] [Nontrivial k] (c : S.C2 χ k) (H : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) (h : S.Φ2 χ k c = GExt.hcobdry H) : c = S.d1 χ k (S.coef1 k H)

A coboundary has coefficients d₁ of coefficients.

Realization of relative cochains of character χ

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.coefOf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (k : Type u) [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) (φ : Λ →ₗ[k] Λ →ₗ[k] Λ) : S.C2 χ k

The coefficients of a two-cochain on Λ ≅ kP: the coordinate of φ(r, s) at w₂(r, s).

theorem MultiplicativeBasisDeformations.RaySys.Sys.basisΛ_repr {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] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) (x : Λ) (t : R) : ((S.basisΛ k Θ).repr x) t = ((S.P.basis k).repr (Θ.symm x)) t

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_smul_of_repr {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] [IsAlgClosed k] {z : ↥(S.P.Lin k)} {t₀ : R} (h : ∀ (t : R), ((S.P.basis k).repr z) t ≠ 0 → t = t₀) : z = ((S.P.basis k).repr z) t₀ • S.P.b k t₀

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_zero_of_repr {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] [IsAlgClosed k] {z : ↥(S.P.Lin k)} (h : ∀ (t : R), ((S.P.basis k).repr z) t = 0) : z = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.realize {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} {W : LatGrading k Λ L} (hW : ∀ (r : R), W.IsHom (S.P.wt r) (Θ (S.P.b k r))) (Vx : G.Vertices) (hVx : ∀ (x : V), ∃ (i : Fin Vx.n), Vx.e i = Θ (S.P.b k (S.P.e x))) {φ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hr : LenGrading.IsRel₂ Vx φ) (hc : W.Char₂ χ φ) : φ = S.transp k Θ (S.Φ2 χ k (S.coefOf χ k Θ φ))

A normalized relative two-cochain of character χ is Φ₂ of its coefficients.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coef_of_isCobdry {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} {q : ℕ} (c : S.C2 χ k) (h : IsCobdry k G q (S.transp k Θ (S.Φ2 χ k c))) : ∃ (f : S.C1 χ k), c = S.d1 χ k f

A coboundary on Λ has coefficients d₁ of coefficients.

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_hcobdry {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] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) (h : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) : S.transp k Θ (GExt.hcobdry h) = LenGrading.cobdry k (Θ.toLinearMap ∘ₗ h ∘ₗ Θ.symm.toLinearMap)

theorem MultiplicativeBasisDeformations.RaySys.Sys.isCobdry_of_d1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} (hG : ∀ (r : R), G.IsHom (S.P.deg (S.P.wt r)).toNat (Θ (S.P.b k r))) (hχ : 0 ≤ S.P.deg χ) (f : S.C1 χ k) : IsCobdry k G (S.P.deg χ).toNat (S.transp k Θ (S.Φ2 χ k (S.d1 χ k f)))

d₁ of coefficients is a coboundary of degree deg χ on Λ.

Corollary 10.5 on Λ ≅ kP, given Proposition 10.3

theorem MultiplicativeBasisDeformations.RaySys.Sys.isHCocycle_of_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] [IsAlgClosed 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 : LenGrading.IsCocycle₂ (S.transp k Θ μ)) : GExt.IsHCocycle μ

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.indOf {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (k : Type u) [Field k] (u : S.C2 χ k) (x y : R) : k

The indicator coefficients of a supported coefficient cochain.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_indOf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {u : S.C2 χ k} (hu : u ∈ S.Usub χ k) : S.coch k (S.indOf χ k u) = S.Φ2 χ k u

theorem MultiplicativeBasisDeformations.RaySys.Sys.cor105_of_IStar {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) [CharP k 2] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hWl : ∀ (w : R → ZMod 2), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → w t = w r + w s) → ∃ (ω : R → ℤ), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) ∧ ∀ (r : R), S.TB χ r → ↑(ω r) = w r) (hI : S.IStar χ) {G : LenGrading k Λ} {W : LatGrading k Λ L} (hG : ∀ (r : R), G.IsHom (S.P.deg (S.P.wt r)).toNat (Θ (S.P.b k r))) (hW : ∀ (r : R), W.IsHom (S.P.wt r) (Θ (S.P.b k r))) (Vx : G.Vertices) (hVx : ∀ (x : V), ∃ (i : Fin Vx.n), Vx.e i = Θ (S.P.b k (S.P.e x))) {q : ℕ} {φ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hr : LenGrading.IsRel₂ Vx φ) (hd : G.HasDeg₂ q φ) (hcoc : LenGrading.IsCocycle₂ φ) (hc : W.Char₂ χ φ) (hnc : ¬IsCobdry k G q φ) : ∃ (a : R → R → k), S.EdgeOK k a ∧ (∀ (z : R × R), a z.1 z.2 ≠ 0 → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) ∧ ¬IsCobdry k G (S.P.deg χ).toNat (S.transp k Θ (S.coch k a))

Corollary 10.5 (cor:zero-supported-coverage) on Λ ≅ kP, given Proposition 10.3.