Projective count under primitive deletion

For a complete primitive-projective presentation of a directed basic algebra, the images of all primitive idempotents except the deleted one form a complete primitive family in A / AeA. This file identifies that family with the indecomposable projectives in the literal primitive-quotient skeleton and deduces the one-projective drop used by the manuscript's direct mesh count.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientNoetherian {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : IsNoetherianRing (primitiveQuotientAlgebra (P.idempotent p))ᵐᵒᵖ

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.PrimitiveSurvivingProjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (_P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : Type

The primitive-projective labels other than the deleted label.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientIdempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : primitiveQuotientAlgebra (P.idempotent p)

The image of a surviving primitive idempotent in A / Ae_p A.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientIdempotent_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) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : P.primitiveQuotientIdempotent p q ≠ 0

A primitive idempotent distinct from the deleted one has nonzero image in the primitive quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientIdempotents_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : CompleteOrthogonalIdempotents (P.primitiveQuotientIdempotent p)

The surviving quotient idempotents are complete and orthogonal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientPrimitiveIdempotentData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : PrimitiveIdempotentData (P.primitiveQuotientIdempotent p q)

Every surviving quotient idempotent is primitive.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.PrimitiveQuotientFGProjectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P₀ : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : Type

Projective labels in the quotient-module realization of the literal surviving ambient skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveCoordinateLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : S.PrimitiveQuotientLabel ⋯

The quotient-skeleton label representing a surviving primitive right ideal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveCoordinateIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : rightIdealFGObj (P.primitiveQuotientIdempotent p q) ≅ S.primitiveQuotientFGObj ⋯ (P.primitiveQuotientProjectiveCoordinateLabel p q)

The chosen quotient coordinate represents the corresponding primitive right ideal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (q : P.PrimitiveSurvivingProjectiveLabel p) : P.PrimitiveQuotientFGProjectiveLabel p

A surviving primitive idempotent determines an indecomposable projective label of the primitive quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveCoordinate_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : Function.Surjective (P.primitiveQuotientProjectiveCoordinate p)

The surviving primitive idempotents exhaust all indecomposable projectives in the quotient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ambient_projective_hom_of_primitiveQuotient_hom_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) (p : S.ProjectiveLabel) (q r : P.PrimitiveSurvivingProjectiveLabel p) (f : rightIdealFGObj (P.primitiveQuotientIdempotent p q) ⟶ rightIdealFGObj (P.primitiveQuotientIdempotent p r)) (hf : f ≠ 0) : ∃ (g : S.fgObj (↑q).label ⟶ S.fgObj (↑r).label), g ≠ 0

A nonzero map between surviving primitive right ideals after quotienting lifts to a nonzero map between the corresponding ambient projectives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveCoordinate_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.ProjectiveLabel) : Function.Injective (P.primitiveQuotientProjectiveCoordinate p)

Directedness prevents two distinct surviving primitive projectives from becoming isomorphic in the primitive quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientProjectiveEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.ProjectiveLabel) : P.PrimitiveSurvivingProjectiveLabel p ≃ P.PrimitiveQuotientFGProjectiveLabel p

Surviving ambient primitive labels are exactly the indecomposable projectives of the quotient-module skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveQuotientFGProjectiveEquivSubcategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : P.PrimitiveQuotientFGProjectiveLabel p ≃ { x : S.PrimitiveQuotientLabel ⋯ // CategoryTheory.Projective (S.primitiveQuotientLabelObj ⋯ x) }

Projectivity in the quotient-module realization is equivalent to projectivity in the annihilated full subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.card_ambientProjective_eq_primitiveQuotientProjective_add_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.ProjectiveLabel) : Nat.card { x : Fin S.n // CategoryTheory.Projective (S.fgObj x) } = Nat.card { x : S.PrimitiveQuotientLabel ⋯ // CategoryTheory.Projective (S.primitiveQuotientLabelObj ⋯ x) } + 1

Deleting one chosen primitive idempotent removes exactly one indecomposable projective from the quotient.