Iyama saturation through finite Nakayama evaluation

For a saturated quotient of a represented projective, the boundary representable detects every nonzero submodule. Finite Nakayama evaluation therefore embeds that quotient into finitely many copies of the boundary Nakayama module. The factor Auslander global-dimension bound then reduces projective dimension at most one for every such quotient to the single boundary estimate pd (nu U) ≤ 1.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.saturatedSubobjectAmbientQuotient_projectiveDimensionLE_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) {Y : PosetSpace.Obj k T} {X : S.FactorCategory K} (m : Y ⟶ R.representableData.obj X) : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of (S.factorAuslanderRing K) ((S.factorAdditiveGenerator K ⟶ X) ⧸ R.saturatedSubobjectImage H m)) 1

The source quotient in Iyama's saturation argument has projective dimension at most one.