|
| 1 | +/- |
| 2 | +Copyright (c) 2020 Johan Commelin. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Johan Commelin |
| 5 | +-/ |
| 6 | + |
| 7 | +import ring_theory.polynomial.chebyshev.defs |
| 8 | +import analysis.special_functions.trigonometric |
| 9 | +import ring_theory.localization |
| 10 | +import data.zmod.basic |
| 11 | +import algebra.invertible |
| 12 | + |
| 13 | +/-! |
| 14 | +# Chebyshev polynomials |
| 15 | +
|
| 16 | +The Chebyshev polynomials are two families of polynomials indexed by `ℕ`, |
| 17 | +with integral coefficients. |
| 18 | +In this file, we only consider Chebyshev polynomials of the first kind. |
| 19 | +
|
| 20 | +## Main declarations |
| 21 | +
|
| 22 | +* `polynomial.chebyshev₁_mul`, the `(m * n)`-th Chebyshev polynomial is the composition |
| 23 | + of the `m`-th and `n`-th Chebyshev polynomials. |
| 24 | +* `polynomial.lambdashev_mul`, the `(m * n)`-th lambdashev polynomial is the composition |
| 25 | + of the `m`-th and `n`-th lambdashev polynomials. |
| 26 | +* `polynomial.lambdashev_char_p`, for a prime number `p`, the `p`-th lambdashev polynomial |
| 27 | + is congruent to `X ^ p` modulo `p`. |
| 28 | +
|
| 29 | +## Implementation details |
| 30 | +
|
| 31 | +Since Chebyshev polynomials have interesting behaviour over the complex numbers and modulo `p`, |
| 32 | +we define them to have coefficients in an arbitrary commutative ring, even though |
| 33 | +technically `ℤ` would suffice. |
| 34 | +The benefit of allowing arbitrary coefficient rings, is that the statements afterwards are clean, |
| 35 | +and do not have `map (int.cast_ring_hom R)` interfering all the time. |
| 36 | +
|
| 37 | +
|
| 38 | +-/ |
| 39 | + |
| 40 | +noncomputable theory |
| 41 | + |
| 42 | +namespace polynomial |
| 43 | +open complex |
| 44 | +variables (R S : Type*) [comm_ring R] [comm_ring S] |
| 45 | + |
| 46 | +/-- The `(m * n)`-th Chebyshev polynomial is the composition of the `m`-th and `n`-th -/ |
| 47 | +lemma chebyshev₁_mul (m n : ℕ) : |
| 48 | + chebyshev₁ R (m * n) = (chebyshev₁ R m).comp (chebyshev₁ R n) := |
| 49 | +begin |
| 50 | + simp only [← map_comp, ← map_chebyshev₁ (int.cast_ring_hom R)], |
| 51 | + congr' 1, |
| 52 | + apply map_injective (int.cast_ring_hom ℂ) int.cast_injective, |
| 53 | + simp only [map_comp, map_chebyshev₁], |
| 54 | + apply polynomial.funext, |
| 55 | + intro z, |
| 56 | + obtain ⟨θ, rfl⟩ := cos_surjective z, |
| 57 | + simp only [chebyshev₁_complex_cos, nat.cast_mul, eval_comp, mul_assoc], |
| 58 | +end |
| 59 | + |
| 60 | +section lambdashev |
| 61 | +/-! |
| 62 | +
|
| 63 | +### A Lambda structure on `polynomial ℤ` |
| 64 | +
|
| 65 | +Mathlib doesn't currently know what a Lambda ring is. |
| 66 | +But once it does, we can endow `polynomial ℤ` with a Lambda structure |
| 67 | +in terms of the `lambdashev` polynomials defined below. |
| 68 | +There is exactly one other Lambda structure on `polynomial ℤ` in terms of binomial polynomials. |
| 69 | +
|
| 70 | +-/ |
| 71 | + |
| 72 | +variables {R} |
| 73 | + |
| 74 | +lemma lambdashev_eval_add_inv (x y : R) (h : x * y = 1) : |
| 75 | + ∀ n, (lambdashev R n).eval (x + y) = x ^ n + y ^ n |
| 76 | +| 0 := by simp only [bit0, eval_one, eval_add, pow_zero, lambdashev_zero] |
| 77 | +| 1 := by simp only [eval_X, lambdashev_one, pow_one] |
| 78 | +| (n + 2) := |
| 79 | +begin |
| 80 | + simp only [eval_sub, eval_mul, lambdashev_eval_add_inv, eval_X, lambdashev_add_two], |
| 81 | + conv_lhs { simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul] }, |
| 82 | + ring_exp |
| 83 | +end |
| 84 | + |
| 85 | +variables (R) |
| 86 | + |
| 87 | +lemma lambdashev_eq_chebyshev₁ [invertible (2 : R)] : |
| 88 | + ∀ n, lambdashev R n = 2 * (chebyshev₁ R n).comp (C (⅟2) * X) |
| 89 | +| 0 := by simp only [chebyshev₁_zero, mul_one, one_comp, lambdashev_zero] |
| 90 | +| 1 := by rw [lambdashev_one, chebyshev₁_one, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul, |
| 91 | + mul_inv_of_self, C_1, one_mul] |
| 92 | +| (n + 2) := |
| 93 | +begin |
| 94 | + simp only [lambdashev_add_two, chebyshev₁_add_two, lambdashev_eq_chebyshev₁ (n + 1), |
| 95 | + lambdashev_eq_chebyshev₁ n, sub_comp, mul_comp, add_comp, X_comp, bit0_comp, one_comp], |
| 96 | + simp only [← C_1, ← C_bit0, ← mul_assoc, ← C_mul, mul_inv_of_self], |
| 97 | + rw [C_1, one_mul], |
| 98 | + ring |
| 99 | +end |
| 100 | + |
| 101 | +lemma chebyshev₁_eq_lambdashev [invertible (2 : R)] (n : ℕ) : |
| 102 | + chebyshev₁ R n = C (⅟2) * (lambdashev R n).comp (2 * X) := |
| 103 | +begin |
| 104 | + rw lambdashev_eq_chebyshev₁, |
| 105 | + simp only [comp_assoc, mul_comp, C_comp, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul], |
| 106 | + rw [inv_of_mul_self, C_1, one_mul, one_mul, comp_X] |
| 107 | +end |
| 108 | + |
| 109 | +/-- the `(m * n)`-th lambdashev polynomial is the composition of the `m`-th and `n`-th -/ |
| 110 | +lemma lambdashev_mul (m n : ℕ) : |
| 111 | + lambdashev R (m * n) = (lambdashev R m).comp (lambdashev R n) := |
| 112 | +begin |
| 113 | + simp only [← map_lambdashev (int.cast_ring_hom R), ← map_comp], |
| 114 | + congr' 1, |
| 115 | + apply map_injective (int.cast_ring_hom ℚ) int.cast_injective, |
| 116 | + simp only [map_lambdashev, map_comp, lambdashev_eq_chebyshev₁, chebyshev₁_mul, two_mul, |
| 117 | + ← add_comp], |
| 118 | + simp only [← two_mul, ← comp_assoc], |
| 119 | + apply eval₂_congr rfl rfl, |
| 120 | + rw [comp_assoc], |
| 121 | + apply eval₂_congr rfl _ rfl, |
| 122 | + rw [mul_comp, C_comp, X_comp, ← mul_assoc, ← C_1, ← C_bit0, ← C_mul, |
| 123 | + inv_of_mul_self, C_1, one_mul] |
| 124 | +end |
| 125 | + |
| 126 | +lemma lambdashev_comp_comm (m n : ℕ) : |
| 127 | + (lambdashev R m).comp (lambdashev R n) = (lambdashev R n).comp (lambdashev R m) := |
| 128 | +by rw [← lambdashev_mul, mul_comm, lambdashev_mul] |
| 129 | + |
| 130 | +lemma lambdashev_zmod_p (p : ℕ) [fact p.prime] : |
| 131 | + lambdashev (zmod p) p = X ^ p := |
| 132 | +begin |
| 133 | + -- Recall that `lambdashev_eval_add_inv` characterises `lambdashev R p` |
| 134 | + -- as a polynomial that maps `x + x⁻¹` to `x ^ p + (x⁻¹) ^ p`. |
| 135 | + -- Since `X ^ p` also satisfies this property in characteristic `p`, |
| 136 | + -- we can use a variant on `polynomial.funext` to conclude that these polynomials are equal. |
| 137 | + -- For this argument, we need an arbitrary infinite field of characteristic `p`. |
| 138 | + obtain ⟨K, _, _, H⟩ : ∃ (K : Type) [field K], by exactI ∃ [char_p K p], infinite K, |
| 139 | + { let K := fraction_ring (polynomial (zmod p)), |
| 140 | + let f : zmod p →+* K := (fraction_ring.of _).to_map.comp C, |
| 141 | + haveI : char_p K p := by { rw ← f.char_p_iff_char_p, apply_instance }, |
| 142 | + haveI : infinite K := |
| 143 | + by { apply infinite.of_injective _ (fraction_ring.of _).injective, apply_instance }, |
| 144 | + refine ⟨K, _, _, _⟩; apply_instance }, |
| 145 | + resetI, |
| 146 | + apply map_injective (zmod.cast_hom (dvd_refl p) K) (ring_hom.injective _), |
| 147 | + rw [map_lambdashev, map_pow, map_X], |
| 148 | + apply eq_of_infinite_eval_eq, |
| 149 | + -- The two polynomials agree on all `x` of the form `x = y + y⁻¹`. |
| 150 | + apply @set.infinite_mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, |
| 151 | + { rintro _ ⟨x, rfl, hx⟩, |
| 152 | + simp only [eval_X, eval_pow, set.mem_set_of_eq, @add_pow_char K _ p, |
| 153 | + lambdashev_eval_add_inv _ _ (mul_inv_cancel hx)] }, |
| 154 | + -- Now we need to show that the set of such `x` is infinite. |
| 155 | + -- If the set is finite, then we will show that `K` is also finite. |
| 156 | + { intro h, |
| 157 | + rw ← set.infinite_univ_iff at H, |
| 158 | + apply H, |
| 159 | + -- To each `x` of the form `x = y + y⁻¹` |
| 160 | + -- we `bind` the set of `y` that solve the equation `x = y + y⁻¹`. |
| 161 | + -- For every `x`, that set is finite (since it is governed by a quadratic equation). |
| 162 | + -- For the moment, we claim that all these sets together cover `K`. |
| 163 | + suffices : (set.univ : set K) = |
| 164 | + {x : K | ∃ (y : K), x = y + y⁻¹ ∧ y ≠ 0} >>= (λ x, {y | x = y + y⁻¹ ∨ y = 0}), |
| 165 | + { rw this, clear this, |
| 166 | + apply set.finite_bind h, |
| 167 | + rintro x hx, |
| 168 | + -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`. |
| 169 | + let φ : polynomial K := X ^ 2 - C x * X + 1, |
| 170 | + have hφ : φ ≠ 0, |
| 171 | + { intro H, |
| 172 | + have : φ.eval 0 = 0, by rw [H, eval_zero], |
| 173 | + simpa [eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, |
| 174 | + eval_mul, mul_zero, pow_two, zero_add, one_ne_zero] }, |
| 175 | + classical, |
| 176 | + convert (φ.roots ∪ {0}).to_finset.finite_to_set using 1, |
| 177 | + ext1 y, |
| 178 | + simp only [multiset.mem_to_finset, set.mem_set_of_eq, finset.mem_coe, multiset.mem_union, |
| 179 | + mem_roots hφ, is_root, eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one, |
| 180 | + multiset.mem_singleton, multiset.singleton_eq_singleton], |
| 181 | + by_cases hy : y = 0, |
| 182 | + { simp only [hy, eq_self_iff_true, or_true] }, |
| 183 | + apply or_congr _ iff.rfl, |
| 184 | + rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel hy], |
| 185 | + apply eq_iff_eq_cancel_right.mpr, |
| 186 | + ring }, |
| 187 | + -- Finally, we prove the claim that our finite union of finite sets covers all of `K`. |
| 188 | + { apply (set.eq_univ_of_forall _).symm, |
| 189 | + intro x, |
| 190 | + simp only [exists_prop, set.mem_Union, set.bind_def, ne.def, set.mem_set_of_eq], |
| 191 | + by_cases hx : x = 0, |
| 192 | + { simp only [hx, and_true, eq_self_iff_true, inv_zero, or_true], |
| 193 | + exact ⟨_, 1, rfl, one_ne_zero⟩ }, |
| 194 | + { simp only [hx, or_false, exists_eq_right], |
| 195 | + exact ⟨_, rfl, hx⟩ } } } |
| 196 | +end |
| 197 | + |
| 198 | +lemma lambdashev_char_p (p : ℕ) [fact p.prime] [char_p R p] : |
| 199 | + lambdashev R p = X ^ p := |
| 200 | +by rw [← map_lambdashev (zmod.cast_hom (dvd_refl p) R), lambdashev_zmod_p, map_pow, map_X] |
| 201 | + |
| 202 | +end lambdashev |
| 203 | + |
| 204 | +end polynomial |
0 commit comments