The indicator family on a graded algebra Λ ≅ kP

For Θ : kP ≅ Λ carrying ray vectors to homogeneous elements (degree deg ℓ(r) and weight ℓ(r)): transported supported cochains satisfying the equalities of Proposition 11.2 are cocycles; they are normalized relative to the transported identities; an indicator of a class of character χ has character χ and internal degree deg χ; and the family m + Σ t_E μ_E is associative (Proposition 11.3(1)). These are the hypotheses of Theorem 7.7 other than spanning (binary-families.tex).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.basisΛ {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] Λ) : Module.Basis R k Λ

The transported ray basis.

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

Cocycles and associativity

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_isCocycle {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₂ μ) : LenGrading.IsCocycle₂ (S.transp k Θ μ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_coch_isCocycle {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {a : R → R → k} (ha : S.EdgeOK k a) : LenGrading.IsCocycle₂ (S.transp k Θ (S.coch k a))

theorem MultiplicativeBasisDeformations.RaySys.Sys.edgeOK_add {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] {a a' : R → R → k} (ha : S.EdgeOK k a) (ha' : S.EdgeOK k a') : S.EdgeOK k (a + a')

theorem MultiplicativeBasisDeformations.RaySys.Sys.edgeOK_smul {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] (t : k) {a : R → R → k} (ha : S.EdgeOK k a) : S.EdgeOK k (t • a)

theorem MultiplicativeBasisDeformations.RaySys.Sys.edgeOK_indComb {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) (lam : Fin n → k) : S.EdgeOK k (S.indComb k E lam)

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_family_assoc {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {n : ℕ} (E : Fin n → Quotient S.pairSetoid) (lam : Fin n → k) (x y z : Λ) : ((LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam) (((LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam) x) y)) z = ((LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam) x) (((LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam) y) z)

The transported indicator family is associative (Proposition 11.3(1)).

Relative cochains

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_isRel {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} (Vx : G.Vertices) (hVx : ∀ (i : Fin Vx.n), ∃ (x : V), Vx.e i = Θ (S.P.b k (S.P.e x))) (a : R → R → k) : LenGrading.IsRel₂ Vx (S.transp k Θ (S.coch k a))

Transported supported cochains are normalized relative cochains.

Degrees and characters

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_muE_char {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {W : LatGrading k Λ L} (hW : ∀ (r : R), W.IsHom (S.P.wt r) (Θ (S.P.b k r))) {E : Quotient S.pairSetoid} {χ : L} (hE : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) : W.Char₂ χ (S.transp k Θ (S.muE k E))

An indicator of a class of character χ has character χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_muE_deg {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 Λ] (Θ : ↥(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))) {E : Quotient S.pairSetoid} {χ : L} (hE : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) (hχ : 0 ≤ S.P.deg χ) : G.HasDeg₂ (S.P.deg χ).toNat (S.transp k Θ (S.muE k E))

An indicator of a class of character χ has internal degree deg χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_add {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)) : S.transp k Θ (μ + ν) = S.transp k Θ μ + S.transp k Θ ν

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_smul {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] Λ) (t : k) (μ : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) : S.transp k Θ (t • μ) = t • S.transp k Θ μ

theorem MultiplicativeBasisDeformations.RaySys.Sys.transp_sum {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] Λ) {ι : Type u_1} (s : Finset ι) (μ : ι → ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)) : S.transp k Θ (∑ i ∈ s, μ i) = ∑ i ∈ s, S.transp k Θ (μ i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.muE_eq_zero {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] {E : Quotient S.pairSetoid} (h : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 = 0) : S.muE k E = 0

def MultiplicativeBasisDeformations.RaySys.Sys.IsCobdry (k : Type u) [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) (φ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Prop

A coboundary of internal degree q.

theorem MultiplicativeBasisDeformations.RaySys.Sys.isCobdry_zero (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) : IsCobdry k G q 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.isCobdry_smul (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} (t : k) {φ : Λ →ₗ[k] Λ →ₗ[k] Λ} (h : IsCobdry k G q φ) : IsCobdry k G q (t • φ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.isCobdry_sum (k : Type u) [Field k] [IsAlgClosed k] {Λ : Type u} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {ι : Type u_1} (s : Finset ι) {φ : ι → Λ →ₗ[k] Λ →ₗ[k] Λ} (h : ∀ i ∈ s, IsCobdry k G q (φ i)) : IsCobdry k G q (∑ i ∈ s, φ i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.select_class {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} {a : R → R → k} (ha : S.EdgeOK k a) {χ : L} (hsupp : ∀ (z : R × R), a z.1 z.2 ≠ 0 → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) {q : ℕ} (hnz : ¬IsCobdry k G q (S.transp k Θ (S.coch k a))) : ∃ (E : Quotient S.pairSetoid), (∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) ∧ ¬IsCobdry k G q (S.transp k Θ (S.muE k E))

Selection of an indicator (proof of Proposition 8.3): a supported cocycle of character χ with nonzero class is a combination of indicators of that character, at least one of which has nonzero class.

theorem MultiplicativeBasisDeformations.RaySys.Sys.classChar_unique {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 Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {E : Quotient S.pairSetoid} {χ χ' : L} (h1 : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) (h2 : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ') {G : LenGrading k Λ} {q : ℕ} (hnz : ¬IsCobdry k G q (S.transp k Θ (S.muE k E))) : χ = χ'

A class with a nonzero correction has only one character.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_eq_of_ne_zero {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] Λ) {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))) {φ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hφ : φ ≠ 0) {q : ℕ} (hd : G.HasDeg₂ q φ) {χ : L} (hc : W.Char₂ χ φ) : S.P.deg χ = ↑q

A nonzero cochain of internal degree q and character χ has deg χ = q.