[Merged by Bors] - feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors #4838
Conversation
jcommelin
added
the
awaiting-review
There was a problem hiding this comment.
I'm pretty sure Johan knows more about tricks with Witt polynomials than me by now. This is one monster proof plus a bunch of beautiful code. I guess the only real question is whether one can cut down the monster proof. The literature apparently is leaving this stuff as an exercise. As far as I'm concerned, if it compiles, take it. I'm sure this proof will have taken a very long time to write. The general strategy in the file certainly looks sensible. Is there a short cut with the monster proof? I don't know one.
| /-- The polynomials that give the coefficients of `frobenius x`, | ||
| in terms of the coefficients of `x`. -/ | ||
| def frobenius_poly (n : ℕ) : mv_polynomial ℕ ℤ := | ||
| X n ^ p + C ↑p * (frobenius_poly_aux p n) |
There was a problem hiding this comment.
I see. You compute an explicit formula for the polys here.
| begin | ||
| generalize h : (v p ⟨j + 1, j.succ_pos⟩) = m, | ||
| suffices : m ≤ n - i ∧ m ≤ j, | ||
| { cases this, unfreezingI { clear_dependent p }, omega }, |
There was a problem hiding this comment.
This unfreezing nonsense is just buggy omega, right?
There was a problem hiding this comment.
We need it so that we can clear p (which is otherwise blocked by hp : fact p.prime). And we want to clear p to help omega a bit.
| apply nat.le_of_lt_succ, | ||
| calc m < p ^ m : nat.lt_pow_self hp.one_lt m | ||
| ... ≤ j + 1 : by { rw ← nat.sub_eq_of_eq_add hc, apply nat.sub_le } } | ||
| end |
There was a problem hiding this comment.
Probably this proof could be made slightly shorter at the expense of making some sort of an API for v, but given that it's a private def and one is forever wrestling with those gets because of enat I think this is fine.
There was a problem hiding this comment.
Making enat and multiplicity easier to use would be great. But I don't really know how to do that...
| add_left_comm, ← add_sub, ← add_sub, ← mul_sub, ← sum_sub_distrib], }, | ||
|
|
||
| -- now that we have managed to isolate `X n ^ p`, we gladly cancel it | ||
| rw [add_right_inj], |
There was a problem hiding this comment.
Here and on line 210 the square brackets aren't needed, but I don't know what the style guide says (they don't bother me, I'm just observing).
There was a problem hiding this comment.
My personal opinion is that it's harmless, and I'm happy to have both styles in mathlib. But I don't have a strong opinion.
Co-authored-by: Ruben-VandeVelde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
@Ruben-VandeVelde thanks for those comments! |
|
I really need to head to bed now, but here's a golfed version that I've been working on: lemma map_frobenius_poly (n : ℕ) :
mv_polynomial.map (int.cast_ring_hom ℚ) (frobenius_poly p n) = frobenius_poly_rat p n :=
begin
rw [frobenius_poly, ring_hom.map_add, ring_hom.map_mul, ring_hom.map_pow, map_C, map_X,
ring_hom.eq_int_cast, int.cast_coe_nat, frobenius_poly_rat],
apply nat.strong_induction_on n, clear n,
intros n IH,
rw [X_in_terms_of_W_eq],
simp only [alg_hom.map_sum, alg_hom.map_sub, alg_hom.map_mul, alg_hom.map_pow, bind₁_C_right],
have h1 : (↑p ^ n) * (⅟ (↑p : ℚ) ^ n) = 1 := by rw [←mul_pow, mul_inv_of_self, one_pow],
rw [bind₁_X_right, function.comp_app, witt_polynomial_eq_sum_C_mul_X_pow, sum_range_succ,
sum_range_succ, nat.sub_self, nat.add_sub_cancel_left, pow_zero, pow_one, pow_one, sub_mul,
add_mul, add_mul, mul_assoc, mul_assoc, mul_comm _ (C (⅟ ↑p ^ n)), mul_comm _ (C (⅟ ↑p ^ n)),
←mul_assoc, ←mul_assoc, ←C_mul, ←C_mul, pow_succ, mul_assoc ↑p (↑p ^ n) (⅟ ↑p ^ n), h1,
mul_one, C_1, one_mul, ←add_assoc, add_comm _ (X n ^ p), add_assoc, ←add_sub, add_right_inj],
rw [frobenius_poly_aux_eq, ring_hom.map_sub, map_X, mul_sub, ←add_sub, sub_eq_add_neg,
add_right_inj, neg_eq_iff_neg_eq, neg_sub],
simp only [ring_hom.map_sum, mul_sum, sum_mul, ←sum_sub_distrib],
apply sum_congr rfl,
intros i hi,
rw mem_range at hi,
rw [← IH i hi],
clear IH,
rw [add_comm (X i ^ p), add_pow, sum_range_succ', pow_zero, nat.sub_zero, nat.choose_zero_right,
one_mul, nat.cast_one, mul_one, mul_add, add_mul, nat.succ_sub (le_of_lt hi),
nat.succ_eq_add_one (n - i), pow_succ, pow_mul, add_sub_cancel, mul_sum, sum_mul],
apply sum_congr rfl,
intros j hj,
rw mem_range at hj,
rw [ring_hom.map_mul, ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_pow, ring_hom.map_pow,
ring_hom.map_pow, ring_hom.map_pow, map_C, map_X, mul_pow],
rw [mul_comm (C ↑p ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C ↑p ^ (j + 1)), mul_comm (C ↑p)],
simp only [mul_assoc],
have cancel : ∀ x y z : mv_polynomial ℕ ℚ, y = z → x * y = x * z := by { intros x y z h, rw h },
apply cancel,
apply cancel,
rw [←C_eq_coe_nat],
simp only [←ring_hom.map_pow, ←C_mul],
rw C_inj,
sorry,
end |
|
Wow, that's a pretty awesome golf! Thanks a lot @tb65536 |
|
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
Vierkantor
added
delegated
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
…f witt vectors (#4838) Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com