Rays of the fibres of the zero-product family

Proposition 11.3(3) (binary-families.tex), in the form used by Proposition 7.9: let B be an algebra with a linear isomorphism Ψ : kP → B carrying a fibre product m_c = m + Σ c_z ε_z to the product of B. "Corrections involve only generating nonlocal inputs. Products with local basis vectors […] are unchanged. Thus the local rings and both endpoint actions are the same as in A₀, and the basis vectors represent exactly the same endpoint-unit orbits." Hence the images Ψ b_e are a complete set of primitive orthogonal idempotents of B, and the images Ψ b_r are a ray transversal. When the coefficients are zero or one, products of these vectors are basis vectors or zero, and by Corollary 3.3 the transversal is a normed multiplicative basis.

Deviation: the fibre is not formed as a separate algebra; everything is read in B through Ψ, which is how Proposition 7.9 uses it.

Corrections vanish on local inputs

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_b_local_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) {l : R} (hl : S.P.src l = S.P.tgt l) (z : ↥(S.P.Lin k)) : ((S.coch k c) (S.P.b k l)) z = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_local_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) {x : V} {a : ↥(S.P.Lin k)} (ha : a ∈ S.P.corSp k x x) (z : ↥(S.P.Lin k)) : ((S.coch k c) a) z = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_b_local_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) {l : R} (hl : S.P.src l = S.P.tgt l) (a : ↥(S.P.Lin k)) : ((S.coch k c) a) (S.P.b k l) = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_local_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) {y : V} {z : ↥(S.P.Lin k)} (hz : z ∈ S.P.corSp k y y) (a : ↥(S.P.Lin k)) : ((S.coch k c) a) z = 0

The transported structure

theorem MultiplicativeBasisDeformations.RaySys.Sys.Ψ_mul_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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {x : V} {a : ↥(S.P.Lin k)} (ha : a ∈ S.P.corSp k x x) (z : ↥(S.P.Lin k)) : Ψ a * Ψ z = Ψ (a * z)

theorem MultiplicativeBasisDeformations.RaySys.Sys.Ψ_mul_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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {y : V} {z : ↥(S.P.Lin k)} (hz : z ∈ S.P.corSp k y y) (a : ↥(S.P.Lin k)) : Ψ a * Ψ z = Ψ (a * z)

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mem_corSp {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] (x : V) : S.P.b k (S.P.e x) ∈ S.P.corSp k x x

