Chosen representatives of indecomposable modules

The manuscript works with a chosen set ind A of representatives rather than with a quotient of all modules by isomorphism. This file packages that choice as a type ι and a family of finitely generated modules indexed by ι.

The structure is not restricted to representation-finite rings. Later finite-type statements add [Finite ι]; the arbitrary-type structural theorems use the same interface without that hypothesis.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.RightFGModule (A : Type u_1) [Ring A] [IsNoetherianRing Aᵐᵒᵖ] : Type (max u_1 (u_2 + 1))

Finitely generated right A-modules, represented using Mathlib's left-module convention over the opposite ring.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton (R : Type u) [Ring R] [IsNoetherianRing R] (ι : Type v) : Type (max (max u v) (w + 1))

A chosen, duplicate-free and complete family of representatives of indecomposable finitely generated R-modules, together with a finite Krull--Schmidt decomposition for every finitely generated module.

The decomposition field is kept explicit as the interface consumed by the later closure arguments. FiniteLengthDecomposition.lean constructs it from finite module length.

• obj : ι → FGModuleCat R
• indecomposable (i : ι) : Foundation.IsIndecomposableModule R ↑(self.obj i)
• finiteLength (i : ι) : IsFiniteLength R ↑(self.obj i)
• eq_of_iso {i j : ι} : Nonempty (self.obj i ≅ self.obj j) → i = j
• complete (X : FGModuleCat R) : Foundation.IsIndecomposableModule R ↑X → ∃ (i : ι), Nonempty (X ≅ self.obj i)
• decomposes (X : FGModuleCat R) : ∃ (n : ℕ) (a : Fin n → ι), Nonempty (X ≅ ⨁ fun (t : Fin n) => self.obj (a t))

structure QuotientSubmoduleEquidistribution.FiniteIndecomposableSkeleton (R : Type u) [Ring R] [IsNoetherianRing R] : Type (max (max u (v + 1)) (w + 1))

A finite chosen skeleton, with its representative type bundled. The index and module universes intentionally occur together in the bundled IndecomposableSkeleton.

• ι : Type v
• finite_ι : Finite self.ι
• skeleton : IndecomposableSkeleton R self.ι

instance QuotientSubmoduleEquidistribution.FiniteIndecomposableSkeleton.instFiniteι {R : Type u} [Ring R] [IsNoetherianRing R] (M : FiniteIndecomposableSkeleton R) : Finite M.ι

@[reducible, inline]

noncomputable abbrev QuotientSubmoduleEquidistribution.IndecomposableSkeleton.sum {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) (n : ℕ) (a : Fin n → ι) : FGModuleCat R

The finite direct sum of the representatives indexed by a.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.eq_iff_nonempty_iso {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) {i j : ι} : i = j ↔ Nonempty (σ.obj i ≅ σ.obj j)

The chosen representative family has no isomorphic duplicates.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.obj_injective {R : Type u} [Ring R] [IsNoetherianRing R] {ι : Type v} (σ : IndecomposableSkeleton R ι) : Function.Injective σ.obj

Equality of chosen representative objects forces equality of their indices.