Right-module invariants under algebra equivalence

An algebra equivalence transports complete finite indecomposable right-module skeletons, their Auslander--Reiten surplus, primitive idempotents, and literal primitive quotients. These facts let the standard-covering calculation be performed in its strict orbit algebra and stated in the manuscript's literal standard-form algebra.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.fgModuleEquivalenceOfAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (f : A ≃ₐ[k] B) : FinitelyGeneratedCategory A ≌ FinitelyGeneratedCategory B

Restriction of scalars along the opposite algebra equivalence, regarded as an equivalence of finitely generated right-module categories.

def MagnitudeConjecture.RightModule.rightIdealMapAlgEquivLinearEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (f : A ≃ₐ[k] B) (e : A) : ↑((fgModuleEquivalenceOfAlgEquiv f).functor.obj (rightIdealFGObj e)) ≃ₗ[Bᵐᵒᵖ] ↑(rightIdealFGObj (f e))

Applying an algebra equivalence coefficientwise identifies the image of the principal right ideal eA with the principal right ideal f(e)B.

noncomputable def MagnitudeConjecture.RightModule.rightIdealFGObjMapAlgEquivIso {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (f : A ≃ₐ[k] B) (e : A) : (fgModuleEquivalenceOfAlgEquiv f).functor.obj (rightIdealFGObj e) ≅ rightIdealFGObj (f e)

The categorical form of the coefficientwise principal-right-ideal equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapAlgEquiv {k A B : Type u} [Field 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) : FiniteIndecomposableSkeleton k B

Transport a complete duplicate-free right-module skeleton along an algebra equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mapAlgEquivObjIso {k A B : Type u} [Field 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) (i : Fin S.n) : (fgModuleEquivalenceOfAlgEquiv f).functor.obj (S.fgObj i) ≅ (S.mapAlgEquiv f).fgObj i

The transported skeleton object is the functorial image of the original one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_mapAlgEquiv {k A B : Type u} [Field 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) : (S.mapAlgEquiv f).ambientARSurplus = S.ambientARSurplus

Algebra equivalence preserves the ambient Auslander--Reiten surplus.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.relabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : Fin T.n

The label of T representing the finitely generated module at a label of S.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.relabelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.fgObj i ≅ T.fgObj (S.relabel T i)

The chosen module isomorphism underlying relabelling.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.relabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) : Function.Injective (S.relabel T)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.relabel_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) : Function.Surjective (S.relabel T)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.relabelEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) : Fin S.n ≃ Fin T.n

Any two complete duplicate-free right-module skeletons for the same algebra have equivalent label types.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientARSurplus_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S T : FiniteIndecomposableSkeleton k A) : S.ambientARSurplus = T.ambientARSurplus

The ambient Auslander--Reiten surplus does not depend on the chosen complete duplicate-free right-module skeleton.

theorem MagnitudeConjecture.RightModule.primitiveIdeal_eq_comap_algEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (e : A) : primitiveIdeal e = (TwoSidedIdeal.comap f) (primitiveIdeal (f e))

An algebra equivalence carries the generated ideal AeA to the ideal generated by the image of e.

theorem MagnitudeConjecture.RightModule.primitiveIdeal_ringCon_eq_comap_algEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (e : A) : (primitiveIdeal e).ringCon = (primitiveIdeal (f e)).ringCon.comap f

noncomputable def MagnitudeConjecture.RightModule.primitiveQuotientAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (e : A) : primitiveQuotientAlgebra e ≃ₐ[k] primitiveQuotientAlgebra (f e)

Algebra equivalence transports the literal primitive quotient.

@[simp]

theorem MagnitudeConjecture.RightModule.primitiveQuotientAlgEquiv_mk {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (e a : A) : (primitiveQuotientAlgEquiv f e) ((primitiveQuotientMap e) a) = (primitiveQuotientMap (f e)) (f a)

theorem MagnitudeConjecture.RightModule.PrimitiveIdempotentData.mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] {e : A} (D : PrimitiveIdempotentData e) (f : A ≃ₐ[k] B) : PrimitiveIdempotentData (f e)

Algebra equivalence transports primitive idempotents.