Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveIdempotent

The primitive-idempotent multiplicity package #

For a primitive idempotent e : A, this file constructs the projective right ideal eA, the injective right module D(Ae), and the common coordinate Xe. Evaluation identifies Hom_A(eA, X) with Xe, while duality identifies Hom_A(X, D(Ae)) with D(Xe). On a finite indecomposable skeleton these literal modules give the source, sink, and weight satisfying both factor mesh unit equations used in the frozen manuscript.

source
def MagnitudeConjecture.RightModule.rightRegularLinearEquiv {A : Type u} [Ring A] :
Aᵐᵒᵖ ≃ₗ[Aᵐᵒᵖ] A

The right regular module is linearly equivalent to the regular module over the opposite ring.

Instances For
    source
    def MagnitudeConjecture.RightModule.rightRegularLeftMul {A : Type u} [Ring A] (e : A) :
    A →ₗ[Aᵐᵒᵖ] A

    Left multiplication by e, regarded as an endomorphism of the right regular module.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.rightRegularLeftMul_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e a : A) :
      (rightRegularLeftMul e) a = e * a
      source
      def MagnitudeConjecture.RightModule.rightIdeal {A : Type u} [Ring A] (e : A) :
      Submodule Aᵐᵒᵖ A

      The literal right ideal eA.

      Instances For
        source
        def MagnitudeConjecture.RightModule.rightIdealGenerator {A : Type u} [Ring A] (e : A) :
        ↥(rightIdeal e)

        The canonical generator e of eA.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.rightIdeal_fixed {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (y : ↥(rightIdeal e)) :
          e * ↑y = ↑y

          Every element of eA is fixed by left multiplication by e.

          source
          def MagnitudeConjecture.RightModule.rightIdealFGObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) :
          FinitelyGeneratedCategory A

          The right ideal eA as a literal finitely generated right module.

          Instances For
            source
            theorem MagnitudeConjecture.RightModule.rightRegular_projective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] :
            Module.Projective Aᵐᵒᵖ A

            The regular right module is projective.

            source
            theorem MagnitudeConjecture.RightModule.rightIdeal_moduleProjective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
            Module.Projective Aᵐᵒᵖ ↥(rightIdeal e)

            The idempotent right ideal eA is projective.

            source
            theorem MagnitudeConjecture.RightModule.rightIdealFGObj_projective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
            CategoryTheory.Projective (rightIdealFGObj e)

            The idempotent right ideal is categorically projective in the literal finitely generated module category.

            source
            def MagnitudeConjecture.RightModule.idempotentCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (X : FinitelyGeneratedCategory A) :
            Submodule k ↑X

            The e-coordinate Xe, realized as the range of right multiplication by e on a right module X.

            Instances For
              source
              theorem MagnitudeConjecture.RightModule.idempotentCoordinate_fixed {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (x : ↥(idempotentCoordinate e X)) :
              MulOpposite.op e • ↑x = ↑x

              An element of Xe is fixed by right multiplication by e.

              source
              def MagnitudeConjecture.RightModule.rightIdealLinearMapCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
              (↥(rightIdeal e) →ₗ[Aᵐᵒᵖ] ↑X) ≃ₗ[k] ↥(idempotentCoordinate e X)

              Evaluation at the generator identifies right-ideal maps with the idempotent coordinate.

              Instances For
                source
                def MagnitudeConjecture.RightModule.rightIdealHomCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                (rightIdealFGObj e ⟶ X) ≃ₗ[k] ↥(idempotentCoordinate e X)

                The categorical Hom space from eA is linearly equivalent to Xe.

                Instances For
                  source
                  def MagnitudeConjecture.RightModule.rightIdealActionHom {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (X : FinitelyGeneratedCategory A) (x : ↑X) :
                  rightIdealFGObj e ⟶ X

                  The map eA → X associated to an element x ∈ X, namely y ↦ x y.

                  Instances For
                    source
                    @[simp]
                    theorem MagnitudeConjecture.RightModule.rightIdealActionHom_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (X : FinitelyGeneratedCategory A) (x : ↑X) (y : ↑(rightIdealFGObj e)) :
                    (ModuleCat.Hom.hom (rightIdealActionHom e X x).hom) y = MulOpposite.op ↑y • x
                    source
                    theorem MagnitudeConjecture.RightModule.finrank_idempotentCoordinate_eq_zero_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                    Module.finrank k ↥(idempotentCoordinate e X) = 0 ↔ ∀ (x : ↑X), MulOpposite.op e • x = 0

                    The idempotent coordinate has dimension zero exactly when e acts by zero on the whole module.

                    source
                    theorem MagnitudeConjecture.RightModule.finrank_hom_rightIdeal_eq_coordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                    Module.finrank k (rightIdealFGObj e ⟶ X) = Module.finrank k ↥(idempotentCoordinate e X)

                    The Hom dimension from eA is exactly the dimension of the e-coordinate.

                    source
                    def MagnitudeConjecture.RightModule.leftRegularRightMul {A : Type u} [Ring A] (e : A) :
                    A →ₗ[A] A

                    Right multiplication by e, regarded as an endomorphism of the left regular module.

                    Instances For
                      source
                      def MagnitudeConjecture.RightModule.leftIdeal {A : Type u} [Ring A] (e : A) :
                      Submodule A A

                      The literal left ideal Ae.

                      Instances For
                        source
                        def MagnitudeConjecture.RightModule.leftIdealGenerator {A : Type u} [Ring A] (e : A) :
                        ↥(leftIdeal e)

                        The canonical generator e of Ae.

                        Instances For
                          source
                          @[reducible, inline]
                          abbrev MagnitudeConjecture.RightModule.leftIdealFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                          FGModuleCat A

                          The left ideal Ae as a literal finitely generated left module.

                          Instances For
                            source
                            theorem MagnitudeConjecture.RightModule.leftIdeal_moduleProjective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
                            Module.Projective A ↥(leftIdeal e)

                            The idempotent left ideal Ae is projective.

                            source
                            theorem MagnitudeConjecture.RightModule.leftIdealFGObj_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
                            CategoryTheory.Projective (leftIdealFGObj e)

                            The idempotent left ideal is categorically projective.

                            source
                            @[reducible, inline]
                            abbrev MagnitudeConjecture.RightModule.primitiveInjectiveFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                            FinitelyGeneratedCategory A

                            The manuscript's injective I(e)=D(Ae) as a literal finitely generated right module.

                            Instances For
                              source
                              def MagnitudeConjecture.RightModule.oppositeRightIdealToLeftIdeal {A : Type u} [Ring A] (e : A) :
                              ↥(rightIdeal (MulOpposite.op e)) → ↥(leftIdeal e)

                              The principal right ideal generated by op e over the opposite algebra, viewed as the original left ideal Ae.

                              Instances For
                                source
                                def MagnitudeConjecture.RightModule.leftIdealToOppositeRightIdeal {A : Type u} [Ring A] (e : A) :
                                ↥(leftIdeal e) → ↥(rightIdeal (MulOpposite.op e))

                                The inverse identification of Ae with the principal right ideal generated by op e over the opposite algebra.

                                Instances For
                                  source
                                  def MagnitudeConjecture.RightModule.oppositeRightIdealBidualMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                  ↥(rightIdeal (MulOpposite.op e)) →ₗ[Aᵐᵒᵖᵐᵒᵖ] ↑((QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k Aᵐᵒᵖ).obj (Opposite.op (primitiveInjectiveFGObj e)))

                                  Evaluation identifies the opposite principal projective (op e)Aᵒᵖ with the contragredient dual of the original primitive injective D(Ae). The scalar calculation is exactly the reversal of multiplication under MulOpposite.

                                  Instances For
                                    source
                                    theorem MagnitudeConjecture.RightModule.oppositeRightIdealBidualMap_bijective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                    Function.Bijective ⇑(oppositeRightIdealBidualMap e)

                                    The evaluation map from the opposite principal projective to the dual of the primitive injective is bijective.

                                    source
                                    noncomputable def MagnitudeConjecture.RightModule.oppositeRightIdealBidualLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                    ↥(rightIdeal (MulOpposite.op e)) ≃ₗ[Aᵐᵒᵖᵐᵒᵖ] ↑((QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k Aᵐᵒᵖ).obj (Opposite.op (primitiveInjectiveFGObj e)))

                                    The opposite principal projective is linearly equivalent to the contragredient dual of the original primitive injective.

                                    Instances For
                                      source
                                      noncomputable def MagnitudeConjecture.RightModule.oppositeRightIdealDualPrimitiveInjectiveIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (e : A) :
                                      rightIdealFGObj (MulOpposite.op e) ≅ (QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k Aᵐᵒᵖ).obj (Opposite.op (primitiveInjectiveFGObj e))

                                      Categorical form of the identification (op e)Aᵒᵖ ≅ D(D(Ae)).

                                      Instances For
                                        source
                                        theorem MagnitudeConjecture.RightModule.primitiveInjectiveFGObj_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) :
                                        CategoryTheory.Injective (primitiveInjectiveFGObj e)

                                        Contragredient duality sends the projective left ideal Ae to the injective right module D(Ae).

                                        source
                                        theorem MagnitudeConjecture.RightModule.leftIdeal_fixed {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (y : ↥(leftIdeal e)) :
                                        ↑y * e = ↑y

                                        Every element of Ae is fixed by right multiplication by e.

                                        source
                                        def MagnitudeConjecture.RightModule.coordinateProduct {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (x : ↑X) (y : ↑(leftIdealFGObj e)) :
                                        ↥(idempotentCoordinate e X)

                                        Multiplication of x : X by an element of Ae lands in Xe.

                                        Instances For
                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coordinateProduct_add_leftIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (x : ↑X) (y z : ↑(leftIdealFGObj e)) :
                                          coordinateProduct he X x (y + z) = coordinateProduct he X x y + coordinateProduct he X x z
                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coordinateProduct_add_source {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (x z : ↑X) (y : ↑(leftIdealFGObj e)) :
                                          coordinateProduct he X (x + z) y = coordinateProduct he X x y + coordinateProduct he X z y
                                          source
                                          theorem MagnitudeConjecture.RightModule.leftIdeal_module_eq_restrictScalars {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) :
                                          inferInstance = Module.restrictScalars k A ↑(leftIdealFGObj e)

                                          The inherited k-action on the literal left ideal agrees with the action obtained by restricting its A-module structure.

                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coe_smul_leftIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (r : k) (x : ↥(leftIdeal e)) :
                                          ↑(r • x) = r • ↑x
                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coe_smul_rightIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (r : k) (x : ↥(rightIdeal e)) :
                                          ↑(r • x) = r • ↑x
                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coe_restrictScalars_smul_leftIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (r : k) (x : ↑(leftIdealFGObj e)) :
                                          ↑(SMul.smul r x) = r • ↑x
                                          source
                                          @[simp]
                                          theorem MagnitudeConjecture.RightModule.coe_restrictScalars_smul_rightIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (r : k) (x : ↑(rightIdealFGObj e)) :
                                          ↑(SMul.smul r x) = r • ↑x
                                          source
                                          def MagnitudeConjecture.RightModule.leftIdealToRightCoordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (h : ↥(leftIdeal f) →ₗ[A] ↥(leftIdeal e)) :
                                          ↥(idempotentCoordinate e (rightIdealFGObj f))

                                          Evaluation of a left-ideal map at the generator, bundled in the common corner coordinate.

                                          Instances For
                                            source
                                            def MagnitudeConjecture.RightModule.rightCoordinateToLeftIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (x : ↥(idempotentCoordinate e (rightIdealFGObj f))) :
                                            ↥(leftIdeal f) →ₗ[A] ↥(leftIdeal e)

                                            A common corner coordinate acts by right multiplication to produce a map Af → Ae.

                                            Instances For
                                              source
                                              def MagnitudeConjecture.RightModule.leftIdealLinearMapRightCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) :
                                              (↥(leftIdeal f) →ₗ[A] ↥(leftIdeal e)) ≃ₗ[k] ↥(idempotentCoordinate e (rightIdealFGObj f))

                                              Evaluation at the generator of Af identifies maps Af → Ae with the same corner coordinate that represents maps eA → fA.

                                              Instances For
                                                source
                                                def MagnitudeConjecture.RightModule.leftIdealHomRightCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) :
                                                (leftIdealFGObj f ⟶ leftIdealFGObj e) ≃ₗ[k] ↥(idempotentCoordinate e (rightIdealFGObj f))

                                                Categorical left-ideal Hom and right-ideal Hom have the same corner coordinate.

                                                Instances For
                                                  source
                                                  def MagnitudeConjecture.RightModule.leftIdealHomPrimitiveInjectiveHomLinearMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e f : A) :
                                                  (leftIdealFGObj f ⟶ leftIdealFGObj e) →ₗ[k] primitiveInjectiveFGObj e ⟶ primitiveInjectiveFGObj f

                                                  Contragredient duality sends a map Af → Ae to the reversed map D(Ae) → D(Af), linearly over the coefficient field.

                                                  Instances For
                                                    source
                                                    noncomputable def MagnitudeConjecture.RightModule.leftIdealHomPrimitiveInjectiveHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e f : A) :
                                                    (leftIdealFGObj f ⟶ leftIdealFGObj e) ≃ₗ[k] primitiveInjectiveFGObj e ⟶ primitiveInjectiveFGObj f

                                                    The Hom space between primitive injectives is the reversed Hom space between their defining left ideals.

                                                    Instances For
                                                      source
                                                      noncomputable def MagnitudeConjecture.RightModule.primitiveInjectiveHomRightIdealHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) :
                                                      (primitiveInjectiveFGObj e ⟶ primitiveInjectiveFGObj f) ≃ₗ[k] rightIdealFGObj e ⟶ rightIdealFGObj f

                                                      Maps between primitive injectives and maps between the corresponding primitive projectives have the same corner coordinate.

                                                      Instances For
                                                        source
                                                        @[simp]
                                                        theorem MagnitudeConjecture.RightModule.coordinateProduct_restrictScalars_smul {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (x : ↑X) (r : k) (y : ↑(leftIdealFGObj e)) :
                                                        coordinateProduct he X x (SMul.smul r y) = r • coordinateProduct he X x y

                                                        The coordinate product is k-linear when the left ideal is equipped with the restricted scalar action used by contragredient duality.

                                                        source
                                                        def MagnitudeConjecture.RightModule.primitiveInjectiveInnerDualEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                                        ↑((QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k A).obj (Opposite.op (leftIdealFGObj e))) ≃ₗ[k] Module.Dual k ↑(leftIdealFGObj e)

                                                        The concrete contragredient object has the ordinary vector-space dual as its underlying k-module.

                                                        Instances For
                                                          source
                                                          def MagnitudeConjecture.RightModule.homPrimitiveInjectiveCoordinateDualEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                                                          (↑X →ₗ[Aᵐᵒᵖ] ↑(primitiveInjectiveFGObj e)) ≃ₗ[k] Module.Dual k ↥(idempotentCoordinate e X)

                                                          The elementary dual-coordinate form of the standard isomorphism Hom_A(X,D(Ae)) ≅ D(Xe).

                                                          Instances For
                                                            source
                                                            def MagnitudeConjecture.RightModule.primitiveInjectiveHomCoordinateDualEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                                                            (X ⟶ primitiveInjectiveFGObj e) ≃ₗ[k] Module.Dual k ↥(idempotentCoordinate e X)

                                                            The categorical sink Hom space is linearly equivalent to the dual of the primitive coordinate.

                                                            Instances For
                                                              source
                                                              @[simp]
                                                              theorem MagnitudeConjecture.RightModule.primitiveInjectiveHomCoordinateDualEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (f : X ⟶ primitiveInjectiveFGObj e) (x : ↥(idempotentCoordinate e X)) :
                                                              ((primitiveInjectiveHomCoordinateDualEquiv he X) f) x = ((primitiveInjectiveInnerDualEquiv e) ((ModuleCat.Hom.hom f.hom) ↑x)) (leftIdealGenerator e)
                                                              source
                                                              theorem MagnitudeConjecture.RightModule.primitiveInjectiveHomCoordinateDualEquiv_apply_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) (f : X ⟶ primitiveInjectiveFGObj e) (x : ↥(idempotentCoordinate e X)) (hfx : (ModuleCat.Hom.hom f.hom) ↑x = 0) :
                                                              ((primitiveInjectiveHomCoordinateDualEquiv he X) f) x = 0
                                                              source
                                                              theorem MagnitudeConjecture.RightModule.finrank_hom_primitiveInjective_eq_coordinate {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (X : FinitelyGeneratedCategory A) :
                                                              Module.finrank k (X ⟶ primitiveInjectiveFGObj e) = Module.finrank k ↥(idempotentCoordinate e X)

                                                              The Hom dimension into D(Ae) is the dimension of Xe.

                                                              source
                                                              theorem MagnitudeConjecture.RightModule.fgIndecomposable_of_isIndecomposableModule {R : Type u} [Ring R] [IsNoetherianRing R] (M : FGModuleCat R) (hM : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↑M) :
                                                              CategoryTheory.Indecomposable M

                                                              Module-theoretic indecomposability implies categorical indecomposability in the finitely generated module category.

                                                              source
                                                              structure MagnitudeConjecture.RightModule.PrimitiveIdempotentData {A : Type u} [Ring A] (e : A) :
                                                              Prop

                                                              A primitive idempotent, expressed by the absence of nontrivial idempotents in its corner eAe.

                                                              • idempotent : IsIdempotentElem e
                                                              • nonzero : e ≠ 0
                                                              • corner_idempotent (b : A) : IsIdempotentElem b → e * b = b → b * e = b → b = 0 ∨ b = e
                                                              Instances For
                                                                source
                                                                theorem MagnitudeConjecture.RightModule.PrimitiveIdempotentData.opposite {A : Type u} [Ring A] {e : A} (D : PrimitiveIdempotentData e) :
                                                                PrimitiveIdempotentData (MulOpposite.op e)

                                                                A primitive idempotent remains primitive in the opposite algebra.

                                                                source
                                                                theorem MagnitudeConjecture.RightModule.rightIdeal_isIndecomposableModule {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(rightIdealFGObj e)

                                                                The right ideal of a primitive idempotent is indecomposable in the module-theoretic sense.

                                                                source
                                                                theorem MagnitudeConjecture.RightModule.rightIdealFGObj_indecomposable {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                CategoryTheory.Indecomposable (rightIdealFGObj e)

                                                                The literal right ideal of a primitive idempotent is categorically indecomposable.

                                                                source
                                                                theorem MagnitudeConjecture.RightModule.leftIdeal_isIndecomposableModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule A ↑(leftIdealFGObj e)

                                                                The left ideal of a primitive idempotent is indecomposable in the module-theoretic sense used by contragredient duality.

                                                                source
                                                                theorem MagnitudeConjecture.RightModule.primitiveInjectiveFGObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                CategoryTheory.Indecomposable (primitiveInjectiveFGObj e)

                                                                Contragredient duality sends the primitive left ideal to an indecomposable right injective.

                                                                source
                                                                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSourceLabel {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) :
                                                                Fin S.n

                                                                The unique skeleton label representing the primitive projective eA.

                                                                Instances For
                                                                  source
                                                                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSourceIso {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) :
                                                                  rightIdealFGObj e ≅ S.fgObj (S.primitiveSourceLabel D)

                                                                  The chosen identification of eA with its skeleton representative.

                                                                  Instances For
                                                                    source
                                                                    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSource_projective {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) :
                                                                    CategoryTheory.Projective (S.fgObj (S.primitiveSourceLabel D))

                                                                    The chosen primitive-projective skeleton object is projective.

                                                                    source
                                                                    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSourceHomCoordinateEquiv {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 : FinitelyGeneratedCategory A) :
                                                                    (S.fgObj (S.primitiveSourceLabel D) ⟶ X) ≃ₗ[k] ↥(idempotentCoordinate e X)

                                                                    Transporting evaluation at e across the chosen skeleton isomorphism identifies the distinguished source Hom space with Xe.

                                                                    Instances For
                                                                      source
                                                                      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSinkLabel {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) :
                                                                      Fin S.n

                                                                      The unique skeleton label representing the primitive injective D(Ae).

                                                                      Instances For
                                                                        source
                                                                        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSinkIso {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) :
                                                                        primitiveInjectiveFGObj e ≅ S.fgObj (S.primitiveSinkLabel D)

                                                                        The chosen identification of D(Ae) with its skeleton representative.

                                                                        Instances For
                                                                          source
                                                                          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSink_injective {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) :
                                                                          CategoryTheory.Injective (S.fgObj (S.primitiveSinkLabel D))

                                                                          The chosen primitive-injective skeleton object is injective.

                                                                          source
                                                                          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSinkHomCoordinateDualEquiv {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 : FinitelyGeneratedCategory A) :
                                                                          (X ⟶ S.fgObj (S.primitiveSinkLabel D)) ≃ₗ[k] Module.Dual k ↥(idempotentCoordinate e X)

                                                                          Transport across the chosen skeleton isomorphism identifies the distinguished sink Hom space with the dual of Xe.

                                                                          Instances For
                                                                            source
                                                                            def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveKilledLabels {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (_D : PrimitiveIdempotentData e) :
                                                                            Set (Fin S.n)

                                                                            Labels killed by the primitive deletion are exactly those on which e acts by zero.

                                                                            Instances For
                                                                              source
                                                                              noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (_D : PrimitiveIdempotentData e) (x : Fin S.n) :
                                                                              ℕ

                                                                              The paper's primitive coordinate, before identifying it with composition multiplicity.

                                                                              Instances For
                                                                                source
                                                                                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_primitiveKilledLabels_iff_primitiveMultiplicity_zero {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 ↔ S.primitiveMultiplicity D x = 0

                                                                                The zero set of the primitive coordinate is the killed subcategory.

                                                                                source
                                                                                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_eq_sourceHom {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 = Module.finrank k (S.fgObj (S.primitiveSourceLabel D) ⟶ S.fgObj x)

                                                                                The primitive coordinate is the source Hom dimension on every skeleton object.

                                                                                source
                                                                                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicity_eq_sinkHom {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 = Module.finrank k (S.fgObj x ⟶ S.fgObj (S.primitiveSinkLabel D))

                                                                                The same primitive coordinate is the sink Hom dimension on every skeleton object.

                                                                                source
                                                                                theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSource_not_mem_primitiveKilledLabels {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) :
                                                                                S.primitiveSourceLabel D ∉ S.primitiveKilledLabels D

                                                                                The primitive projective itself survives deletion.

                                                                                source
                                                                                noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSource {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) :
                                                                                S.SurvivingLabel (S.primitiveKilledLabels D)

                                                                                The primitive projective as a surviving factor label.

                                                                                Instances For
                                                                                  source
                                                                                  theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSink_not_mem_primitiveKilledLabels {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) :
                                                                                  S.primitiveSinkLabel D ∉ S.primitiveKilledLabels D

                                                                                  The primitive injective itself survives deletion.

                                                                                  source
                                                                                  noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSink {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) :
                                                                                  S.SurvivingLabel (S.primitiveKilledLabels D)

                                                                                  The primitive injective as a surviving factor label.

                                                                                  Instances For
                                                                                    source
                                                                                    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMultiplicityInput {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) :
                                                                                    S.PrimitiveMultiplicityInput (S.primitiveKilledLabels D)

                                                                                    A primitive idempotent supplies the complete ambient multiplicity package used to prove the two factor mesh unit equations.

                                                                                    Instances For
                                                                                      source
                                                                                      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveMeshUnitEquations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] {e : A} (D : PrimitiveIdempotentData e) :
                                                                                      (∀ (target : S.SurvivingLabel (S.primitiveKilledLabels D)), FiniteTauMatrix.meshColumnWeight (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)) (fun (x : S.SurvivingLabel (S.primitiveKilledLabels D)) => ↑(S.primitiveMultiplicity D ↑x)) target = if target = S.primitiveSource D then 1 else 0) ∧ ∀ (source : S.SurvivingLabel (S.primitiveKilledLabels D)), FiniteTauMatrix.meshRowWeight (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)) (fun (x : S.SurvivingLabel (S.primitiveKilledLabels D)) => ↑(S.primitiveMultiplicity D ↑x)) source = if source = S.primitiveSink D then 1 else 0

                                                                                      The primitive coordinate satisfies both mesh unit equations in the literal factor category.