Modules over the primitive quotient

This file identifies finitely generated right modules over the manuscript's literal primitive quotient A/AeA with the full subcategory of ambient right A-modules annihilated by AeA. The auxiliary quotient of Aᵐᵒᵖ is used only to apply Mathlib's quotient-module API; an explicit algebra equivalence returns every public categorical statement to (A/AeA)ᵐᵒᵖ.

def MagnitudeConjecture.RightModule.primitiveLeftIdeal {A : Type u} [Ring A] (e : A) : TwoSidedIdeal Aᵐᵒᵖ

The opposite two-sided ideal used to construct right quotient modules through Mathlib's left-module quotient API.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.PrimitiveLeftQuotient {A : Type u} [Ring A] (e : A) : Type u

The auxiliary left-module quotient of Aᵐᵒᵖ.

def MagnitudeConjecture.RightModule.primitiveQuotientAlgMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) : A →ₐ[k] primitiveQuotientAlgebra e

The canonical algebra map A ⟶ A/AeA.

def MagnitudeConjecture.RightModule.primitiveQuotientOpAlgMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) : Aᵐᵒᵖ →ₐ[k] (primitiveQuotientAlgebra e)ᵐᵒᵖ

The opposite quotient map, used to inflate right A/AeA-modules to right A-modules.

theorem MagnitudeConjecture.RightModule.primitiveQuotientOpAlgMap_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : RingHom.ker (primitiveQuotientOpAlgMap e) = TwoSidedIdeal.asIdeal (primitiveLeftIdeal e)

theorem MagnitudeConjecture.RightModule.primitiveQuotientOpAlgMap_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) : Function.Surjective ⇑(primitiveQuotientOpAlgMap e)

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftQuotientAlgEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : PrimitiveLeftQuotient e ≃ₐ[k] (primitiveQuotientAlgebra e)ᵐᵒᵖ

The auxiliary quotient of Aᵐᵒᵖ is canonically the opposite of the manuscript's literal quotient A/AeA.

instance MagnitudeConjecture.RightModule.primitiveLeftQuotientModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : Module.Finite k (PrimitiveLeftQuotient e)

instance MagnitudeConjecture.RightModule.primitiveQuotientOpModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : Module.Finite k (primitiveQuotientAlgebra e)ᵐᵒᵖ

instance MagnitudeConjecture.RightModule.primitiveQuotientModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : Module.Finite k (primitiveQuotientAlgebra e)

The literal primitive quotient is finite-dimensional on the original algebra side as well as on its opposite.

theorem MagnitudeConjecture.RightModule.isTorsionByPrimitiveLeftIdeal {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : Module.IsTorsionBySet Aᵐᵒᵖ ↑M ↑(TwoSidedIdeal.asIdeal (primitiveLeftIdeal e))

An ambient right module annihilated by AeA is a module over the auxiliary quotient of Aᵐᵒᵖ.

def MagnitudeConjecture.RightModule.PrimitiveQuotientProperty {A : Type u} [Ring A] (e : A) : CategoryTheory.ObjectProperty (FinitelyGeneratedCategory A)

The full subcategory of ambient right modules annihilated by AeA.

instance MagnitudeConjecture.RightModule.primitiveQuotientProperty_stableUnderRetracts {A : Type u} [Ring A] (e : A) : (PrimitiveQuotientProperty e).IsStableUnderRetracts

Annihilation by the primitive ideal is inherited by direct summands.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.PrimitiveQuotientSubcategory {A : Type u} [Ring A] (e : A) : Type (u + 1)

The ambient realization of the finitely generated right A/AeA-module category.

def MagnitudeConjecture.RightModule.primitiveLeftObj {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : ModuleCat (PrimitiveLeftQuotient e)

An annihilated ambient module, regarded as a module over the auxiliary left quotient.

def MagnitudeConjecture.RightModule.primitiveLeftObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : ↑M ≃ₗ[k] ↑(primitiveLeftObj e M hM)

Passing to the auxiliary quotient does not change the underlying finite-dimensional k-vector space.

def MagnitudeConjecture.RightModule.primitiveLeftObjRestrictIso {A : Type u} [Ring A] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (primitiveLeftIdeal e)))).obj (primitiveLeftObj e M hM) ≅ M.obj

Restriction from the auxiliary quotient recovers the original ambient module by the identity on its carrier.

def MagnitudeConjecture.RightModule.primitiveLeftMap {A : Type u} [Ring A] (e : A) (M N : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) (hN : IsAnnihilatedBy (primitiveIdeal e) N) (f : M ⟶ N) : primitiveLeftObj e M hM ⟶ primitiveLeftObj e N hN

Every ambient morphism between annihilated modules is linear over the auxiliary quotient.

@[simp]

theorem MagnitudeConjecture.RightModule.primitiveLeftMap_apply {A : Type u} [Ring A] (e : A) (M N : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) (hN : IsAnnihilatedBy (primitiveIdeal e) N) (f : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (primitiveLeftMap e M N hM hN f)) m = (CategoryTheory.ConcreteCategory.hom f) m

