Simultaneous socle rejection for a basic projective-injective family

This file packages the sum of the embedded socle ideals belonging to a finite basic family of indecomposable projective-injective right modules. Its first layer identifies the modules surviving the simultaneous quotient.

def MagnitudeConjecture.RightModule.rightModuleAnnihilator {A : Type u} [Ring A] (X : FinitelyGeneratedCategory A) : TwoSidedIdeal A

The two-sided annihilator in A of a right A-module represented as a left Aᵐᵒᵖ-module.

theorem MagnitudeConjecture.RightModule.isAnnihilatedBy_iff_le_rightModuleAnnihilator {A : Type u} [Ring A] (I : TwoSidedIdeal A) (X : FinitelyGeneratedCategory A) : IsAnnihilatedBy I X ↔ I ≤ rightModuleAnnihilator X

An ideal annihilates a right module exactly when it is contained in the module's two-sided annihilator.

theorem MagnitudeConjecture.RightModule.isAnnihilatedBy_iSup {A : Type u} [Ring A] {ι : Type u_1} (I : ι → TwoSidedIdeal A) (X : FinitelyGeneratedCategory A) : IsAnnihilatedBy (⨆ (i : ι), I i) X ↔ ∀ (i : ι), IsAnnihilatedBy (I i) X

A supremum of two-sided ideals annihilates a module exactly when every member of the family does.

theorem MagnitudeConjecture.RightModule.isAnnihilatedBy_of_le {A : Type u} [Ring A] {I J : TwoSidedIdeal A} (hIJ : I ≤ J) {X : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy J X) : IsAnnihilatedBy I X

Annihilation is contravariant in the ideal.

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_projective_of_le {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {I J : TwoSidedIdeal A} (hIJ : I ≤ J) (M : FinitelyGeneratedCategory A) (hMJ : IsAnnihilatedBy J M) (hMI : CategoryTheory.Projective { obj := M, property := ⋯ }) : CategoryTheory.Projective { obj := M, property := hMJ }

A projective object in the category annihilated by I remains projective in the smaller full subcategory annihilated by a larger ideal J.

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_injective_of_le {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {I J : TwoSidedIdeal A} (hIJ : I ≤ J) (M : FinitelyGeneratedCategory A) (hMJ : IsAnnihilatedBy J M) (hMI : CategoryTheory.Injective { obj := M, property := ⋯ }) : CategoryTheory.Injective { obj := M, property := hMJ }

An injective object in the category annihilated by I remains injective in the smaller full subcategory annihilated by a larger ideal J.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleQuotientMinimalProjectivePresentation {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)) : MinimalProjectivePresentation (P.primitiveProjectiveSocleQuotientFGObj p)

The projection from a selected indecomposable projective to its quotient by the socle, written with the skeletal projective as source, is its minimal projective presentation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel_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 q : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) (hqInjective : CategoryTheory.Injective (S.fgObj q.label)) (hpNotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (hqNotSimple : ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj q.label)) (hlabel : ↑(P.socleQuotientReplacementLabel p hpInjective hpNotSimple) = ↑(P.socleQuotientReplacementLabel q hqInjective hqNotSimple)) : p = q

Distinct selected projectives have distinct ambient socle-quotient replacement labels.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : TwoSidedIdeal A

The sum of the embedded socle ideals belonging to a finite basic family of indecomposable projective-injective labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleIdeal_le_familyIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : P.primitiveProjectiveSocleIdeal p ⋯ ≤ P.primitiveProjectiveSocleFamilyIdeal T hInjective

The socle ideal of each selected summand is contained in the simultaneous family ideal.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilySelectedLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (T : Finset S.ProjectiveLabel) : Finset (Fin S.n)

The ambient finite labels removed by the simultaneous quotient.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mem_primitiveProjectiveSocleFamilySelectedLabels_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (T : Finset S.ProjectiveLabel) (x : Fin S.n) : x ∈ primitiveProjectiveSocleFamilySelectedLabels T ↔ ∃ p ∈ T, p.label = x

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.card_primitiveProjectiveSocleFamilySelectedLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (T : Finset S.ProjectiveLabel) : (primitiveProjectiveSocleFamilySelectedLabels T).card = T.card

Because the selected family is basic, passing to ambient labels does not change its cardinality.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilySelectedEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (T : Finset S.ProjectiveLabel) : ↥T ≃ ↥(primitiveProjectiveSocleFamilySelectedLabels T)

The selected structured projectives are equivalent to their ambient finite labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.fgObj_isAnnihilatedBy_primitiveProjectiveSocleFamilyIdeal_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (x : Fin S.n) : IsAnnihilatedBy (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.fgObj x) ↔ ∀ p ∈ T, x ≠ p.label

