Homogeneous complete idempotents in the actual standard form

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) : FiniteDimensional k (X ⟶ Y)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeAlgebra_mul_mem {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {i j : ℤ} {a b : (S.standardFormAlgebra ⋯)ᵐᵒᵖ} (ha : a ∈ (S.standardFormOppositeAlgebraGrading ⋯).component i) (hb : b ∈ (S.standardFormOppositeAlgebraGrading ⋯).component j) : a * b ∈ (S.standardFormOppositeAlgebraGrading ⋯).component (i + j)

The standard-form grading is multiplicative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeAlgebra_one_mem {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : 1 ∈ (S.standardFormOppositeAlgebraGrading ⋯).component 0

The unit of the standard-form algebra is homogeneous of degree zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormOppositeAlgebra_negative {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (d : ℤ) (hd : d < 0) : (S.standardFormOppositeAlgebraGrading ⋯).component d = ⊥

Negative degrees vanish in the actual standard-form algebra grading.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousIdempotent {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) : (S.standardFormAlgebra ⋯)ᵐᵒᵖ

The complete projective-summand idempotents transported to the standard form.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousIdempotent_mem_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) : S.standardFormHomogeneousIdempotent p ∈ (S.standardFormOppositeAlgebraGrading ⋯).component 0

Each transported idempotent has degree zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousIdempotent_idempotent {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) : S.standardFormHomogeneousIdempotent p * S.standardFormHomogeneousIdempotent p = S.standardFormHomogeneousIdempotent p

The transported elements are idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormHomogeneousIdempotent_orthogonal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Pairwise fun (p q : S.StandardFormProjectiveMeshCategory) => S.standardFormHomogeneousIdempotent p * S.standardFormHomogeneousIdempotent q = 0

The transported family is orthogonal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_standardFormHomogeneousIdempotent {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ∑ p : S.StandardFormProjectiveMeshCategory, S.standardFormHomogeneousIdempotent p = 1

The transported family is complete.