Directed boundary vanishings in middle-support quotients

This file formalizes the two directed-triangle vanishings used in the manuscript's Ringel support argument. All modules and morphisms live in the literal quotient supported on the middle term of the chosen almost-split sequence.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.leftRegularFGObj {B : Type u} [Ring B] : FGModuleCat B

The regular left module as a literal finitely generated object.

def MagnitudeConjecture.RightModule.leftIdealInclusion {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) : leftIdealFGObj e ⟶ leftRegularFGObj

The literal inclusion Be → B of left ideals.

def MagnitudeConjecture.RightModule.leftIdealProjection {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) : leftRegularFGObj ⟶ leftIdealFGObj e

Right multiplication by e, as the projection B → Be of left ideals.

@[simp]

theorem MagnitudeConjecture.RightModule.leftIdealInclusion_apply_val {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) (y : ↑(leftIdealFGObj e)) : (ModuleCat.Hom.hom (leftIdealInclusion e).hom) y = ↑y

@[simp]

theorem MagnitudeConjecture.RightModule.leftIdealProjection_apply_val {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) (y : ↑leftRegularFGObj) : ↑((ModuleCat.Hom.hom (leftIdealProjection e).hom) y) = y * e

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.injectiveCogeneratorFGObj {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] : FinitelyGeneratedCategory B

The standard injective cogenerator D(B).

def MagnitudeConjecture.RightModule.primitiveInjectiveInclusion {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) : primitiveInjectiveFGObj e ⟶ injectiveCogeneratorFGObj

Dualizing B → Be gives the canonical inclusion D(Be) → D(B).

def MagnitudeConjecture.RightModule.primitiveInjectiveProjection {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) : injectiveCogeneratorFGObj ⟶ primitiveInjectiveFGObj e

Dualizing Be → B gives the canonical projection D(B) → D(Be).

@[simp]

theorem MagnitudeConjecture.RightModule.primitiveInjectiveProjection_comp_inclusion_apply {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : B) (φ : ↑injectiveCogeneratorFGObj) (b : B) : ((QuotientSubmoduleEquidistribution.Contragredient.forwardInnerDualEquiv k B leftRegularFGObj) ((ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (primitiveInjectiveProjection e) (primitiveInjectiveInclusion e)).hom) φ)) b = ((QuotientSubmoduleEquidistribution.Contragredient.forwardInnerDualEquiv k B leftRegularFGObj) φ) (b * e)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportRegularDecompositionMap {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) : rightRegularFGObj ⟶ ⨁ fun (p : SupportedProjectiveLabel X) => rightIdealFGObj (P.supportedIdempotent X p)

Decompose the regular support module into the right ideals belonging to the surviving primitive idempotents.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportRegularAssemblyMap {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) : (⨁ fun (p : SupportedProjectiveLabel X) => rightIdealFGObj (P.supportedIdempotent X p)) ⟶ rightRegularFGObj