An indecomposable ambient module survives the simultaneous family quotient exactly when its label is not one of the selected projectives.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilySurvivingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective) ≃ { x : Fin S.n // ∀ p ∈ T, x ≠ p.label }

Intrinsic labels of the simultaneous quotient are exactly the ambient labels outside the selected projective family.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilySurvivingLabelsEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective) ≃ { x : Fin S.n // x ∉ primitiveProjectiveSocleFamilySelectedLabels T }

The same surviving-label equivalence, stated as the complement of the finite set of selected ambient labels.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteSurvivingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).n ≃ { x : Fin S.n // x ∉ primitiveProjectiveSocleFamilySelectedLabels T }

The finite-ordinal quotient labels are equivalent to the complement of the selected ambient projective family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.card_primitiveProjectiveSocleFamilyLabel_add_card {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) : Fintype.card (S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) + T.card = S.n

Simultaneous rejection removes exactly the selected basic family of indecomposable labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientReplacementLabel_ne_familySelected {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) (q : S.ProjectiveLabel) : q ∈ T → ↑(P.socleQuotientReplacementLabel p ⋯ ⋯) ≠ q.label

The socle-quotient replacement belonging to a selected summand is not the label of any selected projective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyReplacementLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective)

The intrinsic simultaneous-quotient label represented by P / soc(P) for one selected summand P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyReplacementLabel_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : CategoryTheory.Projective (S.idealQuotientLabelObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (P.primitiveProjectiveSocleFamilyReplacementLabel T hInjective hNotSimple p hp))

Every selected replacement P / soc(P) is projective already in the full subcategory annihilated by the entire family ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyReplacementLabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) : Function.Injective fun (p : ↥T) => P.primitiveProjectiveSocleFamilyReplacementLabel T hInjective hNotSimple ↑p ⋯

The selected summands inject into the intrinsic replacement labels of the simultaneous quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyReplacementFGObj_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : CategoryTheory.Projective (S.idealQuotientFGObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (P.primitiveProjectiveSocleFamilyReplacementLabel T hInjective hNotSimple p hp))

Each selected replacement is projective over the literal simultaneous quotient algebra.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteReplacementLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).n

The finite-ordinal quotient-skeleton replacement belonging to a selected summand.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idealQuotientFiniteLabelEquiv_familyFiniteReplacementLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : (S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp) = P.primitiveProjectiveSocleFamilyReplacementLabel T hInjective hNotSimple p hp

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteReplacementIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).fgObj (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp) ≅ S.idealQuotientFGObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (P.primitiveProjectiveSocleFamilyReplacementLabel T hInjective hNotSimple p hp)

The finite quotient representative of a selected replacement is canonically isomorphic to its intrinsic quotient representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteReplacement_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : CategoryTheory.Projective ((S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).fgObj (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp))

Every finite-ordinal replacement label is projective in the simultaneous quotient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteReplacementLabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] : Function.Injective fun (p : ↥T) => P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple ↑p ⋯

The finite-ordinal replacement labels belonging to distinct selected projectives are distinct.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFiniteReplacement_ambient_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : ¬S.finiteTauCategoryData.IsProjective ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp))

A finite-ordinal replacement label is nonprojective in the ambient finite-tau category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.fgObj_not_isAnnihilatedBy_primitiveProjectiveSocleFamilyIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : ¬IsAnnihilatedBy (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.fgObj p.label)

A selected projective is not annihilated by the simultaneous family ideal containing its embedded socle ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadical_isAnnihilatedBy_family {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : IsAnnihilatedBy (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.projectiveBoundaryRadical p.label)

The radical boundary of every selected projective is annihilated by the entire simultaneous family ideal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.idealTorsionFGObj_familyProjectiveInjectiveIsoRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : idealTorsionFGObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.fgObj p.label) ≅ S.projectiveBoundaryRadical p.label

Under simultaneous rejection, the maximal annihilated submodule of a selected projective is still its Jacobson radical.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalFamilyObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : IdealQuotientSubcategory (P.primitiveProjectiveSocleFamilyIdeal T hInjective)

The radical boundary of a selected summand, bundled in the full subcategory annihilated by the simultaneous family ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveInjectiveBoundaryRadicalFamilyObj_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) : CategoryTheory.Injective (P.projectiveInjectiveBoundaryRadicalFamilyObj T hInjective hNotSimple p hp)

After simultaneous socle rejection, the radical of every selected projective is injective in the annihilated ambient full subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.minimalRightAlmostSplitAt_replacement_familySelected_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (p : S.ProjectiveLabel) (hp : p ∈ T) (q : S.ProjectiveLabel) (hq : q ∈ T) (t : (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)).index.obj) (ht : (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)).label t = q.label) : q = p

