Algebra elements as matrices of interval projective morphisms #
def
MagnitudeConjecture.Graded.FiniteGradedModule.intervalProjectiveLabel
{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}
(e : ι → A)
(he0 : ∀ (i : ι), e i ∈ R.component 0)
(m : ℕ)
(p : ι × Fin (m + 1))
:
PrincipalDegreeCategory R ⋯ e he0
An interval coordinate as a degree-labelled projective.
Instances For
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient
{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)
(m : ℕ)
(p q : ι × Fin (m + 1))
:
A →ₗ[k] intervalProjectiveLabel R ⋯ e he0 m p ⟶ intervalProjectiveLabel R ⋯ e he0 m q
The homogeneous corner coefficient regarded as a projective morphism.
Instances For
@[simp]
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_coord
{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)
(m : ℕ)
(p q : ι × Fin (m + 1))
(a : A)
:
↑((principalDegreeHomEquiv R ⋯ e he0 he (intervalProjectiveLabel R ⋯ e he0 m p) (intervalProjectiveLabel R ⋯ e he0 m q))
((intervalActionCoefficient R ⋯ e he0 he m p q) a)) = intervalCorner R e m p q a
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_mul
{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)
(hneg : ∀ d < 0, R.component d = ⊥)
(hsum : ∑ i : ι, e i = 1)
(m : ℕ)
(p q : ι × Fin (m + 1))
(a b : A)
:
(intervalActionCoefficient R ⋯ e he0 he m p q) (a * b) = ∑ z : ι × Fin (m + 1),
CategoryTheory.CategoryStruct.comp ((intervalActionCoefficient R ⋯ e he0 he m p z) a)
((intervalActionCoefficient R ⋯ e he0 he m z q) b)
Matrix multiplication is represented by composition through the interval projectives.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_one_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)
(h1 : 1 ∈ R.component 0)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
(p : ι × Fin (m + 1))
:
(intervalActionCoefficient R ⋯ e he0 he m p p) 1 = CategoryTheory.CategoryStruct.id (intervalProjectiveLabel R ⋯ e he0 m p)
The diagonal coefficient of 1 is the identity.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.intervalActionCoefficient_one_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)
(h1 : 1 ∈ R.component 0)
(horth : Pairwise fun (i j : ι) => e i * e j = 0)
(m : ℕ)
(p q : ι × Fin (m + 1))
(hpq : p ≠ q)
:
(intervalActionCoefficient R ⋯ e he0 he m p q) 1 = 0
The off-diagonal coefficients of 1 vanish.