Complementarity of primitive new-mesh markers #
For a primitive new right mesh, this file proves that the deleted simple is a quotient of the ambient left marker exactly when it is not a subobject of the ambient right marker. The proof uses the Hoshino torsion sequence and stable Auslander--Reiten duality directly.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.markerPositiveHasExt
{A : Type u}
[Ring A]
[IsNoetherianRing Aᵐᵒᵖ]
:
CategoryTheory.HasExt (FinitelyGeneratedCategory A)
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.HasComplementaryMarkers
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
:
The manuscript's marker-complement statement for a new quotient mesh:
the deleted simple is a quotient of the left marker p_M exactly when it is
not a subobject of the right marker q_N.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.hom_leftMarker_to_primitiveSource_eq_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(f : S.fgObj ↑(leftMarker H he N) ⟶ S.fgObj (S.primitiveSourceLabel D))
:
f = 0
No map from the left marker can point back to the distinguished primitive projective.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.projectiveStableClass_leftMarker_to_deletedSimple_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(f : S.fgObj ↑(leftMarker H he N) ⟶ S.primitiveDeletedSimple D)
(hf : f ≠ 0)
:
projectiveStableClass f ≠ 0
A nonzero map from the left marker to the deleted simple remains nonzero in projective-stable Hom.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerTorsionShortComplex
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(N : S.PrimitiveNewRightMeshEndpoint D)
:
CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)
The torsion sequence of the right marker q_N.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerTorsionShortComplex_shortExact
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(N : S.PrimitiveNewRightMeshEndpoint D)
:
N.rightMarkerTorsionShortComplex.ShortExact
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerTorsionQuotient_nontrivial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Nontrivial ↑(primitiveTorsionQuotientFGObj e (S.fgObj ↑N.rightMarker))
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPositiveConnectingLinear
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(N : S.PrimitiveNewRightMeshEndpoint D)
:
(S.primitiveDeletedSimple D ⟶ primitiveTorsionQuotientFGObj e (S.fgObj ↑N.rightMarker)) →ₗ[k] CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) N.sourceModule 1
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPositiveConnectingLinear_injective
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
Function.Injective ⇑N.rightMarkerPositiveConnectingLinear
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.extOne_deletedSimple_rightMarker_subsingleton
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Subsingleton
(CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) (S.fgObj (S.rightTranslationLabel N.ambientLabel)) 1)
Degree-one extensions from the deleted simple into the ambient right marker vanish.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPositiveConnectingLinear_surjective
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Function.Surjective ⇑N.rightMarkerPositiveConnectingLinear
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.deletedSimple_rightMarkerTorsionQuotient_finrank_eq_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Module.finrank k (S.primitiveDeletedSimple D ⟶ primitiveTorsionQuotientFGObj e (S.fgObj ↑N.rightMarker)) = 1
The deleted-simple socle of the torsion-free quotient of q_N is
one-dimensional.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPrimitiveDeletedSocleMap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
S.primitiveDeletedSimple D ⟶ primitiveTorsionQuotientFGObj e (S.fgObj ↑N.rightMarker)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPrimitiveDeletedSocleMap_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPositiveConnectingClass
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) N.sourceModule 1
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.rightMarkerPositiveConnectingClass_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_leftMarker_to_deletedSimple_of_isPositive
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
∃ (f : S.fgObj ↑(leftMarker H he N) ⟶ S.primitiveDeletedSimple D), f ≠ 0
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_nonzero_extOne_deletedSimple_sourceModule_of_leftMarker
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(f : S.fgObj ↑(leftMarker H he N) ⟶ S.primitiveDeletedSimple D)
(hf : f ≠ 0)
:
∃ (xi : CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) N.sourceModule 1), xi ≠ 0
A nonzero left-marker map supplies a nonzero extension of the deleted simple by the source of the relative mesh.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.comp_rightMarkerTorsionQuotientMk_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(N : S.PrimitiveNewRightMeshEndpoint D)
(g : S.primitiveDeletedSimple D ⟶ S.fgObj ↑N.rightMarker)
(hg : g ≠ 0)
:
CategoryTheory.CategoryStruct.comp g (primitiveTorsionQuotientMk e (S.fgObj ↑N.rightMarker)) ≠ 0
A nonzero map from the deleted simple into the right marker remains nonzero after passage to the torsion-free quotient.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.hasComplementaryMarkers
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
:
HasComplementaryMarkers H he N
The two manuscript marker tests are complementary.