structure ZPlusRingGen (ι : Type u_1) [DecidableEq ι] : Type u_1

A ℤ_+-ring (general version, not requiring ι to be finite): a set ι of distinguished basis elements with nonnegative integer structure constants N i j k satisfying unitality and associativity, and with finite multiplicative support.

• N : ι → ι → ι → ℕ
• I₀ : Finset ι
• finite_support (i j : ι) : {k : ι | self.N i j k ≠ 0}.Finite
• 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 ≠ 0}.Finite ∧ {m : ι | self.N j k m * self.N i m l ≠ 0}.Finite ∧ ∑ᶠ (m : ι), self.N i j m * self.N m k l = ∑ᶠ (m : ι), self.N j k m * self.N i m l

@[reducible, inline]

abbrev Definition_1_42_1 (ι : Type u_1) [DecidableEq ι] : Type u_1

Alias for Definition 1.42.1 of Etingof–Gelaki–Nikshych–Ostrik: a ℤ_+-ring is the general (possibly infinite-index) version ZPlusRingGen.

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

A ℤ_+-ring with finite index set ι: nonnegative integer structure constants N i j k, a unit subset I₀, and the unitality and associativity axioms expressed with ordinary finite sums.

• 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

def ZPlusRingGen.toZPlusRing {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRingGen ι) : ZPlusRing ι

When the index set ι is finite, a general ZPlusRingGen collapses to a ZPlusRing: the finsum associativity becomes an ordinary Finset.sum.

def ZPlusRing.toZPlusRingGen {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) : ZPlusRingGen ι

A ZPlusRing over a finite index set ι can always be regarded as a ZPlusRingGen, since finiteness automatically supplies the finite-support and finsum data.

def ZPlusRing.squaredCoeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) (k : ι) : ℕ

The squared coefficient at k: the total ∑_{i,j} N(i, j, k) of structure constants whose product lands at k. This bounds dimensions of irreducible modules.

noncomputable def ZPlusRing.maxSquaredCoeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) [Nonempty ι] : ℕ

The maximum of R.squaredCoeff k over all basis elements k, which bounds the size of any irreducible ℤ_+-module over R.

theorem ZPlusRing.squaredCoeff_le_maxSquaredCoeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) [Nonempty ι] (k : ι) : R.squaredCoeff k ≤ R.maxSquaredCoeff

Each squared coefficient is bounded by the maximum squared coefficient over ι.

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

A ℤ_+-module over a ℤ_+-ring R: a finite basis set κ together with nonnegative integer action constants act i l k, satisfying unitality from R.I₀ and a compatibility expressing associativity of the action.

• 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

@[reducible, inline]

abbrev Definition_2_8_1 {ι : Type u_2} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) (κ : Type u_3) [DecidableEq κ] [Fintype κ] : Type (max u_2 u_3)

Alias for Definition 2.8.1 of Etingof–Gelaki–Nikshych–Ostrik: a ℤ_+-module over a ℤ_+-ring is what ZPlusModule formalizes.

