Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleSocleFamilyPresentationIndependence

Independence of primitive-projective socle families #

Two complete primitive-projective presentations of the same duplicate-free right-module skeleton determine the same embedded socle ideal at each injective projective label, and hence the same simultaneous family ideal.

The proof compares the two decompositions of the regular right module. The resulting regular-module automorphism matches corresponding projective summands and their socles. Since an endomorphism of the regular right module is left multiplication by its value at one, two-sidedness turns that transported equality back into literal equality inside the ambient algebra.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.regularChangeIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) :
rightRegularFGObj ≅ rightRegularFGObj
Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightIdealInclusion_comp_regularDecompositionMap {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) :
    CategoryTheory.CategoryStruct.comp (rightIdealInclusion (P.idempotent p)) (regularDecompositionMap P.idempotent) = CategoryTheory.Limits.biproduct.ι (fun (q : S.ProjectiveLabel) => rightIdealFGObj (P.idempotent q)) p
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightIdealInclusion_comp_regularChangeIso_hom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) :
    CategoryTheory.CategoryStruct.comp (rightIdealInclusion (P.idempotent p)) (P.regularChangeIso Q).hom = CategoryTheory.CategoryStruct.comp (P.primitiveProjectiveIso p).hom (CategoryTheory.CategoryStruct.comp (Q.primitiveProjectiveIso p).inv (rightIdealInclusion (Q.idempotent p)))
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveChangeIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) :
    rightIdealFGObj (P.idempotent p) ≅ rightIdealFGObj (Q.idempotent p)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.map_primitiveProjectiveSocleSubmodule_regularChangeIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) :
      Submodule.map (ModuleCat.Hom.hom (P.regularChangeIso Q).hom.hom) (P.primitiveProjectiveSocleSubmodule p) = Q.primitiveProjectiveSocleSubmodule p
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightRegularFGHom_apply_eq_apply_one_mul {A : Type u} [Ring A] (f : rightRegularFGObj ⟶ rightRegularFGObj) (x : A) :
      (ModuleCat.Hom.hom f.hom) x = (ModuleCat.Hom.hom f.hom) 1 * x
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleIdeal_le_of_presentations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) :
      P.primitiveProjectiveSocleIdeal p hpInjective ≤ Q.primitiveProjectiveSocleIdeal p hpInjective
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleIdeal_eq_of_presentations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (hpInjective : CategoryTheory.Injective (S.fgObj p.label)) :
      P.primitiveProjectiveSocleIdeal p hpInjective = Q.primitiveProjectiveSocleIdeal p hpInjective
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveSocleFamilyIdeal_eq_of_presentations {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P Q : S.PrimitiveProjectivePresentation) (T : Finset S.ProjectiveLabel) (hInjective : ∀ p ∈ T, CategoryTheory.Injective (S.fgObj p.label)) :
      P.primitiveProjectiveSocleFamilyIdeal T hInjective = Q.primitiveProjectiveSocleFamilyIdeal T hInjective