Proposition 11.3(2): scalar fibres are positive filtered deformations

binary-families.tex (prop:zero-product-family(2)): "Every scalar fibre is a positive filtered deformation of A₀." A scalar fibre of the family m + Σ_E T_E μ_E is the product x · y = xy + Σ_E λ_E μ_E(x, y), that is xy + coch_a(x, y) for a coefficient function a constant on the classes (EdgeOK). For Θ : kP ≅ Λ carrying each ray to a homogeneous element of degree deg ℓ(r): the product is associative (Prop 11.3(1), family_assoc) and unital (corrections vanish at identities, coch_e_left, coch_e_right); a correction u q_y v has degree at least deg ℓ(u) + deg ℓ(v) + 1 (deg_eps), so the product agrees with that of Λ up to terms of higher degree, and the length filtration makes the fibre a positive filtered deformation (Definition 6.2, Fib.posFiltration).

theorem MultiplicativeBasisDeformations.LenGrading.ge_sum' {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (m : ℕ) {κ : Type u_2} (s : Finset κ) (f : κ → Λ) (hf : ∀ i ∈ s, G.Ge m (f i)) : G.Ge m (∑ i ∈ s, f i)

theorem MultiplicativeBasisDeformations.LenGrading.ge₂_of_basis {k : Type u} [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {ι : Type u_1} [Fintype ι] (β : Module.Basis ι k Λ) (δ : ι → ℕ) (hβ : ∀ (i : ι), G.IsHom (δ i) (β i)) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) (h : ∀ (i j : ι), G.Ge (δ i + δ j + 1) ((μ (β i)) (β j))) {d e : ℕ} {a b : Λ} (ha : G.IsHom d a) (hb : G.IsHom e b) : G.Ge (d + e + 1) ((μ a) b)

A bilinear map raising degrees on basis pairs raises degrees.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_eps {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)) {u v t : R} (h : S.eps u v = S.rr t) : S.P.deg (S.P.wt u) + S.P.deg (S.P.wt v) + 1 ≤ S.P.deg (S.P.wt t)

A correction u q_y v raises the degree.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_one_left {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)) (c : R → R → k) (z : ↥(S.P.Lin k)) : ((S.coch k c) 1) z = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_one_right {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)) (c : R → R → k) (z : ↥(S.P.Lin k)) : ((S.coch k c) z) 1 = 0

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibreMul {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) : AssocMul k Λ

The scalar fibre with coefficients a (constant on the classes): the product x · y = xy + coch_a(x, y) transported to Λ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreMul_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] (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) (x y : ↥(S.P.Lin k)) : ((S.fibreMul k hfin Θ ha).mm (Θ x)) (Θ y) = Θ (x * y + ((S.coch k a) x) y)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreMul_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] (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) : (S.fibreMul k hfin Θ ⋯).mm = LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam

The fibre of the indicator family at T_{E_i} = λ_i is the fibre with coefficients Σ_i λ_i [E_i].

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreMul_hdef {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))) {a : R → R → k} (ha : S.EdgeOK k a) (d e : ℕ) (x y : Λ) (hx : G.IsHom d x) (hy : G.IsHom e y) : G.Ge (d + e + 1) (((S.fibreMul k hfin Θ ha).mm x) y - x * y)

The fibre product agrees with that of Λ up to terms of higher degree.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibrePosFiltration {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))) {a : R → R → k} (ha : S.EdgeOK k a) : PosFiltration G (Fib (S.fibreMul k hfin Θ ha))

Proposition 11.3(2) (prop:zero-product-family(2)): every scalar fibre of the family m + Σ_E T_E μ_E is a positive filtered deformation of A₀ ≅ Λ (Definition 6.2), filtered by degree.

theorem MultiplicativeBasisDeformations.RaySys.Sys.zeroProductFamily_fibre {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))) {n : ℕ} (E : Fin n → Quotient S.pairSetoid) (lam : Fin n → k) : ∃ (A : AssocMul k Λ), A.mm = LenGrading.mLam (fun (i : Fin n) => S.transp k Θ (S.muE k (E i))) lam ∧ Nonempty (PosFiltration G (Fib A))

Proposition 11.3(2), for the family of indicators of the classes E_i at T_{E_i} = λ_i.