Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleProjectiveInjectiveSocleIdeal

Socle ideals of primitive projective-injective right modules #

Let eA be one member of a complete duplicate-free family of primitive projective right ideals. If eA is injective, then its socle, embedded in the regular right module, is stable under left multiplication and hence is a two-sided ideal. This is the algebraic first step of the rejection lemma.

The proof is the Auslander--Reiten argument in coordinates. A nonzero off-diagonal component eA → fA on the simple essential socle would be monic; injectivity of eA would split it; and indecomposability of fA would then make the two selected primitive projectives isomorphic, contradicting the duplicate-free skeleton.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleSubmodule {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) :
Submodule Aᵐᵒᵖ A

The socle of the selected primitive projective p, embedded in the right regular module.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveLeftActionComponent {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) (a : A) :
    rightIdealFGObj (P.idempotent p) ⟶ rightIdealFGObj (P.idempotent q)

    The (q,p) coordinate of left multiplication by a, restricted from pA to qA.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveLeftActionComponent_apply_val {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) (a : A) (x : ↑(rightIdealFGObj (P.idempotent p))) :
      ↑((ModuleCat.Hom.hom (P.primitiveLeftActionComponent p q a).hom) x) = P.idempotent q * (a * ↑x)
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.moduleSocleInclusion_comp_primitiveLeftActionComponent_eq_zero {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)) (hpq : q ≠ p) (a : A) :
      CategoryTheory.CategoryStruct.comp (moduleSocleInclusion (rightIdealFGObj (P.idempotent p))) (P.primitiveLeftActionComponent p q a) = 0

      Every off-diagonal left-action component kills the socle of a selected primitive projective-injective.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mul_mem_primitiveProjectiveSocleSubmodule {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)) {a x : A} (hx : x ∈ P.primitiveProjectiveSocleSubmodule p) :
      a * x ∈ P.primitiveProjectiveSocleSubmodule p

      Left multiplication preserves the embedded socle of a selected primitive projective-injective.

      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleIdeal {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)) :
      TwoSidedIdeal A

      The socle of a selected primitive projective-injective, embedded in the regular module, is a two-sided ideal.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mem_primitiveProjectiveSocleIdeal {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)) (x : A) :
        x ∈ P.primitiveProjectiveSocleIdeal p hpInjective ↔ x ∈ P.primitiveProjectiveSocleSubmodule p
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.isAnnihilatedBy_primitiveProjectiveSocleIdeal_of_not_iso {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)) (M : FinitelyGeneratedCategory A) (hM : CategoryTheory.Indecomposable M) (hnoniso : ¬Nonempty (M ≅ S.fgObj p.label)) :
        IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) M

        Every indecomposable module other than the selected projective-injective is annihilated by its embedded socle ideal.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.fgObj_isAnnihilatedBy_primitiveProjectiveSocleIdeal {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)) (i : Fin S.n) (hip : i ≠ p.label) :
        IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) (S.fgObj i)

        In the fixed finite skeleton, every label except the rejected projective-injective belongs to the annihilated quotient subcategory.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightIdealFGObj_not_isAnnihilatedBy_primitiveProjectiveSocleIdeal {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) (rightIdealFGObj (P.idempotent p))

        The rejected literal primitive projective is not annihilated by its own socle ideal.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.fgObj_not_isAnnihilatedBy_primitiveProjectiveSocleIdeal {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) (S.fgObj p.label)

        The selected skeletal projective is not annihilated by its own socle ideal.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.fgObj_isAnnihilatedBy_primitiveProjectiveSocleIdeal_iff {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)) (i : Fin S.n) :
        IsAnnihilatedBy (P.primitiveProjectiveSocleIdeal p hpInjective) (S.fgObj i) ↔ i ≠ p.label

        The annihilated indecomposable labels are exactly the complement of the rejected projective-injective label.

        source
        def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.socleQuotientLabelEquivComplement {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 }

        The quotient's intrinsic label type is canonically the complement of the single rejected ambient label.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.card_socleQuotientLabel_add_one {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)) :
          Fintype.card (S.IdealQuotientLabel (P.primitiveProjectiveSocleIdeal p hpInjective)) + 1 = S.n

          One socle rejection removes exactly one indecomposable label.