Idempotents project onto their reconstructed coordinate rows

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

A selected idempotent has only its own diagonal interval coefficients.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_idempotent_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type v} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (m : ℕ) (p q : ι × Fin (m + 1)) (i : ι) (hpq : p ≠ q) : (intervalActionCoefficient R ⋯ e he0 he m p q) (e i) = 0

Off-diagonal projective morphisms of an idempotent vanish.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_idempotent_self {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type v} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (m : ℕ) (p : ι × Fin (m + 1)) (i : ι) : (intervalActionCoefficient R ⋯ e he0 he m p p) (e i) = if p.1 = i then CategoryTheory.CategoryStruct.id (intervalProjectiveLabel R ⋯ e he0 m p) else 0

The diagonal morphism is identity precisely on the selected idempotent label.

theorem MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionMap_idempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type v} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (F : CategoryTheory.Functor (PrincipalDegreeCategory R ⋯ e he0)ᵒᵖ (ModuleCat k)) [F.Additive] [CategoryTheory.Functor.Linear k F] (m : ℕ) (i : ι) (x : intervalCoordinateSpace R ⋯ e he0 F m) (p : ι × Fin (m + 1)) : (intervalActionMap R ⋯ e he0 he F m (e i)) x p = if p.1 = i then x p else 0

A selected idempotent acts as the projection onto its labelled coordinate row.