The interval matrix coefficients of a nonnegatively graded algebra

noncomputable def MagnitudeConjecture.Graded.intervalCorner {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} (e : ι → A) (m : ℕ) (p q : ι × Fin (m + 1)) (a : A) : A

The coefficient sending the (j,t) coordinate to (i,r).

theorem MagnitudeConjecture.Graded.intervalCorner_add {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} [Fintype ι] (e : ι → A) (m : ℕ) (p q : ι × Fin (m + 1)) (a b : A) : intervalCorner R e m p q (a + b) = intervalCorner R e m p q a + intervalCorner R e m p q b

theorem MagnitudeConjecture.Graded.intervalCorner_smul {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} [Fintype ι] (e : ι → A) (m : ℕ) (p q : ι × Fin (m + 1)) (c : k) (a : A) : intervalCorner R e m p q (c • a) = c • intervalCorner R e m p q a

theorem MagnitudeConjecture.Graded.intervalCorner_mem {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} [Fintype ι] (e : ι → A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (m : ℕ) (p q : ι × Fin (m + 1)) (a : A) : intervalCorner R e m p q a ∈ cornerComponent R (e p.1) (e q.1) (↑↑p.2 - ↑↑q.2)

theorem MagnitudeConjecture.Graded.sum_idempotent_products {A : Type u_2} [Ring A] {ι : Type u_3} [Fintype ι] (e : ι → A) (he : ∀ (i : ι), e i * e i = e i) (hsum : ∑ i : ι, e i = 1) (x y : A) : ∑ i : ι, x * e i * (e i * y) = x * y

Completeness inserts all middle idempotents into a product.

theorem MagnitudeConjecture.Graded.intervalCorner_mul {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} [Fintype ι] (e : ι → A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) (he : ∀ (i : ι), e i * e i = e i) (hneg : ∀ d < 0, R.component d = ⊥) (hsum : ∑ i : ι, e i = 1) (m : ℕ) (p q : ι × Fin (m + 1)) (a b : A) : intervalCorner R e m p q (a * b) = ∑ z : ι × Fin (m + 1), intervalCorner R e m p z a * intervalCorner R e m z q b

Matrix multiplication of the finite interval coefficients agrees with algebra multiplication.

theorem MagnitudeConjecture.Graded.intervalCorner_one {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) {ι : Type u_3} [Fintype ι] (e : ι → A) (he : ∀ (i : ι), e i * e i = e i) (h1 : 1 ∈ R.component 0) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (m : ℕ) (p q : ι × Fin (m + 1)) : intervalCorner R e m p q 1 = if p = q then e p.1 else 0

The coefficient matrix of 1 is the identity on the idempotent coordinates.