The corner-space description of graded projective morphisms

def MagnitudeConjecture.Graded.cornerComponent {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) (e f : A) (d : ℤ) : Submodule k A

The degree-d part of eAf, written by its two idempotent equations.

def MagnitudeConjecture.Graded.principalCoordinateEquiv {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra 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)) [FiniteDimensional k A] (e f : A) (hf : f * f = f) (hf0 : f ∈ R.component 0) (d : ℤ) : ↥(idempotentComponent R (principalProjectiveGrading R ⋯ f hf0) e d) ≃ₗ[k] ↥(cornerComponent R e f d)

The e-coordinate of Af is precisely the corner eAf, degree by degree.

def MagnitudeConjecture.Graded.principalCornerHomEquiv {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra 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)) [FiniteDimensional k A] (e f : A) (he : e * e = e) (hf : f * f = f) (he0 : e ∈ R.component 0) (hf0 : f ∈ R.component 0) (d : ℤ) : ↥((principalProjectiveGrading R ⋯ e he0).homComponent (principalProjectiveGrading R ⋯ f hf0) d) ≃ₗ[k] ↥(cornerComponent R e f d)

Homogeneous module maps Ae → Af identify with the expected homogeneous corner.

theorem MagnitudeConjecture.Graded.principal_apply {A : Type u_2} [Ring A] {M : Type u_3} [AddCommGroup M] [Module A M] (e : A) (he : e * e = e) (f : ↥(principalProjective e) →ₗ[A] M) (z : ↥(principalProjective e)) : f z = ↑z • f (principalGenerator e)

Maps from Ae are determined on every vector by their value at e.

theorem MagnitudeConjecture.Graded.principal_comp_evaluation {A : Type u_2} [Ring A] (e f g : A) (hf : f * f = f) (a : ↥(principalProjective e) →ₗ[A] ↥(principalProjective f)) (b : ↥(principalProjective f) →ₗ[A] ↥(principalProjective g)) : ↑(b (a (principalGenerator e))) = ↑(a (principalGenerator e)) * ↑(b (principalGenerator f))

Composition of projective maps is multiplication of their corner coordinates.