The family criterion with indicator cocycles

Proposition 7.9 (characteristic-two-construction.tex) for the selected binary family of the proof of Proposition 8.3 (main-theorems.tex): with A₀ ≅ kP through Θ, chosen indicator cocycles μ_i = μ_{E_i} of distinct classes satisfying the hypotheses of Theorem 7.7 and characters forming part of an integer basis, Corollary 7.8 gives a binary fibre isomorphic to A; by Proposition 11.3(3) the transported rays are a normed multiplicative basis and a ray transversal of A.

The hypotheses on μ_i (relative, homogeneous, associative family, spanning) are taken as the FamilyHyp of Theorem 7.7; they are discharged where A₀, its gradings and the indicator classes are constructed.

def MultiplicativeBasisDeformations.RaySys.Sys.transp {V R L : Type} [AddCommGroup 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)) : Λ →ₗ[k] Λ →ₗ[k] Λ

A bilinear map on kP transported along Θ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_apply {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)) (a b : Λ) : ((S.transp k Θ μ) a) b = Θ ((μ (Θ.symm a)) (Θ.symm b))

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.indComb {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] {n : ℕ} (E : Fin n → Quotient S.pairSetoid) (lam : Fin n → k) : R → R → k

The coefficient function of a combination of distinct indicator classes.

theorem MultiplicativeBasisDeformations.RaySys.Sys.indComb_binary {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] {n : ℕ} {E : Fin n → Quotient S.pairSetoid} (hE : Function.Injective E) {lam : Fin n → k} (hlam : ∀ (i : Fin n), lam i = 0 ∨ lam i = 1) (r s : R) : S.indComb k E lam r s = 0 ∨ S.indComb k E lam r s = 1

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_family {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] Λ) {n : ℕ} (E : Fin n → Quotient S.pairSetoid) (lam : Fin n → k) (a b : ↥(S.P.Lin k)) : ((LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam) (Θ a)) (Θ b) = Θ (a * b + ((S.coch k (S.indComb k E lam)) a) b)

theorem MultiplicativeBasisDeformations.RaySys.Sys.char2_core {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] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {Λ : Type u} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {Vx : G.Vertices} {L' : Type} [AddCommGroup L'] [DecidableEq L'] {W : LatGrading k Λ L'} (compat : ∀ (d : ℕ) (l : L') (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x)) (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {n : ℕ} {E : Fin n → Quotient S.pairSetoid} (hE : Function.Injective E) {χ : Fin n → L'} (hχ : ∀ (i : Fin n) (l l' : L') (x y : Λ), W.IsHom l x → W.IsHom l' y → W.IsHom (l + l' + χ i) (((S.transp k Θ (S.muE k (E i))) x) y)) {qd : Fin n → ℕ} (H : LenGrading.FamilyHyp Vx (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) qd) (he0 : ∀ (i : Fin Vx.n), W.IsHom 0 (Vx.e i)) (hbasis : ∃ (ι : Type) (b : Module.Basis ι ℤ L') (j : Fin n → ι), Function.Injective j ∧ ∀ (i : Fin n), b (j i) = χ i) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (P : PosFiltration G B) : ∃ (lam : Fin n → k) (_ : ∀ (i : Fin n), lam i = 0 ∨ lam i = 1) (Ψ : Λ ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), (↑Θ ≪≫ₗ Ψ) (a * z + ((S.coch k (S.indComb k E lam)) a) z) = (↑Θ ≪≫ₗ Ψ) a * (↑Θ ≪≫ₗ Ψ) z), IsNormedMultiplicativeBasis (S.fibreBasis k hfin (S.indComb k E lam) (↑Θ ≪≫ₗ Ψ) hΨ) ∧ (S.fibreIdem k hfin (S.indComb k E lam) (↑Θ ≪≫ₗ Ψ) hΨ).IsRayTransversal ⇑(S.fibreBasis k hfin (S.indComb k E lam) (↑Θ ≪≫ₗ Ψ) hΨ) ∧ (S.fibreIdem k hfin (S.indComb k E lam) (↑Θ ≪≫ₗ Ψ) hΨ).IsRayPres S.P.toMult (S.fibreIdx k hfin (S.indComb k E lam) (↑Θ ≪≫ₗ Ψ) hΨ) (S.βv k (↑Θ ≪≫ₗ Ψ))

The selected binary family recovers A with a normed multiplicative ray basis (Proposition 7.9 with Propositions 11.2, 11.3 and Corollary 7.8).