Descent Theorem

We provide a proof of the following result.

Let G be a group and f : G →* G an endomorphism of G that maps every subgroup of G into itself (e.g., f = fun g ↦ g ^ n when G is commutative).

If there is a finite subset s : Set G and there exists a "height" function h : G → ℝ and constants a, b, c : ℝ such that

• s surjects onto the quotient G ⧸ f(G),
• for all g ∈ s and x : G, h x ≤ a * h (g * x) + c,
• for all x : G, h (f x) ≥ b * h x - c,
• for all B : ℝ, there are only finitely many x : G such that h x ≤ B, and
• 0 ≤ a < b, then G is finitely generated. See Group.fg_of_descent / AddGroup.fg_of_descent.

We use this to deduce a more specific version when G is commutative and f is the nth power endomorphism and finally an even more specific version with n = 2, replacing the upper and lower bound for the height function by the "approximate parallelogram law" ∀ x y, |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C. See CommGroup.fg_of_descent / AddCommGroup.fg_of_descent and CommGroup.fg_of_descent' / AddCommGroup.fg_of_descent'.

This last version is one of the main ingredients of the standard proof of the Mordell-Weil Theorem. It allows to reduce the statement to showing that G / 2 • G is finite (where G is the Mordell-Weil group`).

Implementation note

Replacing ℝ by an ordered field ({R : Type*} [LinearOrder R] [Field R] [IsOrderedRing R]) works, but makes the type check quite slow (and to_additive needs some help...). As the application(s) work with ℝ-valued height functions, we think that generalizing is not really worth the trouble.

theorem Group.fg_of_descent {G : Type u_1} [Group G] {f : G →* G} (hf : ∀ (U : Subgroup G), Subgroup.map f U ≤ U) {s : Set G} {h : G → ℝ} {a b c : ℝ} (ha : 0 ≤ a) (H₀ : a < b) (hs : s.Finite) (H₁ : s * ↑f.range = Set.univ) (H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c) (H₃ : ∀ (x : G), b * h x - c ≤ h (f x)) [Northcott h] : FG G

If G is a group and f : G →* G is an endomorphism sending subgroups into themselves, and if there is a "height function" h : G → ℝ with respect to f and a finite subset s of G, then G is finitely generated.

theorem AddGroup.fg_of_descent {G : Type u_1} [AddGroup G] {f : G →+ G} (hf : ∀ (U : AddSubgroup G), AddSubgroup.map f U ≤ U) {s : Set G} {h : G → ℝ} {a b c : ℝ} (ha : 0 ≤ a) (H₀ : a < b) (hs : s.Finite) (H₁ : s + ↑f.range = Set.univ) (H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g + x) + c) (H₃ : ∀ (x : G), b * h x - c ≤ h (f x)) [Northcott h] : FG G

If G is an additive group and f : G →+ G is an endomorphism sending subgroups into themselves, and if there is a "height function" h : G → ℝ with respect to f and a finite subset s of G, then G is finitely generated.

theorem CommGroup.fg_of_descent {G : Type u_1} [CommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ} {c : G → ℝ} (ha : 0 ≤ a) (H₀ : a < b) (H₁ : (powMonoidHom n).range.FiniteIndex) (H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g) (H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)) [Northcott h] : Group.FG G

If G is a commutative group and n : ℕ, h : G → ℝ satisfy

• G / G ^ n is finite,
• for all g x : G, h x ≤ a * h (g * x) + c g,
• for all x : G, h (x ^ n) ≥ b * h x - c₀,
• for all B : ℝ, there are only finitely many x : G such that h x ≤ B, where 0 ≤ a < b and c₀ are real numbers, c : G → ℝ, then G is finitely generated.

theorem AddCommGroup.fg_of_descent {G : Type u_1} [AddCommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ} {c : G → ℝ} (ha : 0 ≤ a) (H₀ : a < b) (H₁ : (nsmulAddMonoidHom n).range.FiniteIndex) (H₂ : ∀ (g x : G), h x ≤ a * h (g + x) + c g) (H₃ : ∀ (x : G), b * h x - c₀ ≤ h (n • x)) [Northcott h] : AddGroup.FG G

If G is a commutative additive group and n : ℕ, h : G → ℝ satisfy

• G / n • G is finite,
• for all g x : G, h x ≤ a * h (g + x) + c g,
• for all x : G, h (n • x) ≥ b * h x - c₀,
• for all B : ℝ, there are only finitely many x : G such that h x ≤ B, where 0 ≤ a < b and c₀ are real numbers, c : G → ℝ, then G is finitely generated.

theorem CommGroup.fg_of_descent' {G : Type u_1} [CommGroup G] {h : G → ℝ} {C : ℝ} (H₁ : (powMonoidHom 2).range.FiniteIndex) (H₂ : ∀ (x : G), 0 ≤ h x) (H₃ : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C) [Northcott h] : Group.FG G

If G is a commutative group and n : ℕ, h : G → ℝ satisfy

• G / G ^ 2 is finite,
• 0 ≤ h x for all x : G,
• there is C : ℝ such that for all x y : G, |h (x * y) + h(x / y) - 2 * (h x + h y)| ≤ C,
• for all B : ℝ, there are only finitely many x : G such that h x ≤ B, then G is finitely generated.

theorem AddCommGroup.fg_of_descent' {G : Type u_1} [AddCommGroup G] {h : G → ℝ} {C : ℝ} (H₁ : (nsmulAddMonoidHom 2).range.FiniteIndex) (H₂ : ∀ (x : G), 0 ≤ h x) (H₃ : ∀ (x y : G), |h (x + y) + h (x - y) - 2 * (h x + h y)| ≤ C) [Northcott h] : AddGroup.FG G

If G is a commutative additive group and n : ℕ, h : G → ℝ satisfy

• G / 2 • G is finite,
• 0 ≤ h x for all x : G,
• there is C : ℝ such that for all x y : G, |h (x + y) + h(x - y) - 2 * (h x + h y)| ≤ C,
• for all B : ℝ, there are only finitely many x : G such that h x ≤ B, then G is finitely generated.