structure ZPlusRing' (ι : Type u_1) [DecidableEq ι] [Fintype ι] : Type u_1

Auxiliary, "primed" version of a ℤ₊-ring used by the standalone development of Lemma 2.8.5. Mirrors ZPlusRing with structure constants N : ι → ι → ι → ℕ, a unit support I₀ : Finset ι and the usual unit and associativity axioms.

• 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 ZPlusModule' {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing' ι) (κ : Type u_2) [DecidableEq κ] [Fintype κ] : Type (max u_1 u_2)

Auxiliary, "primed" version of a ℤ₊-module over a ZPlusRing', used by the standalone development of Lemma 2.8.5. Records action constants act : ι → κ → κ → ℕ and the usual unit and compatibility axioms.

• 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 ZPlusModule'.IsZPlusSubmodule' {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing' ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule' R κ) (S : Finset κ) : Prop

A nonempty proper subset S of basis elements that is closed under the ℤ₊-module action constitutes a ℤ₊-submodule of M (primed variant).

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

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

M is irreducible (primed variant) if it has no nontrivial ℤ₊-submodule.

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

M is indecomposable (primed variant) if there is no partition of its basis into two nonempty disjoint subsets, each closed under the action.

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

M is exact (primed variant) if whenever act i l k ≠ 0 there is some j such that act j k l ≠ 0; this is the combinatorial analogue of exactness from EGNO.

theorem ZPlusModule'.lemma_2_8_5' {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing' ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule' R κ) (hindec : M.IsIndecomposable') (hexact : M.IsExact') : M.IsIrreducible'

Lemma 2.8.5 (EGNO), primed/standalone version. An indecomposable exact ℤ₊-module is irreducible: the complement of any proper closed subset cannot fail to also be closed by exactness, contradicting indecomposability.