At the replacement endpoint belonging to p, any selected projective-injective occurring in the ambient right middle term is p itself.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyExceptionalSourceDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : CategoryTheory.FiniteIndecomposableDecomposition ((idealQuotientEquivalence (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).functor.obj (idealTorsionSubcategoryObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.minimalRightAlmostSplitAt ↑(P.socleQuotientReplacementNonprojectiveLabel p ⋯ ⋯)).middle))

For each selected replacement, restricting its ambient right almost-split source by the simultaneous family ideal preserves the number of indecomposable summands. The unique selected projective summand becomes its radical and every other summand is unchanged.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (p : S.ProjectiveLabel) (hp : p ∈ T) : FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp) + 1 = FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (P.primitiveProjectiveSocleFamilyFiniteReplacementLabel T hInjective hNotSimple p hp))

At each selected replacement endpoint, simultaneous socle rejection removes exactly one indecomposable occurrence from the incoming right mesh.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.minimalRightAlmostSplitAt_label_ne_familySelected_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (x : Fin S.n) (hx : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), x ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) (t : (S.minimalRightAlmostSplitAt x).index.obj) (p : S.ProjectiveLabel) : p ∈ T → (S.minimalRightAlmostSplitAt x).label t ≠ p.label

Away from all selected replacements, an ambient minimal right almost-split middle term contains no selected projective-injective summand.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.minimalRightAlmostSplitAt_middle_isAnnihilatedBy_family_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (x : Fin S.n) (hx : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), x ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) : IsAnnihilatedBy (P.primitiveProjectiveSocleFamilyIdeal T hInjective) (S.minimalRightAlmostSplitAt x).middle

Away from all selected replacements, the entire ambient minimal right almost-split middle term is annihilated by the simultaneous family ideal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyLabelObj_projective_iff_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (x : S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (hx : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), ↑x ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) : CategoryTheory.Projective (S.idealQuotientLabelObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) x) ↔ CategoryTheory.Projective (S.fgObj ↑x)

At an ordinary surviving endpoint, projectivity in the simultaneous annihilated subcategory is equivalent to ambient projectivity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyFGObj_projective_iff_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) (x : S.IdealQuotientLabel (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) (hx : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), ↑x ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) : CategoryTheory.Projective (S.idealQuotientFGObj (P.primitiveProjectiveSocleFamilyIdeal T hInjective) x) ↔ CategoryTheory.Projective (S.fgObj ↑x)

The same ordinary-endpoint projectivity comparison over the literal simultaneous quotient algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_isProjective_iff_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).n) (hj : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) j) ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) : S.finiteTauCategoryData.IsProjective ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) j) ↔ (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).IsProjective j

In the finite-tau presentations, projectivity is unchanged at every ordinary surviving endpoint of simultaneous rejection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_rightMiddleArity_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).n) (hj : ∀ (p : S.ProjectiveLabel) (hp : p ∈ T), ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) j) ≠ ↑(P.socleQuotientReplacementLabel p ⋯ ⋯)) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑((S.idealQuotientFiniteLabelEquiv (P.primitiveProjectiveSocleFamilyIdeal T hInjective)) j) = FiniteTauMatrix.rightMiddleArity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData j

Every ordinary surviving endpoint has the same incoming right-mesh arity before and after simultaneous socle rejection.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyRejectionProfile {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] : FiniteTauMatrix.FamilyRejectionProfile S.finiteTauCategoryData.toFiniteRightTauCategoryData (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData

The complete finite-tau rejection profile produced by simultaneously removing the socles of a finite basic family of non-simple indecomposable projective-injective modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_projectiveCount_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] : ARCount.projectiveCount S.finiteTauCategoryData.IsProjective = ARCount.projectiveCount (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).IsProjective

Simultaneous rejection replaces the selected projectives by the same number of projective quotient modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamily_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) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) (hNotSimple : ∀ p ∈ T, ¬IsSimpleModule Aᵐᵒᵖ ↑(S.fgObj p.label)) [IsNoetherianRing (idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal T hInjective))ᵐᵒᵖ] : ARCount.eulerMagnitude (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData) S.finiteTauCategoryData.IsProjective = ARCount.eulerMagnitude (FiniteTauMatrix.arrowMultiplicity (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).toFiniteRightTauCategoryData) (S.idealQuotientFiniteTauCategoryData (P.primitiveProjectiveSocleFamilyIdeal T hInjective)).IsProjective

Simultaneous rejection of a finite family of non-simple indecomposable projective-injectives preserves the Auslander--Reiten Euler magnitude.