Regular right modules and complete idempotent decompositions

A complete orthogonal family of idempotents decomposes the regular right module as the finite biproduct of its principal right ideals. The explicit maps here are shared by support quotients and primitive deletion.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.rightRegularFGObj {B : Type u} [Ring B] : FinitelyGeneratedCategory B

The regular right module as a literal finitely generated object.

def MagnitudeConjecture.RightModule.rightIdealInclusion {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (e : B) : rightIdealFGObj e ⟶ rightRegularFGObj

The literal inclusion eB → B.

def MagnitudeConjecture.RightModule.rightIdealProjection {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (e : B) : rightRegularFGObj ⟶ rightIdealFGObj e

Left multiplication by e, as the projection B → eB.

@[simp]

theorem MagnitudeConjecture.RightModule.rightIdealInclusion_apply_val {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (e : B) (y : ↑(rightIdealFGObj e)) : (ModuleCat.Hom.hom (rightIdealInclusion e).hom) y = ↑y

@[simp]

theorem MagnitudeConjecture.RightModule.rightIdealProjection_apply_val {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] (e : B) (y : ↑rightRegularFGObj) : ↑((ModuleCat.Hom.hom (rightIdealProjection e).hom) y) = e * y

theorem MagnitudeConjecture.RightModule.exists_fin_free_epimorphism {B : Type u} [Ring B] (X : FinitelyGeneratedCategory B) : ∃ (n : ℕ) (q : FGModuleCat.of Bᵐᵒᵖ (Fin n → Bᵐᵒᵖ) ⟶ X), CategoryTheory.Epi q

Every finitely generated right module is a quotient of a finite free right module, with the source kept explicit for additive-closure arguments.

noncomputable def MagnitudeConjecture.RightModule.regularDecompositionMap {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {I : Type} [Fintype I] (idempotent : I → B) : rightRegularFGObj ⟶ ⨁ fun (i : I) => rightIdealFGObj (idempotent i)

Project the regular module to all right ideals in an idempotent family.

noncomputable def MagnitudeConjecture.RightModule.regularAssemblyMap {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {I : Type} [Fintype I] (idempotent : I → B) : (⨁ fun (i : I) => rightIdealFGObj (idempotent i)) ⟶ rightRegularFGObj

Assemble the right ideals in an idempotent family into the regular module.

theorem MagnitudeConjecture.RightModule.regularDecompositionMap_comp_assemblyMap {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {I : Type} [Fintype I] (idempotent : I → B) (h : CompleteOrthogonalIdempotents idempotent) : CategoryTheory.CategoryStruct.comp (regularDecompositionMap idempotent) (regularAssemblyMap idempotent) = CategoryTheory.CategoryStruct.id rightRegularFGObj

Completeness makes regular decomposition followed by assembly the identity.

theorem MagnitudeConjecture.RightModule.regularAssemblyMap_comp_decompositionMap {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {I : Type} [Fintype I] (idempotent : I → B) (h : CompleteOrthogonalIdempotents idempotent) : CategoryTheory.CategoryStruct.comp (regularAssemblyMap idempotent) (regularDecompositionMap idempotent) = CategoryTheory.CategoryStruct.id (⨁ fun (i : I) => rightIdealFGObj (idempotent i))

Orthogonality makes assembly followed by regular decomposition the identity on the biproduct of principal right ideals.

noncomputable def MagnitudeConjecture.RightModule.regularDecompositionIso {B : Type u} [Ring B] [IsNoetherianRing Bᵐᵒᵖ] {I : Type} [Fintype I] (idempotent : I → B) (h : CompleteOrthogonalIdempotents idempotent) : rightRegularFGObj ≅ ⨁ fun (i : I) => rightIdealFGObj (idempotent i)

The regular right module is the biproduct of the principal right ideals from any complete orthogonal idempotent family.