feat(RingTheory/WittVector): the Teichmuller series

[jjdishere]

In this PR, we show that every element x of the Witt vectors 𝕎 R can be written as the (p-adic) summation of the Teichmuller series. Instead of using tsum, we only show that p ^ (n + 1) divides x minus the summation of the first n + 1 terms of the Teichmuller series. We also show that if p divides the first (n + 1) coefficients of a Witt vector, then p^(n+1) divides the n-th ghost component.

#21564 depends on this PR.

---

[github-actions]

PR summary f0022bcb63

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.WittVector.TeichmullerSeries (new file)	1535

---

Declarations diff

+ coe_one
+ coe_pow
+ dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff
+ eq_of_apply_teichmuller_eq
+ inv_apply
+ iterate_frobeniusEquiv_symm_pow_p_pow
+ map_eq_zero_iff
+ map_id
+ mul_apply
+ one_apply
+ one_eq_refl
+ pow_dvd_ghostComponent_of_dvd_coeff
+ sum_coeff_eq_coeff_sum
+ teichmuller_mul_pow_coeff
+ teichmuller_mul_pow_coeff_of_ne

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[riccardobrasca]

Do we really need those? I mean, nothing against them, but if we add them for RingEquiv we should do the same for all other equivs.

[jjdishere]

I believe we need these lemmas, especially those tagged with [simp]. Currently, the simp normal form will stop at (1 : R ≃+* R) x without any lemma that can further modify the proof state.

I'll add similar lemmas for other equivs in another PR.

[jjdishere]

It seems the corresponding lemmas already exist for MulAut and AddAut. see MulAut.one_def, MulAut.coe_one

AlgAut doesn't exist yet.

I'll check more and open the PR for aut lemmas later.

[riccardobrasca]

Suggested change

	@[simp]
	theorem iterate_frobeniusEquiv_symm_pow_p_pow (R : Type*) (p : ℕ)
	[CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) (n : ℕ) :
	((_root_.frobeniusEquiv R p).symm ^[n]) x ^ (p ^ n) = x := by
	revert x
	induction' n with n ih
	· simp
	· intro x
	simp [pow_succ, pow_mul, ih]
	@[simp]
	theorem iterate_frobeniusEquiv_symm_pow_p_pow (x : R) (n : ℕ) :
	((frobeniusEquiv R p).symm ^[n]) x ^ (p ^ n) = x := by
	induction n generalizing x with
	| zero => simp
	| succ n ih => simp [pow_succ, pow_mul, ih]

R is already in scope, and you can use induction n generalizing x.

[riccardobrasca]

Suggested change

	@[simp]
	theorem map_id (R : Type*) [CommRing R] :
	WittVector.map (RingHom.id R) = RingHom.id (𝕎 R) := by
	ext
	simp
	theorem map_eq_zero_iff {p : ℕ} {R S : Type*} [CommRing R] [CommRing S] [Fact (Nat.Prime p)]
	(f : R →+* S) {x : WittVector p R} :
	((map f) x) = 0 ↔ ∀ n, f (x.coeff n) = 0 := by
	refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
	· apply_fun (fun x ↦ x.coeff n) at h
	simpa using h
	· ext n
	simpa using h n
	variable (R) in
	@[simp]
	theorem map_id : WittVector.map (RingHom.id R) = RingHom.id (𝕎 R) := by
	ext; simp
	theorem map_eq_zero_iff (f : R →+* S) {x : WittVector p R} :
	((map f) x) = 0 ↔ ∀ n, f (x.coeff n) = 0 := by
	refine ⟨fun h n ↦ ?_, fun h ↦ ?_⟩
	· apply_fun (·.coeff n) at h
	simpa using h
	· ext n
	simpa using h n

[riccardobrasca]

Suggested change

	rw [this]
	have : n + 1 = (n - i) + 1 + i := by omega
	nth_rw 1 [this]
	rw [pow_add, mul_comm]
	rw [this, show n + 1 = (n - i) + 1 + i by omega, pow_add, mul_comm]

[riccardobrasca]

Suggested change

	refine (pow_dvd_pow_of_dvd ?_ _).trans (b := (x.coeff i) ^ (n - i + 1)) (pow_dvd_pow _ ?_)
	refine (pow_dvd_pow_of_dvd ?_ _).trans (pow_dvd_pow _ ?_)

[riccardobrasca]

Can you use induction ... generalizing ... here?

[riccardobrasca]

Can you add a variable {R : Type*} ... line?

[riccardobrasca]

Suggested change

	rw [Finset.sum_congr rfl (g := fun x : ℕ ↦ (0 : R))]
	· simp
	rw [Finset.sum_congr rfl (g := g)]
	· simp [g]

It looks nicer to me, but not very important.

[riccardobrasca]

Suggested change

	have := of_not_not ((teichmuller_mul_pow_coeff_of_ne _).mt ha)
	rw [← this]
	have := of_not_not ((teichmuller_mul_pow_coeff_of_ne _).mt hb)
	exact this
	rw [← of_not_not ((teichmuller_mul_pow_coeff_of_ne _).mt ha)]
	exact of_not_not ((teichmuller_mul_pow_coeff_of_ne _).mt hb)