map_frobeniusPoly — Mathlib

English

For all p, n, the map that substitutes frobeniusPolyRat p into wittPolynomial p ℚ n yields the WittPolynomial with index n+1.

Русский

Для любого p, n отображение подстановки frobeniusPolyRat(p) в WittPolynomial p ℚ n даёт WittPolynomial p ℚ с индексом n+1.

LaTeX

$$$\text{bind}_1(\text{frobeniusPolyRat}(p))(\mathrm{wittPolynomial}(p,\mathbb{Q},n)) = \mathrm{wittPolynomial}(p,\mathbb{Q},n+1).$$$

Lean4

theorem map_frobeniusPoly (n : ℕ) : MvPolynomial.map (Int.castRingHom ℚ) (frobeniusPoly p n) = frobeniusPolyRat p n :=
  by
  rw [frobeniusPoly, RingHom.map_add, RingHom.map_mul, RingHom.map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]
  refine Nat.strong_induction_on n ?_; clear n
  intro n IH
  rw [xInTermsOfW_eq]
  simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]
  have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
  rw [bind₁_X_right, Function.comp_apply, wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ, sum_range_succ, tsub_self,
    add_tsub_cancel_left, pow_zero, pow_one, pow_one, sub_mul, add_mul, add_mul, mul_right_comm,
    mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ', mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one,
    C_1, one_mul, add_comm _ (X n ^ p), add_assoc, ← add_sub, add_right_inj, frobeniusPolyAux_eq, RingHom.map_sub,
    map_X, mul_sub, sub_eq_add_neg, add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub, add_right_inj, neg_eq_iff_eq_neg,
    neg_sub, eq_comm]
  simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib]
  apply sum_congr rfl
  intro 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, tsub_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_right, mul_sum, sum_mul]
  apply sum_congr rfl
  intro j hj
  rw [mem_range] at hj
  rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow,
    RingHom.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]
  apply congr_arg
  apply congr_arg
  rw [← C_eq_coe_nat]
  simp only [← RingHom.map_pow, ← C_mul]
  rw [C_inj]
  simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul]
  rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)]
  push_cast
  linear_combination (norm := skip)
    -p / p ^ n / p ^ (n - i - v p (j + 1)) * (p ^ (n - i)).choose (j + 1) *
      congr((p : ℚ) ^ $(map_frobeniusPoly.key₂ p hi.le hj))
  field_simp [hp.1.ne_zero]
  ring

Похожие утверждения