FenchelNielsenZomorrodian/Discrete/Arithmetic/FamilyLcm.lean
1import Mathlib.Algebra.GCDMonoid.Finset
2import Mathlib.Algebra.GCDMonoid.Nat
3import Mathlib.Algebra.Order.BigOperators.Ring.Finset
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Arithmetic/FamilyLcm.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Arithmetic of period families
16GCD, LCM, prime-divisor, replicated-family, and abelian-period numerical lemmas used in compact zero-genus reductions.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
23def otherPeriodsLcmFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
24 (periods : ι → ℕ) (i : ι) : ℕ :=
25 (Finset.univ.erase i).lcm periods
27def otherPeriodsProductFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
28 (periods : ι → ℕ) (i : ι) : ℕ :=
29 (Finset.univ.erase i).prod periods
31def finZeroOfTwoLe {n : ℕ} (hn : 2 ≤ n) : Fin n :=
32 ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩
34def finOneOfTwoLe {n : ℕ} (hn : 2 ≤ n) : Fin n :=
35 ⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩
37def finPartner {n : ℕ} (hn : 2 ≤ n) (i : Fin n) : Fin n :=
38 if _ : i = finZeroOfTwoLe hn then
39 finOneOfTwoLe hn
40 else
41 finZeroOfTwoLe hn
43theorem finPartner_ne {n : ℕ} (hn : 2 ≤ n) (i : Fin n) :
44 finPartner hn i ≠ i := by
45 by_cases hi : i = finZeroOfTwoLe hn
46 · subst hi
47 intro h
48 simp only [finPartner, finZeroOfTwoLe, ↓reduceDIte, finOneOfTwoLe, Fin.mk.injEq, one_ne_zero] at h
49 · intro h
50 have hzero : finZeroOfTwoLe hn = i := by
51 simpa [finPartner, hi] using h
52 exact hi hzero.symm
54def LCMConditionFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
55 (periods : ι → ℕ) : Prop :=
56 ∀ i, periods i ∣ otherPeriodsLcmFamily periods i
58theorem LCMConditionFamily.reindex_iff
59 {α β : Type*} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
60 (e : α ≃ β) {periods : α → ℕ} :
61 LCMConditionFamily (fun b : β => periods (e.symm b)) ↔
62 LCMConditionFamily periods := by
63 let reindexed : β → ℕ := fun b => periods (e.symm b)
64 have hOther (a : α) :
65 otherPeriodsLcmFamily reindexed (e a) =
66 otherPeriodsLcmFamily periods a := by
68 have himage :
69 ((Finset.univ.erase (e a) : Finset β).image e.symm) =
70 (Finset.univ.erase a : Finset α) := by
71 ext x
72 simp only [Finset.mem_image, Finset.mem_erase, ne_eq, Finset.mem_univ, and_true, Equiv.symm_apply_eq,
73 exists_eq_right, EmbeddingLike.apply_eq_iff_eq]
74 calc
75 (Finset.univ.erase (e a) : Finset β).lcm reindexed
76 = (Finset.univ.erase (e a) : Finset β).lcm (periods ∘ e.symm) := rfl
77 _ = ((Finset.univ.erase (e a) : Finset β).image e.symm).lcm periods :=
78 (Finset.lcm_image (f := periods) (g := e.symm)
79 (s := (Finset.univ.erase (e a) : Finset β))).symm
80 _ = (Finset.univ.erase a : Finset α).lcm periods := by rw [himage]
81 constructor
82 · intro h a
83 have hdiv :
84 periods a ∣
85 otherPeriodsLcmFamily reindexed (e a) := by
86 simpa [reindexed] using h (e a)
87 simpa [reindexed, hOther a] using hdiv
88 · intro h b
89 have hdiv :
90 reindexed b ∣ otherPeriodsLcmFamily reindexed (e (e.symm b)) := by
91 have hbase := h (e.symm b)
92 rw [← hOther (e.symm b)] at hbase
93 simpa [reindexed] using hbase
94 simpa [reindexed] using hdiv
96def HasEqualPartnerFamily {ι : Type*}
97 (periods : ι → ℕ) : Prop :=
98 ∀ i, ∃ j, j ≠ i ∧ periods j = periods i
101 {ι : Type*} [Fintype ι] [DecidableEq ι] {periods : ι → ℕ}
102 (hperiods : HasEqualPartnerFamily periods) : LCMConditionFamily periods := by
103 intro i
104 rcases hperiods i with ⟨j, hji, hjEq⟩
105 have hj : j ∈ (Finset.univ.erase i : Finset ι) := by
106 exact Finset.mem_erase.mpr ⟨hji, Finset.mem_univ j⟩
107 rw [otherPeriodsLcmFamily]
108 rw [← hjEq]
109 exact Finset.dvd_lcm hj
111theorem otherPeriodsLcmFamily_pos
112 {ι : Type*} [Fintype ι] [DecidableEq ι] {periods : ι → ℕ}
113 (hpos : ∀ i, 0 < periods i) (i : ι) :
114 0 < otherPeriodsLcmFamily periods i := by
115 rw [Nat.pos_iff_ne_zero, otherPeriodsLcmFamily]
116 exact
117 (Finset.lcm_ne_zero_iff).2
118 (fun j _ => Nat.ne_of_gt (hpos j))
120abbrev NonOneSubfamilyIndex {ι : Type*} (periods : ι → ℕ) :=
121 {i : ι // periods i ≠ 1}
123def nonOneSubfamilyPeriods {ι : Type*} (periods : ι → ℕ)
124 (i : NonOneSubfamilyIndex periods) : ℕ :=
125 periods i.1
127theorem nonOneSubfamilyPeriods_ge_two
128 {ι : Type*} (periods : ι → ℕ) (hpos : ∀ i, 0 < periods i) :
129 ∀ i : NonOneSubfamilyIndex periods, 2 ≤ nonOneSubfamilyPeriods periods i := by
130 intro i
131 have hiPos : 0 < periods i.1 := hpos i.1
132 have hiNe : periods i.1 ≠ 1 := i.2
133 dsimp [nonOneSubfamilyPeriods]
134 omega
136end FenchelNielsen