Directedness of literal support quotients

The module category of a support quotient is equivalent to the full ambient subcategory on the selected vertices. This file uses that equivalence to send each indecomposable of a support-algebra skeleton back to its unique ambient skeleton label. Nonzero nonisomorphisms remain nonzero nonisomorphisms, so ambient representation-directedness descends to the literal support quotient.

No support corner or compatibility presentation is introduced.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInflationFunctor {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.Functor (FinitelyGeneratedCategory (P.SupportAlgebra X)) (FinitelyGeneratedCategory A)

Inflate right modules over a literal support algebra to ambient right modules, through the support-subcategory equivalence.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInflationFunctorFaithful {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.supportInflationFunctor X).Faithful

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInflationFunctorAdditive {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.supportInflationFunctor X).Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInflationFunctorReflectsIsomorphisms {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.supportInflationFunctor X).ReflectsIsomorphisms

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientFGObj {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) (i : Fin (P.supportAlgebraSkeleton hA X).n) : FinitelyGeneratedCategory A

The ambient module represented by one label of the chosen support-algebra skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientFGObj_indecomposable {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) (i : Fin (P.supportAlgebraSkeleton hA X).n) : CategoryTheory.Indecomposable (P.supportSkeletonAmbientFGObj hA X i)

Inflation of a chosen support-algebra indecomposable remains indecomposable in the ambient finitely generated module category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientLabel {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) (i : Fin (P.supportAlgebraSkeleton hA X).n) : Fin S.n

The unique ambient skeleton label represented by a support-algebra skeleton object after inflation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientIso {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) (i : Fin (P.supportAlgebraSkeleton hA X).n) : P.supportSkeletonAmbientFGObj hA X i ≅ S.fgObj (P.supportSkeletonAmbientLabel hA X i)

The selected ambient label represents the inflated support-algebra object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientMap {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) {i j : Fin (P.supportAlgebraSkeleton hA X).n} (f : (P.supportAlgebraSkeleton hA X).fgObj i ⟶ (P.supportAlgebraSkeleton hA X).fgObj j) : S.fgObj (P.supportSkeletonAmbientLabel hA X i) ⟶ S.fgObj (P.supportSkeletonAmbientLabel hA X j)

A morphism between support-skeleton representatives, inflated and conjugated to the corresponding ambient skeleton representatives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientMap_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) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) {i j : Fin (P.supportAlgebraSkeleton hA X).n} {f : (P.supportAlgebraSkeleton hA X).fgObj i ⟶ (P.supportAlgebraSkeleton hA X).fgObj j} (hf : f ≠ 0) : P.supportSkeletonAmbientMap hA X f ≠ 0

Inflation and conjugation preserve nonzero morphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSkeletonAmbientMap_not_isIso {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) {i j : Fin (P.supportAlgebraSkeleton hA X).n} {f : (P.supportAlgebraSkeleton hA X).fgObj i ⟶ (P.supportAlgebraSkeleton hA X).fgObj j} (hf : ¬CategoryTheory.IsIso f) : ¬CategoryTheory.IsIso (P.supportSkeletonAmbientMap hA X f)

Inflation and conjugation reflect isomorphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportNonzeroNonisomorphism_to_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) {i j : Fin (P.supportAlgebraSkeleton hA X).n} (h : (P.supportAlgebraSkeleton hA X).NonzeroNonisomorphism i j) : S.NonzeroNonisomorphism (P.supportSkeletonAmbientLabel hA X i) (P.supportSkeletonAmbientLabel hA X j)

Each nonzero nonisomorphism in the support skeleton gives one in the ambient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportNonzeroNonisomorphism_transGen_to_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) {i j : Fin (P.supportAlgebraSkeleton hA X).n} (h : Relation.TransGen (P.supportAlgebraSkeleton hA X).NonzeroNonisomorphism i j) : Relation.TransGen S.NonzeroNonisomorphism (P.supportSkeletonAmbientLabel hA X i) (P.supportSkeletonAmbientLabel hA X j)

A path of nonzero nonisomorphisms in the support skeleton inflates to such a path in the ambient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportAlgebraSkeleton_hasAcyclicNonzeroNonisomorphisms {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) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) : (P.supportAlgebraSkeleton hA X).HasAcyclicNonzeroNonisomorphisms

Representation-directedness descends to every literal support quotient.