FenchelNielsenZomorrodian.Discrete.Arithmetic.FamilyLcm
This module studies family lcm for fenchel nielsen zomorrodian. The least common multiple of the periods other than the distinguished one. The product of the periods other than the distinguished one.
import
- Mathlib.Algebra.GCDMonoid.Finset
- Mathlib.Algebra.GCDMonoid.Nat
- Mathlib.Algebra.Order.BigOperators.Ring.Finset
def otherPeriodsLcmFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
(periods : ι → ℕ) (i : ι) : ℕ :=
(Finset.univ.erase i).lcm periodsThe least common multiple of the periods other than the distinguished one.
def otherPeriodsProductFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
(periods : ι → ℕ) (i : ι) : ℕ :=
(Finset.univ.erase i).prod periodsThe product of the periods other than the distinguished one.
def finZeroOfTwoLe {n : ℕ} (hn : 2 ≤ n) : Fin n :=
⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩This arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
def finOneOfTwoLe {n : ℕ} (hn : 2 ≤ n) : Fin n :=
⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩This arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
def finPartner {n : ℕ} (hn : 2 ≤ n) (i : Fin n) : Fin n :=
if _ : i = finZeroOfTwoLe hn then
finOneOfTwoLe hn
else
finZeroOfTwoLe hnThis arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
theorem finPartner_ne {n : ℕ} (hn : 2 ≤ n) (i : Fin n) :
finPartner hn i ≠ iThis arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
Show proof
by
by_cases hi : i = finZeroOfTwoLe hn
· subst hi
intro h
simp only [finPartner, finZeroOfTwoLe, ↓reduceDIte, finOneOfTwoLe, Fin.mk.injEq, one_ne_zero] at h
· intro h
have hzero : finZeroOfTwoLe hn = i := by
simpa [finPartner, hi] using h
exact hi hzero.symmProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□def LCMConditionFamily {ι : Type*} [Fintype ι] [DecidableEq ι]
(periods : ι → ℕ) : Prop :=
∀ i, periods i ∣ otherPeriodsLcmFamily periods iThis arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
theorem LCMConditionFamily.reindex_iff
{α β : Type*} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
(e : α ≃ β) {periods : α → ℕ} :
LCMConditionFamily (fun b : β => periods (e.symm b)) ↔
LCMConditionFamily periodsThe reindexed period condition is equivalent to the original period condition after transporting indices.
Show proof
by
let reindexed : β → ℕ := fun b => periods (e.symm b)
have hOther (a : α) :
otherPeriodsLcmFamily reindexed (e a) =
otherPeriodsLcmFamily periods a := by
rw [otherPeriodsLcmFamily, otherPeriodsLcmFamily]
have himage :
((Finset.univ.erase (e a) : Finset β).image e.symm) =
(Finset.univ.erase a : Finset α) := by
ext x
simp only [Finset.mem_image, Finset.mem_erase, ne_eq, Finset.mem_univ, and_true, Equiv.symm_apply_eq,
exists_eq_right, EmbeddingLike.apply_eq_iff_eq]
calc
(Finset.univ.erase (e a) : Finset β).lcm reindexed
= (Finset.univ.erase (e a) : Finset β).lcm (periods ∘ e.symm) := rfl
_ = ((Finset.univ.erase (e a) : Finset β).image e.symm).lcm periods :=
(Finset.lcm_image (f := periods) (g := e.symm)
(s := (Finset.univ.erase (e a) : Finset β))).symm
_ = (Finset.univ.erase a : Finset α).lcm periods := by rw [himage]
constructor
· intro h a
have hdiv :
periods a ∣
otherPeriodsLcmFamily reindexed (e a) := by
simpa [reindexed] using h (e a)
simpa [reindexed, hOther a] using hdiv
· intro h b
have hdiv :
reindexed b ∣ otherPeriodsLcmFamily reindexed (e (e.symm b)) := by
have hbase := h (e.symm b)
rw [← hOther (e.symm b)] at hbase
simpa [reindexed] using hbase
simpa [reindexed] using hdivProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def HasEqualPartnerFamily {ι : Type*}
(periods : ι → ℕ) : Prop :=
∀ i, ∃ j, j ≠ i ∧ periods j = periods iThis arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
theorem lcmConditionFamily_of_hasEqualPartnerFamily
{ι : Type*} [Fintype ι] [DecidableEq ι] {periods : ι → ℕ}
(hperiods : HasEqualPartnerFamily periods) : LCMConditionFamily periodsThis arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
Show proof
by
intro i
rcases hperiods i with ⟨j, hji, hjEq⟩
have hj : j ∈ (Finset.univ.erase i : Finset ι) := by
exact Finset.mem_erase.mpr ⟨hji, Finset.mem_univ j⟩
rw [otherPeriodsLcmFamily]
rw [← hjEq]
exact Finset.dvd_lcm hjProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem otherPeriodsLcmFamily_pos
{ι : Type*} [Fintype ι] [DecidableEq ι] {periods : ι → ℕ}
(hpos : ∀ i, 0 < periods i) (i : ι) :
0 < otherPeriodsLcmFamily periods iThe lcm of the other period family is positive.
Show proof
by
rw [Nat.pos_iff_ne_zero, otherPeriodsLcmFamily]
exact
(Finset.lcm_ne_zero_iff).2
(fun j _ => Nat.ne_of_gt (hpos j))Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□abbrev NonOneSubfamilyIndex {ι : Type*} (periods : ι → ℕ) :=
{i : ι // periods i ≠ 1}This arithmetic lemma packages the LCM or equal-partner condition for the family of elliptic periods.
def nonOneSubfamilyPeriods {ι : Type*} (periods : ι → ℕ)
(i : NonOneSubfamilyIndex periods) : ℕ :=
periods i.1theorem nonOneSubfamilyPeriods_ge_two
{ι : Type*} (periods : ι → ℕ) (hpos : ∀ i, 0 < periods i) :
∀ i : NonOneSubfamilyIndex periods, 2 ≤ nonOneSubfamilyPeriods periods iEvery nontrivial period in the selected subfamily is at least \(2\).
Show proof
by
intro i
have hiPos : 0 < periods i.1 := hpos i.1
have hiNe : periods i.1 ≠ 1 := i.2
dsimp [nonOneSubfamilyPeriods]
omegaProof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□