Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveQuotient

The primitive quotient A/AeA #

This file identifies the coordinate-zero deletion used by the compiled primitive mesh package with the frozen manuscript's literal quotient by the two-sided ideal AeA.

source
def MagnitudeConjecture.RightModule.primitiveIdeal {A : Type u} [Ring A] (e : A) :
TwoSidedIdeal A

The two-sided ideal denoted AeA in the manuscript: the two-sided ideal generated by e.

Instances For
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.RightModule.primitiveQuotientAlgebra {A : Type u} [Ring A] (e : A) :
    Type u

    The manuscript's primitive quotient algebra A/AeA.

    Instances For
      source
      def MagnitudeConjecture.RightModule.primitiveQuotientMap {A : Type u} [Ring A] (e : A) :
      A →+* primitiveQuotientAlgebra e

      The canonical quotient map A ⟶ A/AeA.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.primitiveQuotientMap_ker {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) :
        TwoSidedIdeal.ker (primitiveQuotientMap e) = primitiveIdeal e

        The kernel of the primitive quotient map is exactly AeA.

        source
        theorem MagnitudeConjecture.RightModule.mem_primitiveIdeal_iff_quotient_eq_zero {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e a : A} :
        a ∈ primitiveIdeal e ↔ (primitiveQuotientMap e) a = 0

        Membership in AeA is equivalent to vanishing in A/AeA.

        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.primitiveQuotientMap_generator {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) :
        (primitiveQuotientMap e) e = 0

        The primitive generator is zero in A/AeA.

        source
        def MagnitudeConjecture.RightModule.IsAnnihilatedBy {A : Type u} [Ring A] (I : TwoSidedIdeal A) (X : FinitelyGeneratedCategory A) :
        Prop

        A right module is annihilated by a two-sided ideal when every element of the ideal acts as zero.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.isAnnihilatedBy_primitiveIdeal_iff {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (X : FinitelyGeneratedCategory A) :
          IsAnnihilatedBy (primitiveIdeal e) X ↔ ∀ (x : ↑X), MulOpposite.op e • x = 0

          A right module is annihilated by AeA exactly when e itself acts as zero.

          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_primitiveKilledLabels_iff_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) (x : Fin S.n) :
          x ∈ S.primitiveKilledLabels D ↔ IsAnnihilatedBy (primitiveIdeal e) (S.fgObj x)

          The labels killed by the primitive coordinate are exactly the indecomposable modules annihilated by the manuscript's ideal AeA.

          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_eq_zero_iff_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) (x : Fin S.n) :
          S.primitiveMultiplicity D x = 0 ↔ IsAnnihilatedBy (primitiveIdeal e) (S.fgObj x)

          Equivalently, the zero set of the primitive multiplicity is the literal AeA-annihilated subcategory.