theorem ZPlusModule.act_unit_self {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (l : κ) : ∑ s ∈ R.I₀, M.act s l l = 1

The diagonal unitality identity for a ℤ_+-module: summing the action of the unit elements s ∈ R.I₀ on l against itself gives 1.

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 ⊆ κ is a ℤ_+-submodule of M if it is closed under the action: M.act i l k ≠ 0 and l ∈ S implies k ∈ S.

• 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

A ℤ_+-module is irreducible if it has no proper nonempty ℤ_+-submodule.

@[reducible, inline]

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

Alias for Definition 2.8.3: irreducibility of a ℤ_+-module.

def ZPlusModule.actCoeffSum {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (i : ι) (l : κ) : ℕ

The sum ∑_{k} act(i, l, k) of action coefficients of i ∈ ι acting on l ∈ κ.

def ZPlusModule.totalActCoeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (l : κ) : ℕ

The total action coefficient at l ∈ κ: the sum over all i ∈ ι of actCoeffSum i l.

theorem ZPlusModule.actCoeffSum_unit {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (l : κ) : ∑ s ∈ R.I₀, M.actCoeffSum s l = 1

Summing actCoeffSum s l over s ∈ R.I₀ gives 1, a consequence of unitality of the ℤ_+-module action.

theorem ZPlusModule.totalActCoeff_le_of_min {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) [Nonempty ι] (l₀ : κ) (hmin : ∀ (n : κ), M.totalActCoeff l₀ ≤ M.totalActCoeff n) : M.totalActCoeff l₀ ≤ R.maxSquaredCoeff

If l₀ ∈ κ minimizes totalActCoeff, then M.totalActCoeff l₀ is bounded by R.maxSquaredCoeff. This is the key inequality underlying Proposition 2.8.7.

theorem ZPlusModule.act_pos_of_irreducible {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (hirr : M.IsIrreducible) (l k : κ) : ∃ (i : ι), 0 < M.act i l k

In an irreducible ℤ_+-module, for every pair l, k ∈ κ there exists some i ∈ ι whose action takes l to a positive coefficient at k.

theorem ZPlusModule.card_le_totalActCoeff_of_irreducible {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (hirr : M.IsIrreducible) (l : κ) : Fintype.card κ ≤ M.totalActCoeff l

For an irreducible ℤ_+-module the cardinality of the basis κ is bounded above by totalActCoeff l for every l ∈ κ.

theorem ZPlusModule.prop_2_8_7 {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (hirr : M.IsIrreducible) [Nonempty ι] [hκ : Nonempty κ] : Fintype.card κ ≤ R.maxSquaredCoeff

Proposition 2.8.7 (Etingof–Gelaki–Nikshych–Ostrik): if M is an irreducible ℤ_+-module over a ℤ_+-ring R, then |κ| ≤ R.maxSquaredCoeff.

def ZPlusModule.regularModule {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : ZPlusRing ι) : ZPlusModule R ι

The regular ℤ_+-module of a ℤ_+-ring R: R acting on its own basis ι via the structure constants N.

structure ZPlusModule.ZPlusModuleHom {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ₁ : Type u_3} {κ₂ : Type u_4} [DecidableEq κ₁] [Fintype κ₁] [DecidableEq κ₂] [Fintype κ₂] (M₁ : ZPlusModule R κ₁) (M₂ : ZPlusModule R κ₂) : Type (max u_3 u_4)

A morphism of ℤ_+-modules over the same ℤ_+-ring R: a nonnegative integer matrix toMatrix : κ₁ → κ₂ → ℕ that intertwines the two actions of R.

• toMatrix : κ₁ → κ₂ → ℕ
• equivariant (i : ι) (l : κ₁) (k₂ : κ₂) : ∑ k₁ : κ₁, M₁.act i l k₁ * self.toMatrix k₁ k₂ = ∑ n : κ₂, self.toMatrix l n * M₂.act i n k₂

structure ZPlusModule.IsIsomorphism {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ₁ : Type u_3} {κ₂ : Type u_4} [DecidableEq κ₁] [Fintype κ₁] [DecidableEq κ₂] [Fintype κ₂] (M₁ : ZPlusModule R κ₁) (M₂ : ZPlusModule R κ₂) : Type (max u_3 u_4)

An isomorphism between two ℤ_+-modules: a bijection of basis sets κ₁ ≃ κ₂ that intertwines the two actions of R.

• equiv : κ₁ ≃ κ₂
• compat (i : ι) (l k : κ₁) : M₁.act i l k = M₂.act i (self.equiv l) (self.equiv k)

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

A ℤ_+-module is indecomposable if its basis κ cannot be split into two nonempty disjoint action-closed subsets covering κ.

theorem ZPlusModule.IsIrreducible.isIndecomposable {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (hirr : M.IsIrreducible) : M.IsIndecomposable

Every irreducible ℤ_+-module is indecomposable: a proper action-closed nonempty subset would contradict irreducibility.

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

Exactness of a ℤ_+-module: whenever act i l k ≠ 0 there exists some j ∈ ι with act j k l ≠ 0, i.e. the action is symmetric up to relabeling.

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 of Etingof–Gelaki–Nikshych–Ostrik: an indecomposable, exact ℤ_+-module is irreducible.

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

A subset S ⊆ κ is action-closed under M if whenever l ∈ S and M.act i l k ≠ 0 we have k ∈ S.

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

An action-closed subset S ⊆ κ is an indecomposable piece if it cannot be partitioned into two nonempty disjoint action-closed subsets.

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

An action-closed subset S ⊆ κ is an irreducible piece if it contains no proper nonempty action-closed subset.

structure ZPlusModule.IsZPlusDecomposition {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (parts : Finset (Finset κ)) : Prop

A ℤ_+-decomposition of M: a finite family of nonempty pairwise disjoint action-closed subsets of κ whose union covers κ.

• covers (k : κ) : ∃ P ∈ parts, k ∈ P
• pairwise_disjoint (P₁ : Finset κ) : P₁ ∈ parts → ∀ P₂ ∈ parts, P₁ ≠ P₂ → Disjoint P₁ P₂
• nonempty (P : Finset κ) : P ∈ parts → P.Nonempty
• closed (P : Finset κ) : P ∈ parts → M.IsActionClosed P

theorem ZPlusModule.decompose_finset_aux {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (S : Finset κ) : S.Nonempty → M.IsActionClosed S → ∃ (parts : Finset (Finset κ)), (∀ (k : κ), k ∈ S ↔ ∃ P ∈ parts, k ∈ P) ∧ (∀ P₁ ∈ parts, ∀ P₂ ∈ parts, P₁ ≠ P₂ → Disjoint P₁ P₂) ∧ (∀ P ∈ parts, P.Nonempty) ∧ (∀ P ∈ parts, M.IsActionClosed P) ∧ ∀ P ∈ parts, M.IsIndecomposablePiece P

Auxiliary recursion lemma: every nonempty action-closed subset S ⊆ κ admits a partition into nonempty pairwise disjoint action-closed indecomposable pieces.

theorem ZPlusModule.exists_indecomposable_decomposition {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) [Nonempty κ] : ∃ (parts : Finset (Finset κ)), M.IsZPlusDecomposition parts ∧ ∀ P ∈ parts, M.IsIndecomposablePiece P

Every ℤ_+-module (with nonempty basis) admits a ℤ_+-decomposition into indecomposable pieces.

theorem ZPlusModule.indecomposable_piece_irreducible_of_exact {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : ZPlusRing ι} {κ : Type u_2} [DecidableEq κ] [Fintype κ] (M : ZPlusModule R κ) (hexact : M.IsExact) (S : Finset κ) (hclosed : M.IsActionClosed S) (hindec : M.IsIndecomposablePiece S) : M.IsIrreduciblePiece S

For exact ℤ_+-modules, every indecomposable piece is automatically irreducible: a proper action-closed subset would split off its complement using exactness.

theorem Proposition_2_8_7 {ι : Type u_3} [DecidableEq ι] [Fintype ι] [Nonempty ι] {R : ZPlusRing ι} {κ : Type u_4} [DecidableEq κ] [Fintype κ] [Nonempty κ] (M : ZPlusModule R κ) (hirr : M.IsIrreducible) : Fintype.card κ ≤ R.maxSquaredCoeff

Proposition 2.8.7 (Etingof–Gelaki–Nikshych–Ostrik): the cardinality of the basis of any irreducible ℤ_+-module is bounded by the maximum squared coefficient of R.