The deleted-simple socle class #
At a positive new mesh, the torsion-free quotient of the ambient Auslander--Reiten middle has a simple submodule supported at the deleted primitive idempotent. This produces the manuscript's nonzero map from the deleted simple and hence a nonzero connecting extension class.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSocleHasExt
{A : Type u}
[Ring A]
[IsNoetherianRing Aᵐᵒᵖ]
:
CategoryTheory.HasExt (FinitelyGeneratedCategory A)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.hom_primitiveSource_to_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}
(M : FinitelyGeneratedCategory A)
(hM : IsAnnihilatedBy (primitiveIdeal e) M)
(f : S.fgObj (S.primitiveSourceLabel D) ⟶ M)
:
f = 0
Maps from the primitive projective to an AeA-annihilated module are
zero.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddle_primitiveSourceHom_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Module.finrank k (S.fgObj (S.primitiveSourceLabel D) ⟶ (S.minimalRightAlmostSplitAt ↑N.label).middle) = 1
The primitive projective maps one-dimensionally to the ambient AR middle at a new endpoint.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddle_primitiveMultiplicity_sum_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
∑ i : Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n,
S.primitiveMultiplicity D ((S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).label i) = 1
In the fixed ambient decomposition of the AR middle, the sum of all primitive coordinates is one.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_unique_ambientMiddle_primitiveSummand
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
∃ (i : Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n),
∀ (j : Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n),
S.primitiveMultiplicity D ((S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).label j) = if j = i then 1 else 0
Exactly one displayed ambient middle summand has nonzero primitive coordinate, and that coordinate is one.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleIndex
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n
The unique displayed ambient middle summand carrying the deleted primitive coordinate.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleIndex_spec
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(j : Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n)
:
S.primitiveMultiplicity D ((S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).label j) = if j = exceptionalMiddleIndex B N then 1 else 0
The primitive coordinate of every displayed middle summand, relative to the exceptional index.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleLabel
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Fin S.n
The label of the unique ambient middle summand containing the deleted primitive coordinate.
Instances For
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleModule
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
The manuscript's exceptional middle summand Y.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddle_primitiveMultiplicity_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
S.primitiveMultiplicity D (exceptionalMiddleLabel B N) = 1
The exceptional summand has primitive coordinate one.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleLabel_not_mem
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
exceptionalMiddleLabel B N ∉ S.primitiveKilledLabels D
The exceptional summand is not an A/AeA-module.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddleLabel_mem_of_ne_exceptional
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(j : Fin (S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).n)
(hj : j ≠ exceptionalMiddleIndex B N)
:
(S.chosenLabelDecomposition (S.minimalRightAlmostSplitAt ↑N.label).middle).label j ∈ S.primitiveKilledLabels D
Every other displayed ambient middle summand is an A/AeA-module.
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddleComplement
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
The direct sum of all displayed ambient middle summands except the
exceptional summand Y.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddleSplitIso
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
(S.minimalRightAlmostSplitAt ↑N.label).middle ≅ ambientMiddleComplement B N ⊞ exceptionalMiddleModule B N
The selected ambient decomposition splits the AR middle as
V₀ ⊕ Y.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ambientMiddleComplement_isAnnihilatedBy
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Every summand of V₀ is an A/AeA-module, so V₀ itself is
annihilated by AeA.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionAmbientMiddleSplitIso
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
primitiveTorsionFGObj e (S.minimalRightAlmostSplitAt ↑N.label).middle ≅ ambientMiddleComplement B N ⊞ primitiveTorsionFGObj e (exceptionalMiddleModule B N)
Applying primitive torsion to the manuscript split gives
R(V) ≅ V₀ ⊕ R(Y): torsion fixes the killed complement and acts only on
the exceptional summand.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleInclusion
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
exceptionalMiddleModule B N ⟶ (S.minimalRightAlmostSplitAt ↑N.label).middle
The canonical inclusion of the exceptional summand into the selected ambient decomposition.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleInclusion_mono
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
CategoryTheory.Mono (exceptionalMiddleInclusion B N)
The exceptional summand inclusion is monic.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.hom_primitiveDeletedSimple_to_exceptionalMiddle_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
(f : S.primitiveDeletedSimple D ⟶ exceptionalMiddleModule B N)
:
f = 0
Positivity forces Hom_A(S_e,Y)=0 for the exceptional summand.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotient_nontrivial_of_sourceHom_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}
(M : FinitelyGeneratedCategory A)
(hfinrank : Module.finrank k (S.fgObj (S.primitiveSourceLabel D) ⟶ M) = 1)
:
Nontrivial ↑(primitiveTorsionQuotientFGObj e M)
A module receiving a one-dimensional Hom space from the primitive projective has nonzero primitive torsion-free quotient.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleTorsionShortComplex
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)
The exceptional summand's canonical torsion sequence
0 -> R(Y) -> Y -> T_Y -> 0.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleTorsionShortComplex_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
(exceptionalMiddleTorsionShortComplex B N).ShortExact
The exceptional summand's torsion sequence is short exact.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalMiddleTorsionQuotient_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
Nontrivial ↑(primitiveTorsionQuotientFGObj e (exceptionalMiddleModule B N))
The exceptional torsion-free quotient T_Y is nonzero.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalPositiveConnectingLinear
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
(S.primitiveDeletedSimple D ⟶ primitiveTorsionQuotientFGObj e (exceptionalMiddleModule B N)) →ₗ[k] CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) (primitiveTorsionFGObj e (exceptionalMiddleModule B N)) 1
The connecting map
Hom_A(S_e,T_Y) -> Ext¹_A(S_e,R(Y)).
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalPositiveConnectingLinear_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
Function.Injective ⇑(exceptionalPositiveConnectingLinear B N)
At a positive mesh, the exceptional-summand connecting map is injective.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotientSimpleSubmodule
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(M : FinitelyGeneratedCategory A)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
Submodule Aᵐᵒᵖ ↑(primitiveTorsionQuotientFGObj e M)
A chosen simple submodule of a nonzero primitive torsion-free quotient.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotientSimpleSubmodule_isSimpleModule
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{e : A}
(M : FinitelyGeneratedCategory A)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
IsSimpleModule Aᵐᵒᵖ ↥(primitiveTorsionQuotientSimpleSubmodule M hT)
The chosen torsion-free socle submodule is simple.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotientSimpleFGObj
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{e : A}
(M : FinitelyGeneratedCategory A)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
The chosen simple submodule, bundled as a finitely generated ambient right module.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotientSimpleFGObj_isSimpleModule
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{e : A}
(M : FinitelyGeneratedCategory A)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
IsSimpleModule Aᵐᵒᵖ ↑(primitiveTorsionQuotientSimpleFGObj M hT)
The bundled socle object remains simple.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.primitiveTorsionQuotientSimpleFGObj_not_isAnnihilatedBy
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{e : A}
(M : FinitelyGeneratedCategory A)
(he : IsIdempotentElem e)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
The chosen simple submodule cannot be an A/AeA-module, because the
torsion-free quotient has no nonzero AeA-annihilated submodule.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_nonzero_hom_primitiveDeletedSimple_to_torsionQuotient
{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}
(M : FinitelyGeneratedCategory A)
(hT : Nontrivial ↑(primitiveTorsionQuotientFGObj e M))
:
∃ (f : S.primitiveDeletedSimple D ⟶ primitiveTorsionQuotientFGObj e M), f ≠ 0
The deleted simple occurs in the socle of the torsion-free quotient:
there is a nonzero map from S_e.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalPrimitiveDeletedSocleMap
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
A fixed nonzero deleted-simple map into the exceptional torsion-free
quotient T_Y.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exceptionalPrimitiveDeletedSocleMap_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
The fixed socle map is nonzero.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveConnectingClass
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
:
CategoryTheory.Abelian.Ext (S.primitiveDeletedSimple D) (primitiveTorsionFGObj e (exceptionalMiddleModule B N)) 1
The extension class obtained by applying the torsion-sequence connecting map to the fixed deleted-simple socle map.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveConnectingClass_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
positiveConnectingClass B N ≠ 0
At a positive new mesh, the selected connecting extension class is nonzero.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_positiveConnectingSummand
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
let RY := primitiveTorsionFGObj e (exceptionalMiddleModule B N);
have c := S.chosenLabelDecomposition RY;
∃ (i : Fin c.n),
(CategoryTheory.Abelian.Ext.addEquivBiproduct (S.primitiveDeletedSimple D)
(CategoryTheory.Limits.biproduct.isBilimit fun (j : Fin c.n) => S.fgObj (c.label j)) 1)
((positiveConnectingClass B N).comp (CategoryTheory.Abelian.Ext.mk₀ c.iso.hom) ⋯) i ≠ 0
Some displayed indecomposable summand of R(Y) receives a nonzero
component of the positive connecting class.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveConnectingSummandIndex
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
Fin (S.chosenLabelDecomposition (primitiveTorsionFGObj e (exceptionalMiddleModule B N))).n
A fixed summand index of R(Y) on which the connecting class is
nonzero.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveConnectingSummand_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
let RY := primitiveTorsionFGObj e (exceptionalMiddleModule B N);
let c := S.chosenLabelDecomposition RY;
(CategoryTheory.Abelian.Ext.addEquivBiproduct (S.primitiveDeletedSimple D)
(CategoryTheory.Limits.biproduct.isBilimit fun (j : Fin c.n) => S.fgObj (c.label j)) 1)
((positiveConnectingClass B N).comp (CategoryTheory.Abelian.Ext.mk₀ c.iso.hom) ⋯)
(positiveConnectingSummandIndex B N hpositive) ≠ 0
The nonzero Ext component at the fixed summand index.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceLabel
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
The quotient label Z selected by the nonzero positive connecting
component.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceLabel_not_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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
¬CategoryTheory.Injective (S.fgObj ↑(positiveSourceLabel B N hpositive))
The selected positive source is ambient noninjective, as witnessed by its nonzero degree-one Ext component.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceNoninjectiveLabel
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
The positive pair source bundled with the noninjectivity needed to form its inverse Auslander--Reiten translate.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceLeftMarkerAmbientLabel
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
Fin S.n
The ambient label τ_A⁻¹ Z used to read the sign of the positive
gaining pair selected at a new mesh.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.exists_nonzero_positiveSourceMarker
{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)
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
∃ (f : S.fgObj (positiveSourceLeftMarkerAmbientLabel B N hpositive) ⟶ S.primitiveDeletedSimple D), f ≠ 0
The selected positive gaining-pair source has positive source marker:
there is a nonzero map τ_A⁻¹ Z ⟶ S_e.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceLabel_multiplicity_positive
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
0 < S.indecomposableMultiplicity (↑(positiveSourceLabel B N hpositive))
(primitiveTorsionFGObj e (exceptionalMiddleModule B N))
The selected label occurs with positive multiplicity in R(Y).
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.positiveSourceLabel_strict_multiplicity
{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}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(N : S.PrimitiveNewRightMeshEndpoint D)
(hpositive : N.IsPositive)
:
relativeArrowMultiplicity (positiveSourceLabel B N hpositive) N > FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData
↑(positiveSourceLabel B N hpositive) ↑N.label
At a positive new mesh, the selected quotient label occurs strictly
more often in the relative middle R(V) than in the ambient AR middle
V.