The maximal submodule annihilated by a two-sided ideal

For a two-sided ideal I and a finitely generated right A-module M, this file constructs the largest submodule of M annihilated by I. Bundled in the annihilated full subcategory, this is the right adjoint needed to restrict ambient right almost-split maps to mod (A/I).

theorem MagnitudeConjecture.RightModule.isAnnihilatedBy_biproduct {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {J : Type} [Fintype J] (F : J → FinitelyGeneratedCategory A) (hF : ∀ (j : J), IsAnnihilatedBy I (F j)) : IsAnnihilatedBy I (⨁ F)

A finite biproduct of modules annihilated by I is again annihilated by I.

def MagnitudeConjecture.RightModule.idealTorsionSubmodule {A : Type u} [Ring A] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) : Submodule Aᵐᵒᵖ ↑M

The largest submodule of M annihilated by the two-sided ideal I.

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

The maximal annihilated submodule as a finitely generated ambient right module.

def MagnitudeConjecture.RightModule.idealTorsionInclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) : idealTorsionFGObj I M ⟶ M

The canonical inclusion of the maximal annihilated submodule.

instance MagnitudeConjecture.RightModule.idealTorsionInclusion_mono {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) : CategoryTheory.Mono (idealTorsionInclusion I M)

theorem MagnitudeConjecture.RightModule.idealTorsionFGObj_isAnnihilatedBy {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) : IsAnnihilatedBy I (idealTorsionFGObj I M)

The maximal torsion object is annihilated by I.

def MagnitudeConjecture.RightModule.idealTorsionSubcategoryObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) : IdealQuotientSubcategory I

The maximal torsion object bundled in the annihilated full subcategory.

def MagnitudeConjecture.RightModule.idealTorsionMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) : idealTorsionFGObj I M ⟶ idealTorsionFGObj I N

An ambient morphism restricts to the maximal annihilated submodules.

@[simp]

theorem MagnitudeConjecture.RightModule.idealTorsionMap_apply {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) (x : ↑(idealTorsionFGObj I M)) : ↑((CategoryTheory.ConcreteCategory.hom (idealTorsionMap I f)) x) = (CategoryTheory.ConcreteCategory.hom f) ↑x

theorem MagnitudeConjecture.RightModule.idealTorsionMap_comp_inclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {M N : FinitelyGeneratedCategory A} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (idealTorsionMap I f) (idealTorsionInclusion I N) = CategoryTheory.CategoryStruct.comp (idealTorsionInclusion I M) f

Restriction commutes with the canonical inclusions.