theorem MultiplicativeBasisDeformations.RaySys.Sys.Ψ_one {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : Ψ 1 = 1

def MultiplicativeBasisDeformations.RaySys.Sys.Eb {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] {B : Type u} [Ring B] [Algebra k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (x : V) : B

The transported identity vectors.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Eb_complete {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : CompleteOrthogonalIdempotents (S.Eb k Ψ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.Eb_mul_mul_Eb {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (x y : V) (a : ↥(S.P.Lin k)) : S.Eb k Ψ x * Ψ a * S.Eb k Ψ y = Ψ (S.P.b k (S.P.e x) * a * S.P.b k (S.P.e y))

The corner of B at x, y is the image of the corner of kP.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Eb_primitive {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (x : V) : IsPrimitiveIdempotent (S.Eb k Ψ x)

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibreIdem {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : PrimitiveIdempotents B

The transported identities are a complete set of primitive orthogonal idempotents.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibreIdx {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : V ≃ Fin (S.fibreIdem k hfin c Ψ hΨ).m

Vertices as indices of the transported idempotents.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_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) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (i : Fin (S.fibreIdem k hfin c Ψ hΨ).m) : (S.fibreIdem k hfin c Ψ hΨ).e i = Ψ (S.P.b k (S.P.e ((S.fibreIdx k hfin c Ψ hΨ).symm i)))

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_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) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (x : V) : (S.fibreIdem k hfin c Ψ hΨ).e ((S.fibreIdx k hfin c Ψ hΨ) x) = Ψ (S.P.b k (S.P.e x))

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_mem_corner_iff {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {i j : Fin (S.fibreIdem k hfin c Ψ hΨ).m} {z : B} : z ∈ (S.fibreIdem k hfin c Ψ hΨ).corner i j ↔ Ψ.symm z ∈ S.P.corSp k ((S.fibreIdx k hfin c Ψ hΨ).symm i) ((S.fibreIdx k hfin c Ψ hΨ).symm j)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_isCornerUnit_iff {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {i : Fin (S.fibreIdem k hfin c Ψ hΨ).m} {u : B} : (S.fibreIdem k hfin c Ψ hΨ).IsCornerUnit i u ↔ S.P.IsLocUnit k ((S.fibreIdx k hfin c Ψ hΨ).symm i) (Ψ.symm u)

def MultiplicativeBasisDeformations.RaySys.Sys.βv {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] {B : Type u} [Ring B] [Algebra k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (r : R) : B

The transported ray vectors.

theorem MultiplicativeBasisDeformations.RaySys.Sys.βv_mem_corner {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (r : R) : S.βv k Ψ r ∈ (S.fibreIdem k hfin c Ψ hΨ).corner ((S.fibreIdx k hfin c Ψ hΨ) (S.P.src r)) ((S.fibreIdx k hfin c Ψ hΨ) (S.P.tgt r))

theorem MultiplicativeBasisDeformations.RaySys.Sys.βv_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] {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (r : R) : S.βv k Ψ r ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_of_mem_ray {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {r s : R} (h : S.βv k Ψ r ∈ (S.fibreIdem k hfin c Ψ hΨ).ray ((S.fibreIdx k hfin c Ψ hΨ) (S.P.src s)) ((S.fibreIdx k hfin c Ψ hΨ) (S.P.tgt s)) (S.βv k Ψ s)) : S.InU r s

Rays of the transported vectors are ordered by U.

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_ray_βv {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {i j : Fin (S.fibreIdem k hfin c Ψ hΨ).m} {z : B} (hz : z ∈ (S.fibreIdem k hfin c Ψ hΨ).corner i j) (hz0 : z ≠ 0) : ∃ (r : R), (S.fibreIdx k hfin c Ψ hΨ) (S.P.src r) = i ∧ (S.fibreIdx k hfin c Ψ hΨ) (S.P.tgt r) = j ∧ z ∈ (S.fibreIdem k hfin c Ψ hΨ).ray i j (S.βv k Ψ r)

Every nonzero corner element of B lies in the ray of a transported vector.

def MultiplicativeBasisDeformations.RaySys.Sys.fibreRay {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (r : R) : PrimitiveIdempotents.NonzeroRay k (S.fibreIdem k hfin c Ψ hΨ)

The ray of a transported vector.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_fibreRay {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (r : R) : S.βv k Ψ r ∈ ↑(S.fibreRay k hfin c Ψ hΨ r)

theorem MultiplicativeBasisDeformations.PrimitiveIdempotents.nonzeroRay_eq_of_mem (k : Type u) [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (F : PrimitiveIdempotents A) {ρ ρ' : NonzeroRay k F} {g : A} (h : g ∈ ↑ρ) (h' : g ∈ ↑ρ') : ρ = ρ'

Two nonzero rays with a common element are equal.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreRay_injective {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : Function.Injective (S.fibreRay k hfin c Ψ hΨ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreRay_surjective {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : Function.Surjective (S.fibreRay k hfin c Ψ hΨ)

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibreRayEquiv {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : R ≃ PrimitiveIdempotents.NonzeroRay k (S.fibreIdem k hfin c Ψ hΨ)

Rays of B are the rays of P.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.fibreBasis {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : Module.Basis (PrimitiveIdempotents.NonzeroRay k (S.fibreIdem k hfin c Ψ hΨ)) k B

The transported basis, indexed by the rays of B.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreBasis_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)) (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (ρ : PrimitiveIdempotents.NonzeroRay k (S.fibreIdem k hfin c Ψ hΨ)) : (S.fibreBasis k hfin c Ψ hΨ) ρ = S.βv k Ψ ((S.fibreRayEquiv k hfin c Ψ hΨ).symm ρ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreBasis_ray {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (r : R) : (S.fibreBasis k hfin c Ψ hΨ) ((S.fibreRayEquiv k hfin c Ψ hΨ) r) = S.βv k Ψ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreBasis_isRayTransversal {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) : (S.fibreIdem k hfin c Ψ hΨ).IsRayTransversal ⇑(S.fibreBasis k hfin c Ψ hΨ)

The transported basis is a ray transversal.

theorem MultiplicativeBasisDeformations.RaySys.Sys.βv_mul_βv {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] (c : R → R → k) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (hc01 : ∀ (r s : R), c r s = 0 ∨ c r s = 1) (r s : R) : S.βv k Ψ r * S.βv k Ψ s = 0 ∨ ∃ (t : R), S.βv k Ψ r * S.βv k Ψ s = S.βv k Ψ t

Products of transported vectors at binary points are transported vectors or zero.

Endpoint subbimodules of a fibre are spanned by rays

The endpoint actions of the fibre are those of kP (Ψ_mul_left, Ψ_mul_right), so an endpoint subbimodule of B pulls back to one of kP, which is spanned by rays since kP is representation-finite. No representation-finiteness of B is needed.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_zero_coef {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] : S.coch k 0 = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.hΨ₀ {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 z : ↥(S.P.Lin k)) : (LinearEquiv.refl k ↥(S.P.Lin k)) (a * z + ((S.coch k 0) a) z) = (LinearEquiv.refl k ↥(S.P.Lin k)) a * (LinearEquiv.refl k ↥(S.P.Lin k)) z

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.RaySys.Sys.idem₀ {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)) : PrimitiveIdempotents ↥(S.P.Lin k)

kP with its identity vectors and rays, as the fibre at 0.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_mem_corner_iff₀ {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {x y : V} {z : ↥(S.P.Lin k)} : Ψ z ∈ (S.fibreIdem k hfin c Ψ hΨ).corner ((S.fibreIdx k hfin c Ψ hΨ) x) ((S.fibreIdx k hfin c Ψ hΨ) y) ↔ z ∈ (S.idem₀ k hfin).corner ((S.fibreIdx k hfin 0 (LinearEquiv.refl k ↥(S.P.Lin k)) ⋯) x) ((S.fibreIdx k hfin 0 (LinearEquiv.refl k ↥(S.P.Lin k)) ⋯) y)

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_le_span {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) {x y : V} {N : Submodule k B} (hN : (S.fibreIdem k hfin c Ψ hΨ).IsEndpointSubbimodule ((S.fibreIdx k hfin c Ψ hΨ) x) ((S.fibreIdx k hfin c Ψ hΨ) y) N) : N ≤ Submodule.span k (S.βv k Ψ '' {r : R | S.βv k Ψ r ∈ N})

Every endpoint subbimodule of a fibre is spanned by the transported rays it contains.

def MultiplicativeBasisDeformations.RaySys.Sys.radPowIdeal (k : Type u) [Field k] {A : Type u} [Ring A] [Algebra k A] {n : ℕ} (hn : 1 ≤ n) : TwoSidedIdeal A

A radical power as a two-sided ideal.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_radPowIdeal (k : Type u) [Field k] [IsAlgClosed k] {A : Type u} [Ring A] [Algebra k A] {n : ℕ} (hn : 1 ≤ n) (a : A) : a ∈ radPowIdeal k hn ↔ a ∈ algebraRadicalPow k A n

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibreBasis_normed {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (hc01 : ∀ (r s : R), c r s = 0 ∨ c r s = 1) : IsNormedMultiplicativeBasis (S.fibreBasis k hfin c Ψ hΨ)

Proposition 11.3(3) in B: at binary points the transported rays are a normed multiplicative basis and a ray transversal.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fibre_hasNormedBasis {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) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Ψ : ↥(S.P.Lin k) ≃ₗ[k] B) (hΨ : ∀ (a z : ↥(S.P.Lin k)), Ψ (a * z + ((S.coch k c) a) z) = Ψ a * Ψ z) (hc01 : ∀ (r s : R), c r s = 0 ∨ c r s = 1) : HasNormedMultiplicativeBasis k B

B has a normed multiplicative basis (Proposition 11.3(3) with Proposition 7.9).