Right modules over an arbitrary two-sided quotient

For a two-sided ideal I ⊆ A, finitely generated right modules over A/I are the same as finitely generated right A-modules annihilated by I. Mathlib's quotient-module API is phrased for left modules, so the construction first uses the quotient of Aᵐᵒᵖ by I.op and then transports across the canonical algebra equivalence with (A/I)ᵐᵒᵖ.

This is the ideal-independent categorical boundary needed for socle rejection. It also isolates the common part of the existing primitive and support quotient constructions without imposing either of their additional combinatorial hypotheses.

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

The opposite ideal through which right modules annihilated by I acquire their quotient action.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.IdealLeftQuotient {A : Type u} [Ring A] (I : TwoSidedIdeal A) : Type u

The auxiliary quotient acting on the left on right A-modules.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.idealQuotientAlgebra {A : Type u} [Ring A] (I : TwoSidedIdeal A) : Type u

The literal quotient algebra A/I.

def MagnitudeConjecture.RightModule.idealQuotientAlgMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (I : TwoSidedIdeal A) : A →ₐ[k] idealQuotientAlgebra I

The canonical algebra map A ⟶ A/I.

def MagnitudeConjecture.RightModule.idealQuotientOpAlgMap {k A : Type u} [Field k] [Ring A] [Algebra k A] (I : TwoSidedIdeal A) : Aᵐᵒᵖ →ₐ[k] (idealQuotientAlgebra I)ᵐᵒᵖ

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

theorem MagnitudeConjecture.RightModule.idealQuotientOpAlgMap_ker {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : RingHom.ker (idealQuotientOpAlgMap I) = TwoSidedIdeal.asIdeal (idealLeftIdeal I)

theorem MagnitudeConjecture.RightModule.idealQuotientOpAlgMap_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] (I : TwoSidedIdeal A) : Function.Surjective ⇑(idealQuotientOpAlgMap I)

noncomputable def MagnitudeConjecture.RightModule.idealLeftQuotientAlgEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : IdealLeftQuotient I ≃ₐ[k] (idealQuotientAlgebra I)ᵐᵒᵖ

The quotient of Aᵐᵒᵖ by I.op is canonically the opposite of the literal quotient A/I.

instance MagnitudeConjecture.RightModule.idealLeftQuotientModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : Module.Finite k (IdealLeftQuotient I)

instance MagnitudeConjecture.RightModule.idealQuotientOpModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : Module.Finite k (idealQuotientAlgebra I)ᵐᵒᵖ

instance MagnitudeConjecture.RightModule.idealQuotientModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : Module.Finite k (idealQuotientAlgebra I)

theorem MagnitudeConjecture.RightModule.isTorsionByIdealLeftIdeal {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : Module.IsTorsionBySet Aᵐᵒᵖ ↑M ↑(TwoSidedIdeal.asIdeal (idealLeftIdeal I))

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

def MagnitudeConjecture.RightModule.IdealQuotientProperty {A : Type u} [Ring A] (I : TwoSidedIdeal A) : CategoryTheory.ObjectProperty (FinitelyGeneratedCategory A)

The full subcategory of ambient right modules annihilated by I.

instance MagnitudeConjecture.RightModule.idealQuotientProperty_closedUnderSubobjects {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : (IdealQuotientProperty I).IsClosedUnderSubobjects

Annihilation by a two-sided ideal is inherited by subobjects.

instance MagnitudeConjecture.RightModule.idealQuotientProperty_stableUnderRetracts {A : Type u} [Ring A] (I : TwoSidedIdeal A) : (IdealQuotientProperty I).IsStableUnderRetracts

Annihilation by a two-sided ideal is inherited by direct summands.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.IdealQuotientSubcategory {A : Type u} [Ring A] (I : TwoSidedIdeal A) : Type (u + 1)

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

def MagnitudeConjecture.RightModule.idealLeftObj {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : ModuleCat (IdealLeftQuotient I)

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

def MagnitudeConjecture.RightModule.idealLeftObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : ↑M ≃ₗ[k] ↑(idealLeftObj I M hM)

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

def MagnitudeConjecture.RightModule.idealLeftObjRestrictIso {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (idealLeftIdeal I)))).obj (idealLeftObj I M hM) ≅ M.obj

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

def MagnitudeConjecture.RightModule.idealLeftMap {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M N : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) (hN : IsAnnihilatedBy I N) (f : M ⟶ N) : idealLeftObj I M hM ⟶ idealLeftObj I N hN

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

@[simp]

theorem MagnitudeConjecture.RightModule.idealLeftMap_apply {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M N : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) (hN : IsAnnihilatedBy I N) (f : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (idealLeftMap I M N hM hN f)) m = (CategoryTheory.ConcreteCategory.hom f) m

def MagnitudeConjecture.RightModule.idealLeftFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : FGModuleCat (IdealLeftQuotient I)

The quotient object bundled in the finitely generated module category.

def MagnitudeConjecture.RightModule.idealLeftFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor (IdealQuotientSubcategory I) (FGModuleCat (IdealLeftQuotient I))

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

instance MagnitudeConjecture.RightModule.idealLeftFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : (idealLeftFunctor I).Additive

instance MagnitudeConjecture.RightModule.idealLeftFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealLeftFunctor I)