def MagnitudeConjecture.RightModule.idealTorsionFunctor {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : CategoryTheory.Functor (FinitelyGeneratedCategory A) (FinitelyGeneratedCategory A)

The maximal-annihilated-submodule construction is functorial.

instance MagnitudeConjecture.RightModule.idealTorsionFunctor_additive {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : (idealTorsionFunctor I).Additive

def MagnitudeConjecture.RightModule.idealTorsionLift {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {X M : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy I X) (f : X ⟶ M) : X ⟶ idealTorsionFGObj I M

Every map from an I-annihilated module factors canonically through the maximal annihilated submodule of its target.

@[simp]

theorem MagnitudeConjecture.RightModule.idealTorsionLift_comp_inclusion {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {X M : FinitelyGeneratedCategory A} (hX : IsAnnihilatedBy I X) (f : X ⟶ M) : CategoryTheory.CategoryStruct.comp (idealTorsionLift I hX f) (idealTorsionInclusion I M) = f

def MagnitudeConjecture.RightModule.idealTorsionIsoOfIsAnnihilated {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : FinitelyGeneratedCategory A) (hM : IsAnnihilatedBy I M) : idealTorsionFGObj I M ≅ M

On an annihilated module, the maximal torsion inclusion is an isomorphism.

def MagnitudeConjecture.RightModule.idealTorsionTargetMap {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy I N) (q : E ⟶ N) : idealTorsionSubcategoryObj I E ⟶ { obj := N, property := hN }

Restrict an ambient map to the maximal annihilated submodule of its source when the target is annihilated by I.

noncomputable def MagnitudeConjecture.RightModule.idealTorsionTargetKernelIso {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy I N) (q : E ⟶ N) (hK : IsAnnihilatedBy I (CategoryTheory.Limits.kernel q)) : CategoryTheory.Limits.kernel (idealTorsionTargetMap I hN q) ≅ { obj := CategoryTheory.Limits.kernel q, property := hK }

If the ambient kernel of a map to an annihilated target is itself annihilated, then it is also the kernel after restricting the source to its maximal annihilated submodule.

theorem MagnitudeConjecture.RightModule.idealTorsionTargetMap_isRightAlmostSplit {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hN : IsAnnihilatedBy I N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (idealTorsionTargetMap I hN q)

The right adjoint to the annihilated full-subcategory inclusion carries an ambient right almost-split map to a right almost-split map.

theorem MagnitudeConjecture.RightModule.idealTorsionTargetMap_isRightMinimal_of_source_isAnnihilatedBy {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hE : IsAnnihilatedBy I E) (hN : IsAnnihilatedBy I N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightMinimal q) : QuotientSubmoduleEquidistribution.IsRightMinimal (idealTorsionTargetMap I hN q)

If the ambient source is already annihilated, restricting an ambient right-minimal map preserves right minimality.

noncomputable def MagnitudeConjecture.RightModule.idealTorsionSourceDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (E : FinitelyGeneratedCategory A) (d : CategoryTheory.FiniteIndecomposableDecomposition (idealTorsionFGObj I E)) (hsummand : ∀ (i : Fin d.n), IsAnnihilatedBy I (d.summand i)) : CategoryTheory.FiniteIndecomposableDecomposition ((idealQuotientEquivalence I).functor.obj (idealTorsionSubcategoryObj I E))

A displayed decomposition of a maximal annihilated source transports to the corresponding object over the literal quotient algebra.

noncomputable def MagnitudeConjecture.RightModule.idealTorsionTargetSourceDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (E : FinitelyGeneratedCategory A) (hE : IsAnnihilatedBy I E) (d : CategoryTheory.FiniteIndecomposableDecomposition E) (hsummand : ∀ (i : Fin d.n), IsAnnihilatedBy I (d.summand i)) : CategoryTheory.FiniteIndecomposableDecomposition ((idealQuotientEquivalence I).functor.obj (idealTorsionSubcategoryObj I E))

An explicit ambient decomposition whose summands are annihilated by I transports to a decomposition of the right-adjoint sink source over the literal quotient algebra, with the same number of summands.

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_enoughProjectives {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) : CategoryTheory.EnoughProjectives (IdealQuotientSubcategory I)

The full subcategory annihilated by an arbitrary ideal has enough projectives, transported from finitely generated modules over the literal quotient algebra.

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_projective_of_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : IdealQuotientSubcategory I) (hM : CategoryTheory.Projective M.obj) : CategoryTheory.Projective M

A projective ambient module which is annihilated by I remains projective in the full annihilated subcategory.

theorem MagnitudeConjecture.RightModule.idealQuotientFGObj_projective_of_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (M : FinitelyGeneratedCategory A) (hAnn : IsAnnihilatedBy I M) (hM : CategoryTheory.Projective M) : CategoryTheory.Projective ((idealQuotientEquivalence I).functor.obj { obj := M, property := hAnn })

Transporting an annihilated ambient projective through the literal ideal-quotient equivalence produces a projective quotient module.

theorem MagnitudeConjecture.RightModule.idealQuotientSubcategory_injective_of_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : IdealQuotientSubcategory I) (hM : CategoryTheory.Injective M.obj) : CategoryTheory.Injective M

An injective ambient module which is annihilated by I remains injective in the full annihilated subcategory.

theorem MagnitudeConjecture.RightModule.idealQuotientFGObj_injective_of_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (M : FinitelyGeneratedCategory A) (hAnn : IsAnnihilatedBy I M) (hM : CategoryTheory.Injective M) : CategoryTheory.Injective ((idealQuotientEquivalence I).functor.obj { obj := M, property := hAnn })

Transporting an annihilated ambient injective through the literal ideal-quotient equivalence produces an injective quotient module.

theorem MagnitudeConjecture.RightModule.idealTorsionTargetMap_mono_iff_of_source_isAnnihilatedBy {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hE : IsAnnihilatedBy I E) (hN : IsAnnihilatedBy I N) (q : E ⟶ N) : CategoryTheory.Mono (idealTorsionTargetMap I hN q) ↔ CategoryTheory.Mono q

If the ambient source is already annihilated, the restricted sink map is monic exactly when the ambient sink map is monic.

theorem MagnitudeConjecture.RightModule.idealQuotient_projective_iff_of_minimal_sink_source_isAnnihilatedBy {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) {E N : FinitelyGeneratedCategory A} (hE : IsAnnihilatedBy I E) (hN : IsAnnihilatedBy I N) (q : E ⟶ N) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit q) (hqmin : QuotientSubmoduleEquidistribution.IsRightMinimal q) : CategoryTheory.Projective { obj := N, property := hN } ↔ CategoryTheory.Projective N

When a minimal ambient sink has annihilated source and target, passing to the ideal quotient preserves and reflects projectivity of its target.