Homogeneous maps from the projective attached to an idempotent #
@[reducible, inline]
abbrev
MagnitudeConjecture.Graded.principalProjective
{A : Type u_2}
[Ring A]
(e : A)
:
Submodule A A
The principal left ideal Ae as the image of right multiplication by e.
Instances For
def
MagnitudeConjecture.Graded.principalGenerator
{A : Type u_2}
[Ring A]
(e : A)
:
↥(principalProjective e)
The canonical generator of Ae.
Instances For
theorem
MagnitudeConjecture.Graded.principal_fixed
{A : Type u_2}
[Ring A]
{e : A}
(he : e * e = e)
(x : ↥(principalProjective e))
:
↑x * e = ↑x
theorem
MagnitudeConjecture.Graded.principalMap_homogeneous
{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 : A)
(he : e ∈ R.component 0)
:
(R.regularModuleGrading ⋯).Homogeneous (R.regularModuleGrading ⋯) 0 (LinearMap.toSpanSingleton A A e)
Right multiplication by a degree-zero element is homogeneous of degree zero.
def
MagnitudeConjecture.Graded.principalProjectiveGrading
{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 : A)
(he : e ∈ R.component 0)
:
The induced grading of the actual principal projective module.
Instances For
def
MagnitudeConjecture.Graded.idempotentComponent
{k : Type u_1}
{A : Type u_2}
[Field k]
[Ring A]
[Algebra k A]
(R : VectorGrading k A)
{M : Type u_3}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
(G : ModuleGrading R)
(e : A)
(d : ℤ)
:
Submodule k M
The e-coordinate of a homogeneous component.
Instances For
def
MagnitudeConjecture.Graded.principalMap
{A : Type u_2}
[Ring A]
{M : Type u_3}
[AddCommGroup M]
[Module A M]
(e : A)
(x : M)
:
↥(principalProjective e) →ₗ[A] M
A vector fixed by e determines the unique module map from Ae taking e to it.
Instances For
def
MagnitudeConjecture.Graded.principalHomEquiv
{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]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
(G : ModuleGrading R)
(e : A)
(he : e * e = e)
(he0 : e ∈ R.component 0)
(d : ℤ)
:
↥((principalProjectiveGrading R ⋯ e he0).homComponent G d) ≃ₗ[k] ↥(idempotentComponent R G e d)
Evaluation at the idempotent identifies homogeneous maps with its coordinate space.