structure ZPlusRingIrr (ι : Type u_1) [DecidableEq ι] [Fintype ι] : Type u_1

A combinatorial ℤ₊-ring on the basis ι: nonnegative structure constants N, a distinguished set I₀ whose sum is the unit, and associativity.

• N : ι → ι → ι → ℕ
• I₀ : Finset ι
• unit_mul (j k : ι) : ∑ s ∈ self.I₀, self.N s j k = if j = k then 1 else 0
• mul_unit (i k : ι) : ∑ s ∈ self.I₀, self.N i s k = if i = k then 1 else 0
• assoc (i j k l : ι) : ∑ m : ι, self.N i j m * self.N m k l = ∑ m : ι, self.N j k m * self.N i m l

structure ZPlusModuleIrr {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRingIrr ι) (κ : Type u_2) [DecidableEq κ] [Fintype κ] : Type (max u_1 u_2)

A ℤ₊-module over a ZPlusRingIrr, indexed by a basis κ, with nonnegative action constants compatible with the unit and with the multiplication of R.

• act : ι → κ → κ → ℕ
• act_unit (l k : κ) : ∑ s ∈ R.I₀, self.act s l k = if l = k then 1 else 0
• act_compat (i j : ι) (l k : κ) : ∑ m : ι, R.N i j m * self.act m l k = ∑ n : κ, self.act j l n * self.act i n k

structure ZPlusModuleIrr.IsZPlusSubmodule {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRingIrr ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModuleIrr R κ) (S : Finset κ) : Prop

A subset S ⊆ κ is a proper nontrivial ℤ₊-submodule of M if it is nonempty, not all of κ, and closed under the action of every basis element of the ring.

• nonempty : S.Nonempty
• proper : S ≠ Finset.univ
• closed (i : ι) (l : κ) : l ∈ S → ∀ (k : κ), M.act i l k ≠ 0 → k ∈ S

def ZPlusModuleIrr.IsIrreducible {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRingIrr ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModuleIrr R κ) : Prop

The ℤ₊-module M is irreducible if it admits no proper ℤ₊-submodule.

def ZPlusModuleIrr.IsIndecomposable {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRingIrr ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModuleIrr R κ) : Prop

The ℤ₊-module M is indecomposable if κ cannot be partitioned into two nonempty disjoint subsets each closed under the action.

def ZPlusModuleIrr.IsExact {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRingIrr ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModuleIrr R κ) : Prop

The ℤ₊-module M is exact if whenever some basis element of the ring sends l to k with nonzero coefficient, there is also a basis element sending k back to l.

theorem ZPlusModuleIrr.Lemma_2_8_5 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRingIrr ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModuleIrr R κ) (hindec : M.IsIndecomposable) (hexact : M.IsExact) : M.IsIrreducible

Lemma 2.8.5: An indecomposable exact ℤ₊-module is irreducible — any proper closed subset would give a partition of κ violating indecomposability.