-
Notifications
You must be signed in to change notification settings - Fork 307
/
Derivation.lean
164 lines (134 loc) · 7.51 KB
/
Derivation.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
/-
Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.Data.MvPolynomial.Supported
import Mathlib.RingTheory.Derivation.Basic
#align_import data.mv_polynomial.derivation from "leanprover-community/mathlib"@"b608348ffaeb7f557f2fd46876037abafd326ff3"
/-!
# Derivations of multivariate polynomials
In this file we prove that a derivation of `MvPolynomial σ R` is determined by its values on all
monomials `MvPolynomial.X i`. We also provide a constructor `MvPolynomial.mkDerivation` that
builds a derivation from its values on `X i`s and a linear equivalence
`MvPolynomial.mkDerivationEquiv` between `σ → A` and `Derivation (MvPolynomial σ R) A`.
-/
namespace MvPolynomial
open scoped BigOperators
noncomputable section
variable {σ R A : Type*} [CommSemiring R] [AddCommMonoid A] [Module R A]
[Module (MvPolynomial σ R) A]
section
variable (R)
/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`, as a linear map.
Use `MvPolynomial.mkDerivation` instead. -/
def mkDerivationₗ (f : σ → A) : MvPolynomial σ R →ₗ[R] A :=
Finsupp.lsum R fun xs : σ →₀ ℕ =>
(LinearMap.ringLmapEquivSelf R R A).symm <|
xs.sum fun i k => monomial (xs - Finsupp.single i 1) (k : R) • f i
#align mv_polynomial.mk_derivationₗ MvPolynomial.mkDerivationₗ
end
theorem mkDerivationₗ_monomial (f : σ → A) (s : σ →₀ ℕ) (r : R) :
mkDerivationₗ R f (monomial s r) =
r • s.sum fun i k => monomial (s - Finsupp.single i 1) (k : R) • f i :=
sum_monomial_eq <| LinearMap.map_zero _
#align mv_polynomial.mk_derivationₗ_monomial MvPolynomial.mkDerivationₗ_monomial
theorem mkDerivationₗ_C (f : σ → A) (r : R) : mkDerivationₗ R f (C r) = 0 :=
(mkDerivationₗ_monomial f _ _).trans (smul_zero _)
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mk_derivationₗ_C MvPolynomial.mkDerivationₗ_C
theorem mkDerivationₗ_X (f : σ → A) (i : σ) : mkDerivationₗ R f (X i) = f i :=
(mkDerivationₗ_monomial f _ _).trans <| by simp
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mk_derivationₗ_X MvPolynomial.mkDerivationₗ_X
@[simp]
theorem derivation_C (D : Derivation R (MvPolynomial σ R) A) (a : R) : D (C a) = 0 :=
D.map_algebraMap a
set_option linter.uppercaseLean3 false in
#align mv_polynomial.derivation_C MvPolynomial.derivation_C
@[simp]
theorem derivation_C_mul (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R) :
C (σ := σ) a • D f = a • D f := by
have : C (σ := σ) a • D f = D (C a * f) := by simp
rw [this, C_mul', D.map_smul]
/-- If two derivations agree on `X i`, `i ∈ s`, then they agree on all polynomials from
`MvPolynomial.supported R s`. -/
theorem derivation_eqOn_supported {D₁ D₂ : Derivation R (MvPolynomial σ R) A} {s : Set σ}
(h : Set.EqOn (D₁ ∘ X) (D₂ ∘ X) s) {f : MvPolynomial σ R} (hf : f ∈ supported R s) :
D₁ f = D₂ f :=
Derivation.eqOn_adjoin (Set.forall_mem_image.2 h) hf
#align mv_polynomial.derivation_eq_on_supported MvPolynomial.derivation_eqOn_supported
theorem derivation_eq_of_forall_mem_vars {D₁ D₂ : Derivation R (MvPolynomial σ R) A}
{f : MvPolynomial σ R} (h : ∀ i ∈ f.vars, D₁ (X i) = D₂ (X i)) : D₁ f = D₂ f :=
derivation_eqOn_supported h f.mem_supported_vars
#align mv_polynomial.derivation_eq_of_forall_mem_vars MvPolynomial.derivation_eq_of_forall_mem_vars
theorem derivation_eq_zero_of_forall_mem_vars {D : Derivation R (MvPolynomial σ R) A}
{f : MvPolynomial σ R} (h : ∀ i ∈ f.vars, D (X i) = 0) : D f = 0 :=
show D f = (0 : Derivation R (MvPolynomial σ R) A) f from derivation_eq_of_forall_mem_vars h
#align mv_polynomial.derivation_eq_zero_of_forall_mem_vars MvPolynomial.derivation_eq_zero_of_forall_mem_vars
@[ext]
theorem derivation_ext {D₁ D₂ : Derivation R (MvPolynomial σ R) A} (h : ∀ i, D₁ (X i) = D₂ (X i)) :
D₁ = D₂ :=
Derivation.ext fun _ => derivation_eq_of_forall_mem_vars fun i _ => h i
#align mv_polynomial.derivation_ext MvPolynomial.derivation_ext
variable [IsScalarTower R (MvPolynomial σ R) A]
theorem leibniz_iff_X (D : MvPolynomial σ R →ₗ[R] A) (h₁ : D 1 = 0) :
(∀ p q, D (p * q) = p • D q + q • D p) ↔ ∀ s i, D (monomial s 1 * X i) =
(monomial s 1 : MvPolynomial σ R) • D (X i) + (X i : MvPolynomial σ R) • D (monomial s 1) := by
refine' ⟨fun H p i => H _ _, fun H => _⟩
have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
have : ∀ p i, D (p * X i) = p • D (X i) + (X i : MvPolynomial σ R) • D p := by
intro p i
induction' p using MvPolynomial.induction_on' with s r p q hp hq
· rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc,
smul_add, D.map_smul, smul_comm r (X i)]
· rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
intro p q
induction q using MvPolynomial.induction_on with
| h_C c =>
rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
| h_add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
| h_X q i hq =>
simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
rw [smul_comm (X i), smul_comm (X i)]
set_option linter.uppercaseLean3 false in
#align mv_polynomial.leibniz_iff_X MvPolynomial.leibniz_iff_X
variable (R)
/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`. -/
def mkDerivation (f : σ → A) : Derivation R (MvPolynomial σ R) A where
toLinearMap := mkDerivationₗ R f
map_one_eq_zero' := mkDerivationₗ_C _ 1
leibniz' :=
(leibniz_iff_X (mkDerivationₗ R f) (mkDerivationₗ_C _ 1)).2 fun s i => by
simp only [mkDerivationₗ_monomial, X, monomial_mul, one_smul, one_mul]
rw [Finsupp.sum_add_index'] <;>
[skip; simp; (intros; simp only [Nat.cast_add, (monomial _).map_add, add_smul])]
rw [Finsupp.sum_single_index, Finsupp.sum_single_index] <;> [skip; simp; simp]
rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm,
Finsupp.smul_sum]
refine' congr_arg₂ (· + ·) rfl (Finset.sum_congr rfl fun j hj => _); dsimp only
rw [smul_smul, monomial_mul, one_mul, add_comm s, add_tsub_assoc_of_le]
rwa [Finsupp.single_le_iff, Nat.succ_le_iff, pos_iff_ne_zero, ← Finsupp.mem_support_iff]
#align mv_polynomial.mk_derivation MvPolynomial.mkDerivation
@[simp]
theorem mkDerivation_X (f : σ → A) (i : σ) : mkDerivation R f (X i) = f i :=
mkDerivationₗ_X f i
set_option linter.uppercaseLean3 false in
#align mv_polynomial.mk_derivation_X MvPolynomial.mkDerivation_X
theorem mkDerivation_monomial (f : σ → A) (s : σ →₀ ℕ) (r : R) :
mkDerivation R f (monomial s r) =
r • s.sum fun i k => monomial (s - Finsupp.single i 1) (k : R) • f i :=
mkDerivationₗ_monomial f s r
#align mv_polynomial.mk_derivation_monomial MvPolynomial.mkDerivation_monomial
/-- `MvPolynomial.mkDerivation` as a linear equivalence. -/
def mkDerivationEquiv : (σ → A) ≃ₗ[R] Derivation R (MvPolynomial σ R) A :=
LinearEquiv.symm <|
{ invFun := mkDerivation R
toFun := fun D i => D (X i)
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl
left_inv := fun _ => derivation_ext <| mkDerivation_X _ _
right_inv := fun _ => funext <| mkDerivation_X _ _ }
#align mv_polynomial.mk_derivation_equiv MvPolynomial.mkDerivationEquiv
end
end MvPolynomial