def MagnitudeConjecture.RightModule.primitiveLeftFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy (primitiveIdeal e) M) : FGModuleCat (PrimitiveLeftQuotient e)

The auxiliary quotient object bundled in the finitely generated module category.

def MagnitudeConjecture.RightModule.primitiveLeftFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor (PrimitiveQuotientSubcategory e) (FGModuleCat (PrimitiveLeftQuotient e))

Passage from the annihilated ambient subcategory to modules over the auxiliary quotient.

instance MagnitudeConjecture.RightModule.primitiveLeftFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : (primitiveLeftFunctor e).Additive

The quotient realization functor preserves the preadditive structure.

instance MagnitudeConjecture.RightModule.primitiveLeftFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor.Linear k (primitiveLeftFunctor e)

Passage to the auxiliary quotient is linear over the ground field.

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftInflateFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) (N : FGModuleCat (PrimitiveLeftQuotient e)) : FinitelyGeneratedCategory A

Inflate an auxiliary quotient module to an ambient finitely generated right A-module.

theorem MagnitudeConjecture.RightModule.primitiveLeftInflateFGObj_isAnnihilatedBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) (N : FGModuleCat (PrimitiveLeftQuotient e)) : IsAnnihilatedBy (primitiveIdeal e) (primitiveLeftInflateFGObj e N)

Inflation along the auxiliary quotient is annihilated by AeA.

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftInflateFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor (FGModuleCat (PrimitiveLeftQuotient e)) (PrimitiveQuotientSubcategory e)

Inflation along the auxiliary quotient, bundled in the annihilated full subcategory.

instance MagnitudeConjecture.RightModule.primitiveLeftInflateFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : (primitiveLeftInflateFunctor e).Additive

Inflation from the quotient preserves the preadditive structure.

instance MagnitudeConjecture.RightModule.primitiveLeftInflateFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor.Linear k (primitiveLeftInflateFunctor e)

Inflation from the auxiliary quotient is linear over the ground field.

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftUnitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) (M : PrimitiveQuotientSubcategory e) : M ≅ ((primitiveLeftFunctor e).comp (primitiveLeftInflateFunctor e)).obj M

Unit component for the auxiliary primitive-quotient equivalence.

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftCounitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) (N : FGModuleCat (PrimitiveLeftQuotient e)) : ((primitiveLeftInflateFunctor e).comp (primitiveLeftFunctor e)).obj N ≅ N

Counit component for the auxiliary primitive-quotient equivalence.

noncomputable def MagnitudeConjecture.RightModule.primitiveLeftEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : PrimitiveQuotientSubcategory e ≌ FGModuleCat (PrimitiveLeftQuotient e)

Modules over the auxiliary quotient are equivalent to annihilated ambient modules.

instance MagnitudeConjecture.RightModule.primitiveLeftEquivalenceFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor.Linear k (primitiveLeftEquivalence e).functor

instance MagnitudeConjecture.RightModule.primitiveLeftEquivalenceInverseLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (e : A) : CategoryTheory.Functor.Linear k (primitiveLeftEquivalence e).inverse

noncomputable def MagnitudeConjecture.RightModule.primitiveQuotientEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : PrimitiveQuotientSubcategory e ≌ FinitelyGeneratedCategory (primitiveQuotientAlgebra e)

Finitely generated right modules over the manuscript's literal A/AeA are equivalent to the full ambient subcategory annihilated by AeA.

instance MagnitudeConjecture.RightModule.primitiveQuotientEquivalenceFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : (primitiveQuotientEquivalence e).functor.Additive

The literal primitive-quotient equivalence preserves addition on morphisms.

instance MagnitudeConjecture.RightModule.primitiveQuotientEquivalenceInverseAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : (primitiveQuotientEquivalence e).inverse.Additive

The inverse literal primitive-quotient equivalence preserves addition on morphisms.

instance MagnitudeConjecture.RightModule.primitiveQuotientEquivalenceFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : CategoryTheory.Functor.Linear k (primitiveQuotientEquivalence e).functor

The literal primitive-quotient equivalence is linear over the ground field.

instance MagnitudeConjecture.RightModule.primitiveQuotientEquivalenceInverseLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : CategoryTheory.Functor.Linear k (primitiveQuotientEquivalence e).inverse

The inverse literal primitive-quotient equivalence is linear over the ground field.

theorem MagnitudeConjecture.RightModule.primitiveQuotientSubcategory_epi_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) {M N : PrimitiveQuotientSubcategory e} (f : M ⟶ N) [CategoryTheory.Epi f] : CategoryTheory.Epi f.hom

Epimorphisms in the annihilated full subcategory are already epimorphisms of ambient finitely generated right modules.

theorem MagnitudeConjecture.RightModule.primitiveQuotient_isRepresentationFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (hA : IsRepresentationFinite k A) (e : A) : IsRepresentationFinite k (primitiveQuotientAlgebra e)

Representation-finiteness descends to the manuscript's literal primitive quotient.