Schurian boundary bounds

Weak positivity on the support of an indecomposable projective forces the corresponding Cartan column to be thin. This gives the projective half of the schurian boundary estimate without importing a classification theorem.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.PrimitiveInjectiveCoordinateIndex {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) : Type

Coordinates indexing a finite family of maps from X to the primitive injectives selected by the complete idempotent presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveInjectiveCoordinateMap {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.PrimitiveInjectiveCoordinateIndex X) : X ⟶ primitiveInjectiveFGObj (P.idempotent a.fst)

The map to a primitive injective corresponding to one dual-basis coordinate of X e_p.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveInjectiveEmbedding {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) : X ⟶ ⨁ fun (a : P.PrimitiveInjectiveCoordinateIndex X) => primitiveInjectiveFGObj (P.idempotent a.fst)

The finite family of all primitive-injective coordinate maps.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveInjectiveEmbedding_mono {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) : CategoryTheory.Mono (P.primitiveInjectiveEmbedding X)

Completeness of the primitive idempotents makes the coordinate map a monomorphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_iso_primitiveSink {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (i : S.InjectiveLabel) : ∃ (p : S.ProjectiveLabel), Nonempty (S.fgObj i.label ≅ S.fgObj (S.primitiveSinkLabel ⋯))

Every selected indecomposable injective is one of the primitive injectives belonging to the complete idempotent presentation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHom_le_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (p q : S.ProjectiveLabel) : Module.finrank k (S.fgObj p.label ⟶ S.fgObj q.label) ≤ 1

Every Hom space between indecomposable projectives in a representation-directed representation-finite algebra has dimension at most one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveInjectiveHom_le_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) [IsAlgClosed k] (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (p q : S.ProjectiveLabel) : Module.finrank k (primitiveInjectiveFGObj (P.idempotent p) ⟶ primitiveInjectiveFGObj (P.idempotent q)) ≤ 1

Every Hom space between the literal primitive injectives has dimension at most one. Contragredient duality identifies it with the corresponding primitive-projective corner.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.injectiveHom_le_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) (i j : S.InjectiveLabel) : Module.finrank k (S.fgObj i.label ⟶ S.fgObj j.label) ≤ 1

Every Hom space between the selected indecomposable injectives has dimension at most one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.schurianBoundaryData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) : S.SchurianBoundaryData

Representation-directedness constructs the complete schurian boundary package used in Appendix A.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.multiplicityCoordinateEstimate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) : S.MultiplicityCoordinateEstimate (S.primitiveMultiplicityInput D)

The literal support quotients and the schurian corner theorem construct the numerical coordinate estimate required by the primitive deletion.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveDirectedBoundaryData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D)

The representation-directed hypotheses construct the complete boundary data used by the primitive projective-poset realization.