Assemble the supported primitive right ideals back into the regular support module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportRegularDecompositionMap_comp_assemblyMap {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.CategoryStruct.comp (P.supportRegularDecompositionMap X) (P.supportRegularAssemblyMap X) = CategoryTheory.CategoryStruct.id rightRegularFGObj

Completeness of the quotient idempotents makes regular decomposition followed by assembly the identity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportRegularDecompositionMap_isSplitMono {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.IsSplitMono (P.supportRegularDecompositionMap X)

The regular decomposition map is split monic.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInjectiveAssemblyMap {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) : (⨁ fun (p : SupportedProjectiveLabel X) => primitiveInjectiveFGObj (P.supportedIdempotent X p)) ⟶ injectiveCogeneratorFGObj

Assemble the primitive injectives belonging to the surviving quotient idempotents into the standard injective cogenerator D(B).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInjectiveDecompositionMap {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) : injectiveCogeneratorFGObj ⟶ ⨁ fun (p : SupportedProjectiveLabel X) => primitiveInjectiveFGObj (P.supportedIdempotent X p)

Restrict a functional on the support algebra to all primitive left ideals.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInjectiveDecompositionMap_comp_assemblyMap {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.CategoryStruct.comp (P.supportInjectiveDecompositionMap X) (P.supportInjectiveAssemblyMap X) = CategoryTheory.CategoryStruct.id injectiveCogeneratorFGObj

Restriction followed by assembly is the identity on D(B).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportInjectiveAssemblyMap_isSplitEpi {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.IsSplitEpi (P.supportInjectiveAssemblyMap X)

Assembly of the surviving primitive injectives is split epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMap_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.Epi (rightSequenceSupportMap z)

The ambient epimorphism remains epic after restriction to the full middle-support subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSkeletonMap_epi {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.Epi (P.rightSequenceSupportSkeletonMap hA z)

The transported middle-support almost-split map is still epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportTarget_not_projective {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : ¬CategoryTheory.Projective ((P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).almostSplitSkeleton.obj (P.rightSequenceSupportTargetLabel hA z))

The endpoint remains nonprojective in the literal middle-support quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_from_supportProjective_to_rightMiddle {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (p : SupportedProjectiveLabel (S.minimalRightAlmostSplitAt ↑z).middle) : ∃ (f : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.supportProjectiveCoordinate hA (S.minimalRightAlmostSplitAt ↑z).middle ↑p ⋯).label ⟶ (P.rightSequenceSupportMinimalRightAlmostSplitDecomposition hA z).middle), f ≠ 0

Every supported primitive-projective skeleton object maps nontrivially to the actual middle object of the transported sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_ne_zero_hom_from_rightMiddle_to_supportInjective {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (p : SupportedProjectiveLabel (S.minimalRightAlmostSplitAt ↑z).middle) : ∃ (f : (P.rightSequenceSupportMinimalRightAlmostSplitDecomposition hA z).middle ⟶ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj ((P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).primitiveSinkLabel ⋯)), f ≠ 0

The actual middle object maps nontrivially to every supported primitive-injective skeleton object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hom_from_rightTarget_to_supportProjective_eq_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) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (p : SupportedProjectiveLabel (S.minimalRightAlmostSplitAt ↑z).middle) (q : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportTargetLabel hA z) ⟶ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.supportProjectiveCoordinate hA (S.minimalRightAlmostSplitAt ↑z).middle ↑p ⋯).label) : q = 0

The supported endpoint has no nonzero map to any surviving primitive projective. A hypothetical map closes a directed triangle with one irreducible component of the transported right almost-split map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hom_from_rightTarget_to_supportRegular_eq_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) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (q : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportTargetLabel hA z) ⟶ rightRegularFGObj) : q = 0

The supported endpoint has no nonzero map to the regular support module. This is the finite aggregation of the primitive-projective vanishing over the complete quotient idempotent family.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernelLabel {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Fin (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).n

The support-skeleton label selected for the kernel of the transported right almost-split map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportKernelIso {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : CategoryTheory.Limits.kernel (P.rightSequenceSupportMinimalRightAlmostSplitDecomposition hA z).map ≅ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).almostSplitSkeleton.obj (P.rightSequenceSupportKernelLabel hA z)

The kernel is represented by its selected support-skeleton label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMinimalLeftAlmostSplitDecomposition {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) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).almostSplitSkeleton.MinimalLeftAlmostSplitDecomposition (P.rightSequenceSupportKernelLabel hA z)

The kernel inclusion, transported to its selected skeleton object and equipped with the actual middle decomposition, is minimal left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hom_from_supportInjective_to_rightKernel_eq_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) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (p : SupportedProjectiveLabel (S.minimalRightAlmostSplitAt ↑z).middle) (q : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj ((P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).primitiveSinkLabel ⋯) ⟶ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportKernelLabel hA z)) : q = 0

No surviving primitive injective maps nontrivially to the kernel of the transported sequence. A hypothetical map closes a directed triangle with one irreducible component of the kernel's minimal left almost-split map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.hom_from_supportInjectiveCogenerator_to_rightKernel_eq_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) (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (q : injectiveCogeneratorFGObj ⟶ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportKernelLabel hA z)) : q = 0

The injective cogenerator of the support algebra has no nonzero map to the kernel. This is the finite aggregation of the primitive-injective vanishing over the complete quotient idempotent family.