The replacement projective after socle rejection #
For a non-simple primitive projective-injective eA, this file realizes
eA / soc(eA) as an indecomposable projective over the literal quotient
algebra A / soc(eA). Projectivity is proved directly in the annihilated
ambient full subcategory; indecomposability follows from preservation of the
simple top.
@[reducible, inline]
abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientFGObj
{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)
:
The literal ambient module e_p A / soc(e_p A).
Instances For
@[reducible, inline]
abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientProjection
{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)
:
The canonical quotient map e_p A → e_p A / soc(e_p A).
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientProjection_epi
{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)
:
CategoryTheory.Epi (P.primitiveProjectiveSocleQuotientProjection p)
The quotient map to e_p A / soc(e_p A) is epic.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientProjection_isLeftAlmostSplit
{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))
:
The canonical quotient is the minimal left almost-split map out of the selected primitive projective-injective.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientProjection_isLeftMinimal
{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)
:
The canonical quotient map is left minimal.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotient_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))
:
IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) (P.primitiveProjectiveSocleQuotientFGObj p)
The embedded socle ideal annihilates the quotient
e_p A / soc(e_p A).
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientObj
{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))
:
IdealQuotientSubcategory (P.primitiveProjectiveSocleIdeal p hpInjective)
The replacement quotient, bundled in the full ambient subcategory annihilated by the embedded socle ideal.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientObj_projective
{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))
:
CategoryTheory.Projective (P.primitiveProjectiveSocleQuotientObj p hpInjective)
The replacement quotient is projective in the full subcategory of ambient modules annihilated by the embedded socle ideal.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjective_top_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 : S.ProjectiveLabel)
:
IsSimpleModule Aᵐᵒᵖ (↑(rightIdealFGObj (P.idempotent p)) ⧸ Module.jacobson Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p)))
The literal primitive right ideal has simple top.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjective_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 : S.ProjectiveLabel)
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
¬IsSimpleModule Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p))
Non-simplicity of the selected skeletal projective is equivalent in the direction needed for its literal primitive-right-ideal realization.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjective_moduleSocle_le_jacobson
{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)
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
moduleSocle Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p)) ≤ Module.jacobson Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p))
For a non-simple selected projective, its socle is contained in its module Jacobson radical.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotient_top_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 : S.ProjectiveLabel)
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
IsSimpleModule Aᵐᵒᵖ
(↑(P.primitiveProjectiveSocleQuotientFGObj p) ⧸ Module.jacobson Aᵐᵒᵖ ↑(P.primitiveProjectiveSocleQuotientFGObj p))
The replacement quotient retains the simple top of the selected primitive projective.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotient_isIndecomposableModule
{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)
(hnotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label))
:
If the selected projective is non-simple, e_p A / soc(e_p A) is
indecomposable as an ambient right A-module.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientAlgebraFGObj
{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))
:
FinitelyGeneratedCategory (idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))
The replacement module, transported to a literal right module over
A / soc(e_p A).
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientAlgebraFGObj_projective
{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))
:
CategoryTheory.Projective (P.primitiveProjectiveSocleQuotientAlgebraFGObj p hpInjective)
The transported replacement is projective over the literal socle quotient algebra.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientAlgebraFGObj_isIndecomposableModule
{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))
:
QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule
(idealQuotientAlgebra (P.primitiveProjectiveSocleIdeal p hpInjective))ᵐᵒᵖ
↑(P.primitiveProjectiveSocleQuotientAlgebraFGObj p hpInjective)
If the selected projective is non-simple, the transported replacement is indecomposable over the literal socle quotient algebra.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel
{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
e_p A / soc(e_p A).
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientReplacementIso
{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.primitiveProjectiveSocleQuotientAlgebraFGObj p hpInjective ≅ S.idealQuotientFGObj (P.primitiveProjectiveSocleIdeal p hpInjective)
(P.socleQuotientReplacementLabel p hpInjective hnotSimple)
The replacement module is isomorphic to its chosen intrinsic quotient skeleton representative.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel_projective
{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.Projective
(S.idealQuotientFGObj (P.primitiveProjectiveSocleIdeal p hpInjective)
(P.socleQuotientReplacementLabel p hpInjective hnotSimple))
The replacement quotient-skeleton representative is projective.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel_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))
:
↑(P.socleQuotientReplacementLabel p hpInjective hnotSimple) ≠ p.label
The replacement label is not the rejected projective label.