Documentation

Formalizations.NumberTheory.NumericalSemigroup.GenusThree

Submonoids of ℕ with exactly three gaps #

A submonoid of ℕ with exactly three gaps has gap set {1,2,3}, {1,2,4}, {1,2,5} or {1,3,5}, i.e. it is ⟨4,5,6,7⟩, ⟨3,5,7⟩, ⟨3,4⟩ or ⟨2,7⟩ (classical, Rosales–García-Sánchez; Lemma 4 of «The order generated by a column of the SU(n)ₖ S-matrix», Part II). Every gap is at most 2δ − 1 = 5 (P3b.gap_le_two_mul_genus_sub_one), 1 is a gap, sums of non-gaps are not gaps, and a finite case analysis (decide over the subsets of {1,…,5}) leaves the four sets.

Main results #

References #

theorem P3a.zero_not_mem_gaps (A : Set ℕ) :
0 ∉ gaps A

No gap: 0 is in every submonoid.

theorem P3a.one_mem_gaps {A : Set ℕ} (h : 0 < genus A) :
1 ∈ gaps A

With a positive genus, 1 is a gap (otherwise the submonoid is all of ℕ).

theorem P3a.add_not_mem_gaps {A : Set ℕ} {a b : ℕ} (ha : a ∉ gaps A) (hb : b ∉ gaps A) :
a + b ∉ gaps A

The sum of two non-gaps is not a gap.

theorem P3a.finset_case_genus_three (T : Finset ℕ) :
T ∈ (Finset.Icc 1 5).powerset → T.card = 3 → 1 ∈ T → (2 ∉ T → 4 ∉ T) → (2 ∉ T → 3 ∉ T → 5 ∉ T) → T = {1, 2, 3} ∨ T = {1, 2, 4} ∨ T = {1, 2, 5} ∨ T = {1, 3, 5}

The finite case analysis: a 3-subset of {1,…,5} with 1, closed as the gaps of a monoid must be.

theorem P3a.gaps_of_genus_eq_three {A : Set ℕ} (hfin : (gaps A).Finite) (h : genus A = 3) :
gaps A = {1, 2, 3} ∨ gaps A = {1, 2, 4} ∨ gaps A = {1, 2, 5} ∨ gaps A = {1, 3, 5}

Lemma 4 of s-matrix-orders-II (classical, Rosales–García-Sánchez): a submonoid of ℕ with exactly three gaps has gap set {1,2,3}, {1,2,4}, {1,2,5} or {1,3,5}, i.e. it is ⟨4,5,6,7⟩, ⟨3,5,7⟩, ⟨3,4⟩ or ⟨2,7⟩.