Multiplicative bases

MBDVendor.Magnitude.Algebra.RightModulePrimitiveIdempotent

The primitive-idempotent multiplicity package #

(Extracted glue file: lines 1–1245 of the magnitude file of the same name; see MBDVendor/README.md. The skeleton-specific remainder is not copied.)

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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.rightRegularLeftMul_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e a : A) :
      (rightRegularLeftMul e) a = e * a
      source
      def MBDVendor.Magnitude.RightModule.rightIdeal {A : Type u} [Ring A] (e : A) :
      Submodule Aᵐᵒᵖ A

      The literal right ideal eA.

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

        The canonical generator e of eA.

        Instances For
          source
          theorem MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.rightRegular_projective {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] :
            Module.Projective Aᵐᵒᵖ A

            The regular right module is projective.

            source
            theorem MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.leftIdeal {A : Type u} [Ring A] (e : A) :
                      Submodule A A

                      The literal left ideal Ae.

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

                        The canonical generator e of Ae.

                        Instances For
                          source
                          @[reducible, inline]
                          abbrev MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.oppositeRightIdealBidualMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                  ↥(rightIdeal (MulOpposite.op e)) →ₗ[Aᵐᵒᵖᵐᵒᵖ] ↑((QSE.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.oppositeRightIdealBidualLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                    ↥(rightIdeal (MulOpposite.op e)) ≃ₗ[Aᵐᵒᵖᵐᵒᵖ] ↑((QSE.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 MBDVendor.Magnitude.RightModule.oppositeRightIdealDualPrimitiveInjectiveIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (e : A) :
                                      rightIdealFGObj (MulOpposite.op e) ≅ (QSE.Contragredient.dualFunctor k Aᵐᵒᵖ).obj (Opposite.op (primitiveInjectiveFGObj e))

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

                                      Instances For
                                        source
                                        theorem MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.primitiveInjectiveInnerDualEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) :
                                                        ↑((QSE.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.fgIndecomposable_of_isIndecomposableModule {R : Type u} [Ring R] [IsNoetherianRing R] (M : FGModuleCat R) (hM : QSE.Foundation.IsIndecomposableModule R ↑M) :
                                                              CategoryTheory.Indecomposable M

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

                                                              source
                                                              structure MBDVendor.Magnitude.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 MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.rightIdeal_isIndecomposableModule {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                QSE.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(rightIdealFGObj e)

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

                                                                source
                                                                theorem MBDVendor.Magnitude.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 MBDVendor.Magnitude.RightModule.leftIdeal_isIndecomposableModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (D : PrimitiveIdempotentData e) :
                                                                QSE.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 MBDVendor.Magnitude.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.