Finite ideal lattices and primitive-projective Hom chains

For a complete primitive-projective presentation, endpoint-stable subspaces of a concrete corner Hom space embed into the ambient two-sided ideal lattice. The remainder of the Jans pencil argument will use this finiteness together with the residue characters of the local endpoint endomorphism rings.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdealCorner {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (I : TwoSidedIdeal A) (p q : P.PrimitiveCornerCategory) : Submodule k (p ⟶ q)

The selected corner of an ambient two-sided ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdealCorner_isHomSubbimodule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (I : TwoSidedIdeal A) (p q : P.PrimitiveCornerCategory) : IsHomSubbimodule (P.finiteIdealCorner I p q)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdealHomSpan {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : P.PrimitiveCornerCategory} (T : Submodule k (p ⟶ q)) : TwoSidedIdeal A

The ambient ideal generated by an endpoint-stable Hom subspace.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdealCorner_homSpan_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : P.PrimitiveCornerCategory} (T : Submodule k (p ⟶ q)) (hT : IsHomSubbimodule T) : P.finiteIdealCorner (P.finiteIdealHomSpan T) p q = T

Generating an ambient ideal and taking the original corner recovers an endpoint-stable Hom subspace exactly.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finiteIdeal_homSubbimodule_comparable {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) {p q : P.PrimitiveCornerCategory} (T U : Submodule k (p ⟶ q)) (hT : IsHomSubbimodule T) (hU : IsHomSubbimodule U) : T ≤ U ∨ U ≤ T

Representation-finiteness forces every pair of endpoint-stable subspaces of a concrete primitive-projective Hom space to be comparable.