Primitive coordinates in literal support quotients

For a primitive vertex belonging to a selected support, its image in the literal complementary-vertex quotient is nonzero and primitive. The right ideal generated by this image is therefore the actual projective coordinate in the support-algebra skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportQuotientMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : A →+* P.SupportAlgebra X

The literal quotient map, reoriented from the quotient of Aᵐᵒᵖ to a ring map from A into the right-module support algebra.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportQuotientMap_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (a : A) : (P.supportQuotientMap X) a = MulOpposite.op ((Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (P.supportIdeal X))) (MulOpposite.op a))

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportQuotientMap_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : Function.Surjective ⇑(P.supportQuotientMap X)

The support quotient map is surjective.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportIdempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) : P.SupportAlgebra X

The image in the support quotient of one ambient primitive idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportIdempotent_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : P.supportIdempotent X p ≠ 0

A primitive idempotent whose vertex belongs to the selected support has nonzero image in the literal support quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportIdempotent_eq_zero_of_not_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∉ S.projectiveSupport X) : P.supportIdempotent X p = 0

An omitted ambient primitive idempotent has zero image in the support quotient.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.SupportedProjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (X : FinitelyGeneratedCategory A) : Type

Ambient projective labels which survive in the selected support.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportedProjectiveLabelFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (X : FinitelyGeneratedCategory A) : Fintype (SupportedProjectiveLabel X)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportedIdempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : SupportedProjectiveLabel X) : P.SupportAlgebra X

The surviving complete family of primitive idempotents in the literal support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportedIdempotents_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : CompleteOrthogonalIdempotents (P.supportedIdempotent X)

The surviving quotient idempotents are still a complete orthogonal family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_idempotentCoordinate_of_mem_support {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : ∃ (x : ↥(idempotentCoordinate (P.idempotent p) X)), x ≠ 0

Membership in projective support produces a nonzero vector in the corresponding ambient idempotent coordinate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ambientToSupportLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : ↑M ≃ₗ[k] ↑(P.supportFGObj X M hsub)

Passage to the support algebra preserves the underlying k-vector space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportIdempotent_smul {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (p : S.ProjectiveLabel) (m : ↑M) : MulOpposite.op (P.supportIdempotent X p) • (P.ambientToSupportLinearEquiv X M hsub) m = (P.ambientToSupportLinearEquiv X M hsub) (MulOpposite.op (P.idempotent p) • m)

On a supported module, the quotient idempotent acts by the original ambient idempotent.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idempotentCoordinateSupportEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (p : S.ProjectiveLabel) : ↥(idempotentCoordinate (P.idempotent p) M) ≃ₗ[k] ↥(idempotentCoordinate (P.supportIdempotent X p) (P.supportFGObj X M hsub))

The ambient primitive coordinate and the corresponding coordinate in the literal support quotient are the same k-vector space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportPrimitiveIdempotentData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : PrimitiveIdempotentData (P.supportIdempotent X p)

The surviving image of an ambient primitive idempotent is primitive in the literal support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_from_supportedRightIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : SupportedProjectiveLabel X) : ∃ (f : rightIdealFGObj (P.supportIdempotent X ↑p) ⟶ P.supportFGObj X X ⋯), f ≠ 0

Every surviving primitive projective maps nontrivially to the selected support module itself.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_to_supportedPrimitiveInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : SupportedProjectiveLabel X) : ∃ (f : P.supportFGObj X X ⋯ ⟶ primitiveInjectiveFGObj (P.supportIdempotent X ↑p)), f ≠ 0

Every surviving primitive injective receives a nonzero map from the selected support module itself.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_from_supportedRightIdeal_to_supportFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (p : S.ProjectiveLabel) (hpX : p ∈ S.projectiveSupport X) (hpM : p ∈ S.projectiveSupport M) : ∃ (f : rightIdealFGObj (P.supportedIdempotent X ⟨p, hpX⟩) ⟶ P.supportFGObj X M hsub), f ≠ 0

A surviving primitive projective maps nontrivially to any supported module on which its ambient primitive coordinate is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_from_supportFGObj_to_supportedPrimitiveInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (p : S.ProjectiveLabel) (hpX : p ∈ S.projectiveSupport X) (hpM : p ∈ S.projectiveSupport M) : ∃ (f : P.supportFGObj X M hsub ⟶ primitiveInjectiveFGObj (P.supportedIdempotent X ⟨p, hpX⟩)), f ≠ 0

A surviving primitive injective receives a nonzero map from any supported module on which its ambient primitive coordinate is nonzero.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportProjectiveCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : (P.supportAlgebraSkeleton hA X).ProjectiveLabel

The actual indecomposable-projective coordinate in the chosen support algebra skeleton attached to a supported ambient primitive vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportProjectiveHom_finrank_eq_idempotentCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : Module.finrank k ((P.supportAlgebraSkeleton hA X).fgObj (P.supportProjectiveCoordinate hA X p hp).label ⟶ (P.supportAlgebraSkeleton hA X).fgObj (P.supportLabel hA X M hsub hM)) = Module.finrank k ↥(idempotentCoordinate (P.idempotent p) M)

The Hom dimension from the selected support-projective coordinate is the ambient p-idempotent coordinate. In particular, this statement is independent of the arbitrary duplicate-free skeleton chosen for the support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportProjectiveHomVector_eq_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) (x : Fin S.n) (hsub : S.projectiveSupport (S.fgObj x) ⊆ S.projectiveSupport X) (p : S.ProjectiveLabel) (hp : p ∈ S.projectiveSupport X) : (P.supportAlgebraSkeleton hA X).projectiveHomVector (P.supportLabel hA X (S.fgObj x) hsub ⋯) (P.supportProjectiveCoordinate hA X p hp) = S.projectiveHomVector x p

A supported indecomposable has the same projective-Hom coordinate before and after passage to the literal support quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportProjectiveHomVector_eq_primitiveMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) {e : A} (D : PrimitiveIdempotentData e) (X : FinitelyGeneratedCategory A) (x : Fin S.n) (hsub : S.projectiveSupport (S.fgObj x) ⊆ S.projectiveSupport X) (hp : S.primitiveSourceProjectiveLabel D ∈ S.projectiveSupport X) : (P.supportAlgebraSkeleton hA X).projectiveHomVector (P.supportLabel hA X (S.fgObj x) hsub ⋯) (P.supportProjectiveCoordinate hA X (S.primitiveSourceProjectiveLabel D) hp) = ↑(S.primitiveMultiplicity D x)

At the ambient primitive source selected by D, the support-projective coordinate is exactly the manuscript's primitive multiplicity.