Socle rejection at a projective-injective module #
Besides making P / soc(P) projective, rejection of the embedded socle of a
non-simple indecomposable projective-injective P makes rad(P) injective.
This file proves that assertion first in the full ambient subcategory
annihilated by the socle ideal and then transports it to the literal quotient
algebra.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFiniteTauCategoryData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(I : TwoSidedIdeal A)
[IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ]
:
The finite tau-category of the literal quotient by an arbitrary ideal, with Noetherianity discharged from finite dimensionality.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalRightAlmostSplitAtDecomposition
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x : Fin S.n)
:
The chosen ambient minimal right almost-split decomposition, reindexed by a finite ordinal.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveInjective_rightMiddleArity_eq_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(p : S.ProjectiveLabel)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
A non-simple projective-injective vertex has exactly one incoming right-middle occurrence.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.minimalRightAlmostSplitAt_label_ne_projectiveInjective_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(x : Fin S.n)
(hx : x ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
(t : (S.minimalRightAlmostSplitAt x).index.obj)
:
(S.minimalRightAlmostSplitAt x).label t ≠ p.label
Away from P / soc(P), the ambient minimal right almost-split middle
term contains no copy of the rejected projective-injective P.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.minimalRightAlmostSplitAt_middle_isAnnihilatedBy_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(x : Fin S.n)
(hx : x ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
:
IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) (S.minimalRightAlmostSplitAt x).middle
Away from the exceptional endpoint P / soc(P), the entire ambient
minimal right almost-split middle term is already a module over the socle
quotient.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientLabelObj_projective_iff_ambient_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(x : S.IdealQuotientLabel (P.primitiveProjectiveSocleIdeal p hpInjective))
(hx : ↑x ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
:
CategoryTheory.Projective (S.idealQuotientLabelObj (P.primitiveProjectiveSocleIdeal p hpInjective) x) ↔ CategoryTheory.Projective (S.fgObj ↑x)
At every surviving endpoint other than P / soc(P), projectivity in
the annihilated full subcategory is equivalent to ambient projectivity.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFGObj_projective_iff_ambient_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(x : S.IdealQuotientLabel (P.primitiveProjectiveSocleIdeal p hpInjective))
(hx : ↑x ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
:
CategoryTheory.Projective (S.idealQuotientFGObj (P.primitiveProjectiveSocleIdeal p hpInjective) x) ↔ CategoryTheory.Projective (S.fgObj ↑x)
The same ordinary-vertex projectivity comparison over the literal socle quotient algebra.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientSurvivingEquiv
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
:
S.IdealQuotientLabel (P.primitiveProjectiveSocleIdeal p hpInjective) ≃ { i : Fin S.n // i ≠ p.label }
Intrinsic socle-quotient labels are exactly the ambient labels other than the rejected projective-injective label.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteSurvivingEquiv
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
:
Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).n ≃ { i : Fin S.n // i ≠ p.label }
The finite-ordinal quotient labels are equivalent to the ambient labels surviving rejection.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteSurvivorLabel
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(i : Fin S.n)
(hi : i ≠ p.label)
:
Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).n
The finite quotient-skeleton label corresponding to an ambient label other than the rejected projective-injective.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteSurvivingEquiv_survivorLabel
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(i : Fin S.n)
(hi : i ≠ p.label)
:
(P.socleQuotientFiniteSurvivingEquiv p hpInjective) (P.socleQuotientFiniteSurvivorLabel p hpInjective i hi) = ⟨i, hi⟩
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteSurvivorIso
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(i : Fin S.n)
(hi : i ≠ p.label)
:
(S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).fgObj
(P.socleQuotientFiniteSurvivorLabel p hpInjective i hi) ≅ (idealQuotientEquivalence (P.primitiveProjectiveSocleIdeal p hpInjective)).functor.obj
(S.idealQuotientLabelObj (P.primitiveProjectiveSocleIdeal p hpInjective) ⟨i, ⋯⟩)
The finite quotient representative of a surviving ambient label is the literal quotient module obtained from that ambient object.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_other_projectiveInjective
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(p q : S.ProjectiveLabel)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hq : q.label ≠ p.label)
(hqInjective : CategoryTheory.Injective (S.fgObj q.label))
:
CategoryTheory.Projective
((S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).fgObj
(P.socleQuotientFiniteSurvivorLabel p hpInjective q.label hq)) ∧ CategoryTheory.Injective
((S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).fgObj
(P.socleQuotientFiniteSurvivorLabel p hpInjective q.label hq))
Every other projective-injective vertex remains projective-injective
after rejecting the socle of p.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_other_not_isSimpleModule
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(p q : S.ProjectiveLabel)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hq : q.label ≠ p.label)
(hqNotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj q.label))
:
¬IsSimpleModule (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ
↑((S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).fgObj
(P.socleQuotientFiniteSurvivorLabel p hpInjective q.label hq))
A distinct ambient nonsimple projective-injective remains nonsimple as a module over the one-step socle quotient.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteReplacementLabel
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).n
The replacement vertex in the finite-ordinal quotient skeleton.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idealQuotientFiniteLabelEquiv_socleQuotientFiniteReplacementLabel
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
(S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective))
(P.socleQuotientFiniteReplacementLabel p hpInjective hnotSimple) = P.socleQuotientReplacementLabel p hpInjective hnotSimple
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteReplacement_ambient_not_isProjective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
¬S.finiteTauCategoryData.IsProjective
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective))
(P.socleQuotientFiniteReplacementLabel p hpInjective hnotSimple))
The replacement vertex is nonprojective in the ambient finite-tau presentation.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientFiniteReplacement_isProjective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
(S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleIdeal p hpInjective)).IsProjective
(P.socleQuotientFiniteReplacementLabel p hpInjective hnotSimple)
The replacement vertex is projective in the rejected finite-tau presentation.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_isProjective_iff_ambient_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).n)
(hj :
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective)) j) ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
:
S.finiteTauCategoryData.IsProjective
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective)) j) ↔ (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleIdeal p hpInjective)).IsProjective j
In the finite-tau presentations, projectivity is unchanged at every ordinary surviving endpoint.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_rightMiddleArity_eq_ambient_of_endpoint_ne
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
(j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleIdeal p hpInjective)).n)
(hj :
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective)) j) ≠ ↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
:
FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective)) j) = FiniteTauMatrix.rightMiddleArity
(S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleIdeal p hpInjective)).toFiniteRightTauCategoryData
j
Every ordinary surviving endpoint has the same incoming right-mesh arity before and after rejection of the projective-injective socle.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadical_not_injective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
¬CategoryTheory.Injective (S.projectiveBoundaryRadical p.label)
The radical boundary object is not injective in the ambient module category.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadical_isAnnihilatedBy
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) (S.projectiveBoundaryRadical p.label)
The embedded socle ideal annihilates the radical boundary object.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idealTorsionFGObj_projectiveInjectiveIsoRadical
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
idealTorsionFGObj (P.primitiveProjectiveSocleIdeal p hpInjective) (S.fgObj p.label) ≅ S.projectiveBoundaryRadical p.label
The maximal submodule of the rejected projective-injective annihilated by its embedded socle ideal is its Jacobson radical.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientExceptionalSourceDecomposition
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
CategoryTheory.FiniteIndecomposableDecomposition
((idealQuotientEquivalence (P.primitiveProjectiveSocleIdeal p hpInjective)).functor.obj
(idealTorsionSubcategoryObj (P.primitiveProjectiveSocleIdeal p hpInjective)
(S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p hpInjective hnotSimple)).middle))
The restricted source at the exceptional endpoint has a displayed
indecomposable decomposition with the same number of terms as the ambient
right almost-split middle term. The rejected summand becomes rad(P);
every other summand is already annihilated by the socle ideal.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalObj
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
IdealQuotientSubcategory (P.primitiveProjectiveSocleIdeal p hpInjective)
The radical boundary object bundled in the full annihilated subcategory.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalObj_injective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
CategoryTheory.Injective (P.projectiveInjectiveBoundaryRadicalObj p hpInjective hnotSimple)
After socle rejection, rad(P) is injective in the annihilated ambient
full subcategory.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalAlgebraFGObj
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
FinitelyGeneratedCategory (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))
The literal quotient-algebra module corresponding to rad(P).
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalAlgebraFGObj_injective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
CategoryTheory.Injective (P.projectiveInjectiveBoundaryRadicalAlgebraFGObj p hpInjective hnotSimple)
The transported radical boundary module is injective over the literal socle quotient algebra.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientRadicalLabel
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
S.IdealQuotientLabel (P.primitiveProjectiveSocleIdeal p hpInjective)
The intrinsic quotient-skeleton label represented by rad(P).
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalReplacementIso
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
P.projectiveInjectiveBoundaryRadicalAlgebraFGObj p hpInjective hnotSimple ≅ S.idealQuotientFGObj (P.primitiveProjectiveSocleIdeal p hpInjective)
(P.socleQuotientRadicalLabel p hpInjective hnotSimple)
The literal transported radical is isomorphic to its intrinsic quotient-skeleton representative.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientRadicalLabel_injective
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
CategoryTheory.Injective
(S.idealQuotientFGObj (P.primitiveProjectiveSocleIdeal p hpInjective)
(P.socleQuotientRadicalLabel p hpInjective hnotSimple))
The intrinsic radical label is injective over the socle quotient algebra.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_replacement_rightMiddleArity_add_one_eq_ambient
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
FiniteTauMatrix.rightMiddleArity
(S.idealQuotientFiniteTauCategoryData
(P.primitiveProjectiveSocleIdeal p hpInjective)).toFiniteRightTauCategoryData
(P.socleQuotientFiniteReplacementLabel p hpInjective hnotSimple) + 1 = FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData
↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleIdeal p hpInjective))
(P.socleQuotientFiniteReplacementLabel p hpInjective hnotSimple))
At the exceptional endpoint P / soc(P), socle rejection removes
exactly one indecomposable occurrence from the incoming right mesh.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientRejectionProfile
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
The complete finite-tau rejection profile produced by removing the socle of one non-simple indecomposable projective-injective module.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotient_eulerMagnitude_eq
{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)
(hpInjective : CategoryTheory.Injective (S.fgObj p.label))
[IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ]
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
ARCount.eulerMagnitude (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData)
S.finiteTauCategoryData.IsProjective = ARCount.eulerMagnitude
(FiniteTauMatrix.arrowMultiplicity
(S.idealQuotientFiniteTauCategoryData
(P.primitiveProjectiveSocleIdeal p hpInjective)).toFiniteRightTauCategoryData)
(S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleIdeal p hpInjective)).IsProjective
Removing the socle of one non-simple indecomposable projective-injective preserves the finite Auslander--Reiten Euler magnitude.