RationalFG.lean

1 import Mathlib.GroupTheory.Finiteness
2 import Mathlib.Algebra.Group.Subgroup.Order
3 import Mathlib.GroupTheory.SpecificGroups.Cyclic
4 import Mathlib.Data.Rat.Lemmas
5 import Mathlib.Tactic.Ring
6 
7 /-! # Finitely generated rational subgroups are cyclic -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped BigOperators
11 namespace RealizationBoundaries
12 
13 /-- A finite family of rationals lies in one actual cyclic rational lattice,
14 using the product of its denominators as a common denominator. -/
15 theorem finite_rationals_common_cyclic_lattice (s : Finset ℚ) :
16     ∃ d : ℕ, 0 < d ∧ (↑s : Set ℚ) ⊆ AddSubgroup.zmultiples (1 / (d : ℚ)) := by
17   classical
18   let d : ℕ := ∏ q ∈ s, q.den
19   have hdpos : 0 < d := Finset.prod_pos (fun q _ => q.den_pos)
20   have hd : (d : ℚ) ≠ 0 := by exact_mod_cast hdpos.ne'
21   refine ⟨d, hdpos, ?_⟩
22   intro q hq
23   have hden : q.den ∣ d := Finset.dvd_prod_of_mem (fun q : ℚ => q.den) hq
24   obtain ⟨k, hk⟩ := hden
25   apply AddSubgroup.mem_zmultiples_iff.mpr
26   refine ⟨q.num * (k : ℤ), ?_⟩
27   rw [zsmul_eq_mul]
28   push_cast
29   rw [mul_one_div]
30   apply (div_eq_iff hd).mpr
31   rw [hk, Nat.cast_mul, ← Rat.den_mul_eq_num q]
32   ring
33 
34 /-- Every finitely generated additive subgroup of the actual rational numbers
35 is contained in a cyclic rational lattice, hence is itself cyclic. -/
36 theorem rational_subgroup_fg_isAddCyclic (H : AddSubgroup ℚ) (hH : H.FG) :
37     IsAddCyclic H := by
38   obtain ⟨s, hs⟩ := hH
39   obtain ⟨d, _, hd⟩ := finite_rationals_common_cyclic_lattice s
40   have hle : H ≤ AddSubgroup.zmultiples (1 / (d : ℚ)) := by
41     rw [← hs]
42     exact (AddSubgroup.closure_le _).mpr hd
43   exact AddSubgroup.isAddCyclic_of_le hle
44 
45 /-- Typeclass formulation for the rational image of a finitely generated group. -/
46 theorem rational_fg_isAddCyclic (H : AddSubgroup ℚ) [AddGroup.FG H] : IsAddCyclic H :=
47   rational_subgroup_fg_isAddCyclic H ((AddGroup.fg_iff_addSubgroup_fg H).mp inferInstance)
48 
49 /-- A nonzero finitely generated rational subgroup is additively isomorphic
50 to the integers. No generator of the surrounding rational vector space is assumed. -/
51 theorem rational_fg_equiv_int (H : AddSubgroup ℚ) [AddGroup.FG H] (hH : H ≠ ⊥) :
52     Nonempty (H ≃+ ℤ) := by
53   have : IsAddCyclic H := rational_fg_isAddCyclic H
54   have : Nontrivial H := H.nontrivial_iff_ne_bot.mpr hH
55   obtain ⟨e⟩ := (LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int).mp
56     (inferInstance : IsAddCyclic H)
57   exact ⟨e.toAddEquiv⟩
58 
59 /-- A generator and the exact integer-multiple enumeration are available even
60 in the zero subgroup case. -/
61 theorem rational_fg_generator (H : AddSubgroup ℚ) [AddGroup.FG H] :
62     ∃ q : H, Function.Surjective (fun n : ℤ => n • q) :=
63   (rational_fg_isAddCyclic H).exists_zsmul_surjective
64 
65 end RealizationBoundaries

Back to source controls