feat(ring_theory/witt_vector): redefine subtraction using witt_sub polynomial (#5405)

Author: jcommelin

src/ring_theory/witt_vector/basic.lean

@@ -88,6 +88,8 @@ lemma one : map_fun f (1 : 𝕎 R) = 1 := by map_fun_tac
 
 lemma add : map_fun f (x + y) = map_fun f x + map_fun f y := by map_fun_tac
 
+lemma sub : map_fun f (x - y) = map_fun f x - map_fun f y := by map_fun_tac
+
 lemma mul : map_fun f (x * y) = map_fun f x * map_fun f y := by map_fun_tac
 
 lemma neg : map_fun f (-x) = -map_fun f x := by map_fun_tac
@@ -108,9 +110,11 @@ do fn ← to_expr ```(%%fn : fin _ → ℕ → R),
   to_expr ```(witt_structure_int_prop p (%%φ : mv_polynomial (fin %%k) ℤ) n) >>= note `aux none >>=
      apply_fun_to_hyp ```(aeval (uncurry %%fn)) none,
 `[simp only [aeval_bind₁] at aux,
-  simp only [pi.zero_apply, pi.one_apply, pi.add_apply, pi.mul_apply, pi.neg_apply, ghost_fun],
+  simp only [pi.zero_apply, pi.one_apply, pi.add_apply, pi.sub_apply, pi.mul_apply, pi.neg_apply,
+    ghost_fun],
   convert aux using 1; clear aux;
-  simp only [alg_hom.map_zero, alg_hom.map_one, alg_hom.map_add, alg_hom.map_mul, alg_hom.map_neg,
+  simp only [alg_hom.map_zero, alg_hom.map_one, alg_hom.map_add,
+    alg_hom.map_sub, alg_hom.map_mul, alg_hom.map_neg,
     aeval_X, aeval_rename]; refl]
 end tactic
 
@@ -137,6 +141,9 @@ private lemma ghost_fun_one : ghost_fun (1 : 𝕎 R) = 1 := by ghost_fun_tac 1 !
 private lemma ghost_fun_add : ghost_fun (x + y) = ghost_fun x + ghost_fun y :=
 by ghost_fun_tac (X 0 + X 1) ![x.coeff, y.coeff]
 
+private lemma ghost_fun_sub : ghost_fun (x - y) = ghost_fun x - ghost_fun y :=
+by ghost_fun_tac (X 0 - X 1) ![x.coeff, y.coeff]
+
 private lemma ghost_fun_mul : ghost_fun (x * y) = ghost_fun x * ghost_fun y :=
 by ghost_fun_tac (X 0 * X 1) ![x.coeff, y.coeff]
 
@@ -172,18 +179,18 @@ include hp
 
 local attribute [instance]
 private def comm_ring_aux₁ : comm_ring (𝕎 (mv_polynomial R ℚ)) :=
-(ghost_equiv' p (mv_polynomial R ℚ)).injective.comm_ring (ghost_fun)
-  ghost_fun_zero ghost_fun_one ghost_fun_add ghost_fun_mul ghost_fun_neg
+(ghost_equiv' p (mv_polynomial R ℚ)).injective.comm_ring_sub (ghost_fun)
+  ghost_fun_zero ghost_fun_one ghost_fun_add ghost_fun_mul ghost_fun_neg ghost_fun_sub
 
 local attribute [instance]
 private def comm_ring_aux₂ : comm_ring (𝕎 (mv_polynomial R ℤ)) :=
-(map_fun.injective _ $ map_injective (int.cast_ring_hom ℚ) int.cast_injective).comm_ring _
-  (map_fun.zero _) (map_fun.one _) (map_fun.add _) (map_fun.mul _) (map_fun.neg _)
+(map_fun.injective _ $ map_injective (int.cast_ring_hom ℚ) int.cast_injective).comm_ring_sub _
+  (map_fun.zero _) (map_fun.one _) (map_fun.add _) (map_fun.mul _) (map_fun.neg _) (map_fun.sub _)
 
 /-- The commutative ring structure on `𝕎 R`. -/
 instance : comm_ring (𝕎 R) :=
-(map_fun.surjective _ $ counit_surjective _).comm_ring (map_fun $ mv_polynomial.counit _)
-  (map_fun.zero _) (map_fun.one _) (map_fun.add _) (map_fun.mul _) (map_fun.neg _)
+(map_fun.surjective _ $ counit_surjective _).comm_ring_sub (map_fun $ mv_polynomial.counit _)
+  (map_fun.zero _) (map_fun.one _) (map_fun.add _) (map_fun.mul _) (map_fun.neg _) (map_fun.sub _)
 
 variables {p R}
 

src/ring_theory/witt_vector/defs.lean

@@ -104,10 +104,7 @@ witt_structure_int p 1
 def witt_add : ℕ → mv_polynomial (fin 2 × ℕ) ℤ :=
 witt_structure_int p (X 0 + X 1)
 
-/-- The polynomials used for describing the subtraction of the ring of Witt vectors.
-Note that `a - b` is defined as `a + -b`.
-See `witt_vector.sub_coeff` for a proof that subtraction is precisely
-given by these polynomials `witt_vector.witt_sub` -/
+/-- The polynomials used for describing the subtraction of the ring of Witt vectors. -/
 def witt_sub : ℕ → mv_polynomial (fin 2 × ℕ) ℤ :=
 witt_structure_int p (X 0 - X 1)
 
@@ -153,6 +150,9 @@ instance : has_one (𝕎 R) :=
 instance : has_add (𝕎 R) :=
 ⟨λ x y, eval (witt_add p) ![x, y]⟩
 
+instance : has_sub (𝕎 R) :=
+⟨λ x y, eval (witt_sub p) ![x, y]⟩
+
 instance : has_mul (𝕎 R) :=
 ⟨λ x y, eval (witt_mul p) ![x, y]⟩
 
@@ -281,6 +281,9 @@ variables {p R}
 lemma add_coeff (x y : 𝕎 R) (n : ℕ) :
   (x + y).coeff n = peval (witt_add p n) ![x.coeff, y.coeff] := rfl
 
+lemma sub_coeff (x y : 𝕎 R) (n : ℕ) :
+  (x - y).coeff n = peval (witt_sub p n) ![x.coeff, y.coeff] := rfl
+
 lemma mul_coeff (x y : 𝕎 R) (n : ℕ) :
   (x * y).coeff n = peval (witt_mul p n) ![x.coeff, y.coeff] := rfl
 
@@ -293,6 +296,10 @@ lemma witt_add_vars (n : ℕ) :
   (witt_add p n).vars ⊆ finset.univ.product (finset.range (n + 1)) :=
 witt_structure_int_vars _ _ _
 
+lemma witt_sub_vars (n : ℕ) :
+  (witt_sub p n).vars ⊆ finset.univ.product (finset.range (n + 1)) :=
+witt_structure_int_vars _ _ _
+
 lemma witt_mul_vars (n : ℕ) :
   (witt_mul p n).vars ⊆ finset.univ.product (finset.range (n + 1)) :=
 witt_structure_int_vars _ _ _

src/ring_theory/witt_vector/is_poly.lean

@@ -617,37 +617,4 @@ attribute [ghost_simps]
       nat.succ_ne_zero nat.add_sub_cancel nat.succ_eq_add_one
       if_true eq_self_iff_true if_false forall_true_iff forall_2_true_iff forall_3_true_iff
 
-/-!
-### Subtraction of Witt vectors
-
-In Lean, subtraction in a ring is by definition equal to `x + -y`.
-For Witt vectors, this means that subtraction is not defined in terms of
-the polynomials `witt_sub p`.
-
-As a demonstration of some of the techniques developed in this file,
-we show by a computation that evaluating `witt_sub p` on the coefficients of `x` and `y`
-gives the coefficients of `x - y`.
-
-For a more powerful demonstration, see `ring_theory/witt_vector/identities.lean`.
--/
-
-lemma sub_eq (x y : 𝕎 R) :
-  x - y = eval (witt_sub p) ![x, y] :=
-begin
-  apply is_poly₂.ext ((add_is_poly₂).comp_right
-    (neg_is_poly)) ⟨witt_sub p, by intros; refl⟩ _ _ x y,
-  unfreezingI { clear_dependent R }, introsI R _Rcr x y n,
-  simp only [←sub_eq_add_neg, ring_hom.map_sub],
-  symmetry,
-  have := witt_structure_int_prop p (X 0 - X 1 : mv_polynomial (fin 2) ℤ) n,
-  apply_fun (aeval (function.uncurry ![x.coeff, y.coeff])) at this,
-  simp only [aeval_bind₁, alg_hom.map_sub, bind₁_X_right] at this,
-  simp only [aeval_eq_eval₂_hom, eval₂_hom_rename] at this,
-  exact this,
-end
-
-lemma sub_coeff (x y : 𝕎 R) (n : ℕ) :
-  (x - y).coeff n = peval (witt_sub p n) ![x.coeff, y.coeff] :=
-by { rw [sub_eq], refl }
-
 end witt_vector