Canonical socle families under algebra equivalence

The family of nonuniserial indecomposable projective-injective right modules is intrinsic. Combining this observation with transport of the embedded socle-family ideal gives an algebra equivalence between the two literal canonical socle quotients.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.mapAlgEquivProjectiveLabels_nonuniserialProjectiveInjectiveLabels {k A B : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (f : A ≃ₐ[k] B) : mapAlgEquivProjectiveLabels S f S.nonuniserialProjectiveInjectiveLabels = (S.mapAlgEquiv f).nonuniserialProjectiveInjectiveLabels

Transporting projective labels carries the canonical nonuniserial projective-injective family exactly onto the canonical target family.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.canonicalSocleFamilyQuotientAlgEquiv {k A B : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (f : A ≃ₐ[k] B) : idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯) ≃ₐ[k] idealQuotientAlgebra ((P.mapAlgEquiv f).primitiveProjectiveSocleFamilyIdeal (S.mapAlgEquiv f).nonuniserialProjectiveInjectiveLabels ⋯)

The literal canonical simultaneous-socle quotient is invariant under algebra equivalence.