Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Data.Polynomial.Expand (#4083)
Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
- Loading branch information
1 parent
87c4a75
commit db15210
Showing
2 changed files
with
300 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,299 @@ | ||
/- | ||
Copyright (c) 2020 Kenny Lau. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Kenny Lau | ||
! This file was ported from Lean 3 source module data.polynomial.expand | ||
! leanprover-community/mathlib commit bbeb185db4ccee8ed07dc48449414ebfa39cb821 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.RingTheory.Polynomial.Basic | ||
import Mathlib.RingTheory.Ideal.LocalRing | ||
|
||
/-! | ||
# Expand a polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`. | ||
## Main definitions | ||
* `Polynomial.expand R p f`: expand the polynomial `f` with coefficients in a | ||
commutative semiring `R` by a factor of p, so `expand R p (∑ aₙ xⁿ)` is `∑ aₙ xⁿᵖ`. | ||
* `Polynomial.contract p f`: the opposite of `expand`, so it sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. | ||
-/ | ||
|
||
|
||
universe u v w | ||
|
||
open Classical BigOperators Polynomial | ||
|
||
open Finset | ||
|
||
namespace Polynomial | ||
|
||
section CommSemiring | ||
|
||
variable (R : Type u) [CommSemiring R] {S : Type v} [CommSemiring S] (p q : ℕ) | ||
|
||
/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`. -/ | ||
noncomputable def expand : R[X] →ₐ[R] R[X] := | ||
{ (eval₂RingHom C (X ^ p) : R[X] →+* R[X]) with commutes' := fun _ => eval₂_C _ _ } | ||
#align polynomial.expand Polynomial.expand | ||
|
||
theorem coe_expand : (expand R p : R[X] → R[X]) = eval₂ C (X ^ p) := | ||
rfl | ||
#align polynomial.coe_expand Polynomial.coe_expand | ||
|
||
variable {R} | ||
|
||
theorem expand_eq_sum {f : R[X]} : expand R p f = f.sum fun e a => C a * (X ^ p) ^ e := by | ||
simp [expand, eval₂] | ||
#align polynomial.expand_eq_sum Polynomial.expand_eq_sum | ||
|
||
@[simp] | ||
theorem expand_C (r : R) : expand R p (C r) = C r := | ||
eval₂_C _ _ | ||
set_option linter.uppercaseLean3 false in | ||
#align polynomial.expand_C Polynomial.expand_C | ||
|
||
@[simp] | ||
theorem expand_X : expand R p X = X ^ p := | ||
eval₂_X _ _ | ||
set_option linter.uppercaseLean3 false in | ||
#align polynomial.expand_X Polynomial.expand_X | ||
|
||
@[simp] | ||
theorem expand_monomial (r : R) : expand R p (monomial q r) = monomial (q * p) r := by | ||
simp_rw [← smul_X_eq_monomial, AlgHom.map_smul, AlgHom.map_pow, expand_X, mul_comm, pow_mul] | ||
#align polynomial.expand_monomial Polynomial.expand_monomial | ||
|
||
theorem expand_expand (f : R[X]) : expand R p (expand R q f) = expand R (p * q) f := | ||
Polynomial.induction_on f (fun r => by simp_rw [expand_C]) | ||
(fun f g ihf ihg => by simp_rw [AlgHom.map_add, ihf, ihg]) fun n r _ => by | ||
simp_rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, AlgHom.map_pow, expand_X, pow_mul] | ||
#align polynomial.expand_expand Polynomial.expand_expand | ||
|
||
theorem expand_mul (f : R[X]) : expand R (p * q) f = expand R p (expand R q f) := | ||
(expand_expand p q f).symm | ||
#align polynomial.expand_mul Polynomial.expand_mul | ||
|
||
@[simp] | ||
theorem expand_zero (f : R[X]) : expand R 0 f = C (eval 1 f) := by simp [expand] | ||
#align polynomial.expand_zero Polynomial.expand_zero | ||
|
||
@[simp] | ||
theorem expand_one (f : R[X]) : expand R 1 f = f := | ||
Polynomial.induction_on f (fun r => by rw [expand_C]) | ||
(fun f g ihf ihg => by rw [AlgHom.map_add, ihf, ihg]) fun n r _ => by | ||
rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, pow_one] | ||
#align polynomial.expand_one Polynomial.expand_one | ||
|
||
theorem expand_pow (f : R[X]) : expand R (p ^ q) f = (expand R p^[q]) f := | ||
Nat.recOn q (by rw [pow_zero, expand_one, Function.iterate_zero, id]) fun n ih => by | ||
rw [Function.iterate_succ_apply', pow_succ, expand_mul, ih] | ||
#align polynomial.expand_pow Polynomial.expand_pow | ||
|
||
theorem derivative_expand (f : R[X]) : Polynomial.derivative (expand R p f) = | ||
expand R p (Polynomial.derivative f) * (p * (X ^ (p - 1) : R[X])) := by | ||
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_nat_cast, derivative_X, mul_one] | ||
#align polynomial.derivative_expand Polynomial.derivative_expand | ||
|
||
theorem coeff_expand {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : | ||
(expand R p f).coeff n = if p ∣ n then f.coeff (n / p) else 0 := by | ||
simp only [expand_eq_sum] | ||
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum] | ||
split_ifs with h | ||
· rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl] | ||
· intro b _ hb2 | ||
rw [if_neg] | ||
intro hb3 | ||
apply hb2 | ||
rw [← hb3, Nat.mul_div_cancel_left b hp] | ||
· intro hn | ||
rw [not_mem_support_iff.1 hn] | ||
split_ifs <;> rfl | ||
· rw [Finset.sum_eq_zero] | ||
intro k _ | ||
rw [if_neg] | ||
exact fun hkn => h ⟨k, hkn.symm⟩ | ||
#align polynomial.coeff_expand Polynomial.coeff_expand | ||
|
||
@[simp] | ||
theorem coeff_expand_mul {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : | ||
(expand R p f).coeff (n * p) = f.coeff n := by | ||
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp] | ||
#align polynomial.coeff_expand_mul Polynomial.coeff_expand_mul | ||
|
||
@[simp] | ||
theorem coeff_expand_mul' {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : | ||
(expand R p f).coeff (p * n) = f.coeff n := by rw [mul_comm, coeff_expand_mul hp] | ||
#align polynomial.coeff_expand_mul' Polynomial.coeff_expand_mul' | ||
|
||
/-- Expansion is injective. -/ | ||
theorem expand_injective {n : ℕ} (hn : 0 < n) : Function.Injective (expand R n) := fun g g' H => | ||
ext fun k => by rw [← coeff_expand_mul hn, H, coeff_expand_mul hn] | ||
#align polynomial.expand_injective Polynomial.expand_injective | ||
|
||
theorem expand_inj {p : ℕ} (hp : 0 < p) {f g : R[X]} : expand R p f = expand R p g ↔ f = g := | ||
(expand_injective hp).eq_iff | ||
#align polynomial.expand_inj Polynomial.expand_inj | ||
|
||
theorem expand_eq_zero {p : ℕ} (hp : 0 < p) {f : R[X]} : expand R p f = 0 ↔ f = 0 := | ||
(expand_injective hp).eq_iff' (map_zero _) | ||
#align polynomial.expand_eq_zero Polynomial.expand_eq_zero | ||
|
||
theorem expand_ne_zero {p : ℕ} (hp : 0 < p) {f : R[X]} : expand R p f ≠ 0 ↔ f ≠ 0 := | ||
(expand_eq_zero hp).not | ||
#align polynomial.expand_ne_zero Polynomial.expand_ne_zero | ||
|
||
theorem expand_eq_C {p : ℕ} (hp : 0 < p) {f : R[X]} {r : R} : expand R p f = C r ↔ f = C r := by | ||
rw [← expand_C, expand_inj hp, expand_C] | ||
set_option linter.uppercaseLean3 false in | ||
#align polynomial.expand_eq_C Polynomial.expand_eq_C | ||
|
||
theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.natDegree * p := by | ||
cases' p.eq_zero_or_pos with hp hp | ||
· rw [hp, coe_expand, pow_zero, MulZeroClass.mul_zero, ← C_1, eval₂_hom, natDegree_C] | ||
by_cases hf : f = 0 | ||
· rw [hf, AlgHom.map_zero, natDegree_zero, MulZeroClass.zero_mul] | ||
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf | ||
rw [← WithBot.coe_eq_coe] | ||
convert (degree_eq_natDegree hf1).symm -- Porting note: was `rw [degree_eq_natDegree hf1]` | ||
symm | ||
refine' le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => _) _ | ||
· rw [coeff_expand hp] | ||
split_ifs with hpn | ||
· rw [coeff_eq_zero_of_natDegree_lt] | ||
contrapose! hn | ||
erw [WithBot.coe_le_coe, ← Nat.div_mul_cancel hpn] | ||
exact Nat.mul_le_mul_right p hn | ||
· rfl | ||
· refine' le_degree_of_ne_zero _ | ||
erw [coeff_expand_mul hp, ← leadingCoeff] | ||
exact mt leadingCoeff_eq_zero.1 hf | ||
#align polynomial.nat_degree_expand Polynomial.natDegree_expand | ||
|
||
theorem Monic.expand {p : ℕ} {f : R[X]} (hp : 0 < p) (h : f.Monic) : (expand R p f).Monic := by | ||
rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp] | ||
simp [hp, h] | ||
#align polynomial.monic.expand Polynomial.Monic.expand | ||
|
||
theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} : | ||
map f (expand R p q) = expand S p (map f q) := by | ||
by_cases hp : p = 0 | ||
· simp [hp] | ||
ext | ||
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)] | ||
split_ifs <;> simp_all | ||
#align polynomial.map_expand Polynomial.map_expand | ||
|
||
@[simp] | ||
theorem expand_eval (p : ℕ) (P : R[X]) (r : R) : eval r (expand R p P) = eval (r ^ p) P := by | ||
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp | ||
rw [AlgHom.map_add, eval_add, eval_add, hf, hg] | ||
#align polynomial.expand_eval Polynomial.expand_eval | ||
|
||
@[simp] | ||
theorem expand_aeval {A : Type _} [Semiring A] [Algebra R A] (p : ℕ) (P : R[X]) (r : A) : | ||
aeval r (expand R p P) = aeval (r ^ p) P := by | ||
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp | ||
rw [AlgHom.map_add, aeval_add, aeval_add, hf, hg] | ||
#align polynomial.expand_aeval Polynomial.expand_aeval | ||
|
||
/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/ | ||
noncomputable def contract (p : ℕ) (f : R[X]) : R[X] := | ||
∑ n in range (f.natDegree + 1), monomial n (f.coeff (n * p)) | ||
#align polynomial.contract Polynomial.contract | ||
|
||
theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) : | ||
(contract p f).coeff n = f.coeff (n * p) := by | ||
simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt, | ||
ite_eq_left_iff] | ||
intro hn | ||
apply (coeff_eq_zero_of_natDegree_lt _).symm | ||
calc | ||
f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _ | ||
_ ≤ n * 1 := by simpa only [mul_one] using hn | ||
_ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n) | ||
#align polynomial.coeff_contract Polynomial.coeff_contract | ||
|
||
theorem contract_expand {f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f := by | ||
ext | ||
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt] | ||
#align polynomial.contract_expand Polynomial.contract_expand | ||
|
||
section CharP | ||
|
||
variable [CharP R p] | ||
|
||
theorem expand_contract [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) | ||
(hp : p ≠ 0) : expand R p (contract p f) = f := by | ||
ext n | ||
rw [coeff_expand hp.bot_lt, coeff_contract hp] | ||
split_ifs with h | ||
· rw [Nat.div_mul_cancel h] | ||
· cases' n with n | ||
· exact absurd (dvd_zero p) h | ||
have := coeff_derivative f n | ||
rw [hf, coeff_zero, zero_eq_mul] at this | ||
cases' this with h' | ||
· rw [h'] | ||
rename_i _ _ _ _ h' | ||
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h' | ||
exact absurd h' h | ||
#align polynomial.expand_contract Polynomial.expand_contract | ||
|
||
variable [hp : Fact p.Prime] | ||
|
||
theorem expand_char (f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p := by | ||
refine' f.induction_on' (fun a b ha hb => _) fun n a => _ | ||
· rw [AlgHom.map_add, Polynomial.map_add, ha, hb, add_pow_char] | ||
· rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial, | ||
mul_pow, ← C.map_pow, frobenius_def] | ||
ring | ||
#align polynomial.expand_char Polynomial.expand_char | ||
|
||
theorem map_expand_pow_char (f : R[X]) (n : ℕ) : | ||
map (frobenius R p ^ n) (expand R (p ^ n) f) = f ^ p ^ n := by | ||
induction' n with _ n_ih | ||
· simp [RingHom.one_def] | ||
symm | ||
rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, RingHom.mul_def, ← map_map, mul_comm, | ||
expand_mul, ← map_expand] | ||
#align polynomial.map_expand_pow_char Polynomial.map_expand_pow_char | ||
|
||
end CharP | ||
|
||
end CommSemiring | ||
|
||
section IsDomain | ||
|
||
variable (R : Type u) [CommRing R] [IsDomain R] | ||
|
||
theorem isLocalRingHom_expand {p : ℕ} (hp : 0 < p) : | ||
IsLocalRingHom (↑(expand R p) : R[X] →+* R[X]) := by | ||
refine' ⟨fun f hf1 => _⟩; norm_cast at hf1 | ||
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1) | ||
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2 | ||
rw [hf2, isUnit_C] at hf1; rw [expand_eq_C hp] at hf2; rwa [hf2, isUnit_C] | ||
#align polynomial.is_local_ring_hom_expand Polynomial.isLocalRingHom_expand | ||
|
||
variable {R} | ||
|
||
theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : R[X]} (hf : Irreducible (expand R p f)) : | ||
Irreducible f := | ||
let _ := isLocalRingHom_expand R hp.bot_lt | ||
of_irreducible_map (↑(expand R p)) hf | ||
#align polynomial.of_irreducible_expand Polynomial.of_irreducible_expand | ||
|
||
theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} : | ||
Irreducible (expand R (p ^ n) f) → Irreducible f := | ||
Nat.recOn n (fun hf => by rwa [pow_zero, expand_one] at hf) fun n ih hf => | ||
ih <| of_irreducible_expand hp <| by | ||
rw [pow_succ] at hf | ||
rwa [expand_expand] | ||
#align polynomial.of_irreducible_expand_pow Polynomial.of_irreducible_expand_pow | ||
|
||
end IsDomain | ||
|
||
end Polynomial |