Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveCornerCategory

The concrete corner category of a primitive-projective presentation #

A complete primitive-projective presentation realizes the selected projective category by the literal corners e_q A e_p. This auxiliary category keeps ambient algebra coordinates as the morphism type, which is the convenient form for the finite-ideal pencil argument. Its canonical linear functor to the existing selected-projective category is fully faithful and bijective on objects.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.PrimitiveCornerCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (_P : S.PrimitiveProjectivePresentation) :
Type

The literal primitive-corner category attached to the presentation. The type wrapper retains P as an inferable parameter.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.cornerVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
    P.PrimitiveCornerCategory ≃ S.ProjectiveLabel

    Recover the selected-projective label represented by a corner object.

    Instances For
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
      Fintype P.PrimitiveCornerCategory
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryDecidableEq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
      DecidableEq P.PrimitiveCornerCategory
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
      CategoryTheory.Category.{u, 0} P.PrimitiveCornerCategory
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategory_id_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 : P.PrimitiveCornerCategory) :
      ↑(CategoryTheory.CategoryStruct.id p) = P.idempotent (P.cornerVertex p)
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategory_comp_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 r : P.PrimitiveCornerCategory} (f : p ⟶ q) (g : q ⟶ r) :
      ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g * ↑f
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategory_idempotent_mul_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 : P.PrimitiveCornerCategory} (f : p ⟶ q) :
      P.idempotent (P.cornerVertex q) * ↑f = ↑f
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategory_val_mul_idempotent {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 : P.PrimitiveCornerCategory} (f : p ⟶ q) :
      ↑f * P.idempotent (P.cornerVertex p) = ↑f
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryPreadditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
      CategoryTheory.Preadditive P.PrimitiveCornerCategory
      source
      @[instance_reducible]
      noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
      CategoryTheory.Linear k P.PrimitiveCornerCategory
      source
      instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryHomFinite {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 : P.PrimitiveCornerCategory) :
      Module.Finite k (p ⟶ q)
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerHomLinearEquiv {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 : P.PrimitiveCornerCategory) :
      (p ⟶ q) ≃ₗ[k] S.ordinaryProjectiveObj (P.cornerVertex p) ⟶ S.ordinaryProjectiveObj (P.cornerVertex q)

      The corner Hom space is linearly equivalent to the corresponding selected-projective Hom space.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveHomCoordinate_primitiveCornerHomLinearEquiv {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 : P.PrimitiveCornerCategory} (f : p ⟶ q) :
        P.projectiveHomCoordinate ((P.primitiveCornerHomLinearEquiv p q) f) = ↑f
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerToProjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
        CategoryTheory.Functor P.PrimitiveCornerCategory S.ProjectiveCategory

        The coordinate realization as a linear functor to the existing selected projective category.

        Instances For
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerToProjective_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
          P.primitiveCornerToProjective.Additive
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerToProjective_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
          CategoryTheory.Functor.Linear k P.primitiveCornerToProjective
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerToProjective_full {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
          P.primitiveCornerToProjective.Full
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerToProjective_faithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
          P.primitiveCornerToProjective.Faithful
          source
          instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveCornerCategoryEndLocal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : P.PrimitiveCornerCategory) :
          IsLocalRing (CategoryTheory.End p)

          Every concrete primitive-corner endomorphism ring is local.