noncomputable def MagnitudeConjecture.RightModule.idealLeftInflateFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) (N : FGModuleCat (IdealLeftQuotient I)) : FinitelyGeneratedCategory A

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

theorem MagnitudeConjecture.RightModule.idealLeftInflateFGObj_isAnnihilatedBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) (N : FGModuleCat (IdealLeftQuotient I)) : IsAnnihilatedBy I (idealLeftInflateFGObj I N)

Inflation along the auxiliary quotient is annihilated by I.

noncomputable def MagnitudeConjecture.RightModule.idealLeftInflateFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor (FGModuleCat (IdealLeftQuotient I)) (IdealQuotientSubcategory I)

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

instance MagnitudeConjecture.RightModule.idealLeftInflateFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : (idealLeftInflateFunctor I).Additive

instance MagnitudeConjecture.RightModule.idealLeftInflateFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealLeftInflateFunctor I)

noncomputable def MagnitudeConjecture.RightModule.idealLeftUnitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) (M : IdealQuotientSubcategory I) : M ≅ ((idealLeftFunctor I).comp (idealLeftInflateFunctor I)).obj M

Unit component of the arbitrary ideal-quotient equivalence.

noncomputable def MagnitudeConjecture.RightModule.idealLeftCounitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) (N : FGModuleCat (IdealLeftQuotient I)) : ((idealLeftInflateFunctor I).comp (idealLeftFunctor I)).obj N ≅ N

Counit component of the arbitrary ideal-quotient equivalence.

noncomputable def MagnitudeConjecture.RightModule.idealLeftEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : IdealQuotientSubcategory I ≌ FGModuleCat (IdealLeftQuotient I)

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

instance MagnitudeConjecture.RightModule.idealLeftEquivalenceFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealLeftEquivalence I).functor

instance MagnitudeConjecture.RightModule.idealLeftEquivalenceInverseLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealLeftEquivalence I).inverse

noncomputable def MagnitudeConjecture.RightModule.idealQuotientEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : IdealQuotientSubcategory I ≌ FinitelyGeneratedCategory (idealQuotientAlgebra I)

Finitely generated right modules over A/I are equivalent to the full ambient subcategory annihilated by I.

instance MagnitudeConjecture.RightModule.idealQuotientEquivalenceFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : (idealQuotientEquivalence I).functor.Additive

instance MagnitudeConjecture.RightModule.idealQuotientEquivalenceInverseAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : (idealQuotientEquivalence I).inverse.Additive

instance MagnitudeConjecture.RightModule.idealQuotientEquivalenceFunctorLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealQuotientEquivalence I).functor

instance MagnitudeConjecture.RightModule.idealQuotientEquivalenceInverseLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : CategoryTheory.Functor.Linear k (idealQuotientEquivalence I).inverse

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_epi_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {M N : IdealQuotientSubcategory I} (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.idealQuotient_isRepresentationFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (hA : IsRepresentationFinite k A) (I : TwoSidedIdeal A) : IsRepresentationFinite k (idealQuotientAlgebra I)

Representation-finiteness descends to every literal two-sided quotient.