:: Derivation of Commutative Rings \& {L}eibnitz Formula for Power of
:: Derivation
:: by Yasushige Watase
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, NAT_1, MESFUNC1, VECTSP_2,
STRUCT_0, SUBSET_1, SUPINF_2, GROUP_1, POLYNOM1, POLYNOM3, FUNCSDOM,
HURWITZ, FINSEQ_1, ALGSEQ_1, FUNCT_1, RELAT_1, CARD_1, XBOOLE_0, NUMBERS,
MSSUBFAM, CARD_3, RLVECT_1, AFINSQ_1, PARTFUN1, XXREAL_0, XCMPLX_0,
ORDINAL4, RATFUNC1, NEWTON, ARYTM_1, FIELD_1, FUNCOP_1, ALGSTR_1,
BINOP_1, LATTICES, RFINSEQ, FINSEQ_3, FINSEQ_5, POLYDIFF, POLYNOM5,
FUNCT_2, RINGDER1, TOPGEN_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D,
FINSEQ_1, NEWTON, RFINSEQ, FINSEQ_5, FINSEQ_7, STRUCT_0, ALGSTR_0,
GROUP_1, VECTSP_1, ALGSTR_1, VECTSP_2, GROUP_4, POLYNOM1, ALGSEQ_1,
BINOM, POLYNOM3, RLVECT_1, POLYNOM5, HURWITZ, VECTSP11, RATFUNC1, RING_4,
POLYDIFF, FIELD_1;
constructors RELSET_1, NAT_D, FINSEQOP, NEWTON, RFINSEQ, FINSEQ_5, FINSEQ_7,
GROUP_4, FVSUM_1, ALGSEQ_1, GCD_1, BINOM, POLYNOM3, POLYNOM4, VECTSP11,
RATFUNC1, POLYDIFF, FIELD_1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, CARD_1, ORDINAL1, RELSET_1, MOD_4,
FUNCT_1, NAT_1, INT_1, POLYDIFF, FINSEQ_1, STRUCT_0, RLVECT_1, VECTSP_1,
ALGSTR_1, RING_3, RING_4, RING_5, POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1,
FUNCOP_1, RELAT_1, FDIFF_1, FUNCT_2, GR_CY_1, ALGSEQ_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
reserve L for Abelian left_zeroed add-associative associative right_zeroed
right_complementable distributive non empty doubleLoopStr;
reserve a,b,c for Element of L;
reserve R for non degenerated comRing;
reserve n,m,i,j,k for Nat;
:: Preliminaries
theorem :: RINGDER1:1
n*a + n*b = n*(a+b);
theorem :: RINGDER1:2
(n*a)*b = a*(n*b);
theorem :: RINGDER1:3
n*0.L = 0.L;
theorem :: RINGDER1:4
0.L*n = 0.L;
begin :: Definition of Derivation of Rings and Its Properties
:: Definition of Derivation of Rings and Its Properties
:::::::::::::::::::::::::::::::::::::
::: Derivation Hideyuki Matsumura "Commutative_Ring_Theory" Ch.9 p.190
::: Derivation D: R -> R
:::::::::::::::::::::::::::::::::::::::::::::::
reserve D for Function of R, R;
reserve x,y,z for Element of R;
definition
let R;
let IT be Function of R, R;
attr IT is derivation means
:: RINGDER1:def 1
for x,y be Element of R holds
IT.(x + y) = IT.x + IT.y &
IT.(x*y) = x*IT.y + y*IT.x;
end;
registration let R;
cluster derivation -> additive for Function of R,R;
end;
registration
let R;
cluster derivation for Function of R,R;
end;
definition
let R;
mode Derivation of R is derivation Function of R,R;
end;
definition
let R;
func Der(R) -> Subset of Funcs([#]R,[#]R) equals
:: RINGDER1:def 2
{f where f is Function of R,R : f is derivation };
end;
registration
let R;
cluster Der(R) -> non empty;
end;
reserve D for Derivation of R;
theorem :: RINGDER1:5
D.(1.R) = 0.R & D.(0.R) = 0.R;
theorem :: RINGDER1:6
for n,x holds D.(n*x) = n*D.x;
theorem :: RINGDER1:7
D.(x|^(m+1)) = (m+1)*((x|^m)*D.x);
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Power of Derivation D|^(n+1).f = D.(D|^n.f)
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: D|^2 is Function of the carrier of R,the carrier of R;
:: D|^3 is Function of the carrier of R,the carrier of R;
:: D|^0 = id R by VECTSP11:18;
:: R is non empty & D is Function of R,R;
:: dom D = the carrier of R by FUNCT_2:def 1;
:::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:8
(D|^(n+1)) = (D*D|^n) & dom D = the carrier of R &
dom (D|^n) = the carrier of R & D|^n is (the carrier of R)-valued Function;
theorem :: RINGDER1:9
for n,x holds (D|^(n+1)).x = D.((D|^n).x);
::::::::::::::::::::::::::::::::::::::::
::: D.(a/b) = (b*D.a - a*F.b)/b^2
::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:10
for x,y,z st z*y=1.R holds y|^2*D.(x*z) = (y*D.x -x*D.y);
reserve s for FinSequence of the carrier of R;
reserve h for Function of R,R;
definition
let R,s,h;
redefine func h*s -> FinSequence of the carrier of R;
end;
theorem :: RINGDER1:11
for h,s st h is additive holds h.(Sum s) = Sum(h*s);
::::::::::::::::::::::::::::::::::::::::::::::::
::: Formula
::: (f1 + f2 +...+fn)' = f1' + f2' +...+ fn'
::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:12
for D,s holds D.(Sum s) = Sum(D*s);
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Formula
:: (f1*f2*...*fn)' = f1'*f2...*fn + f1*f2'*..*fn +....+ f1*f2*f3*..*fn'
:: D.(Product s) = (f1*f2*...*fn)'
:: Sum DProd(D,s) = f1'*f2...fn + f1*f2'*....fn + f1*f2*f3'..
:: here DProd(D,s) = f1*..*D.fi*...*fn = Product( replace(s,i,D.fi))
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R,D,s;
func DProd(D,s) -> FinSequence of the carrier of R means
:: RINGDER1:def 3
len it = len s & for i st i in dom it holds
it.i = Product (Replace(s,i,D.(s/.i)));
end;
theorem :: RINGDER1:13
for s holds len s = 1 implies Sum DProd(D,s)= D.(Product s);
theorem :: RINGDER1:14
for t be FinSequence of the carrier of R st len t >= 1 holds
Sum DProd(D,t) = D.(Product t);
begin
:: Proof of Leibnitz Formula for Power of Derivations
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for power of a derivation of a commutative ring
:: LBZ(D,n,x,y) = <* nC0*(D^n.x), nC1*(D^(n-1).x)*(D.y),......*>
:: D^n(x+y) = nC0*(D^n.x) + nC1*(D^(n-1).x)*(D.y) +
:: D^n(x+y) = Sum LBZ(D,n,x,y)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R,D,n;
let x,y be Element of R;
func LBZ(D,n,x,y) -> FinSequence of the carrier of R means
:: RINGDER1:def 4
len it = n+1 & for i st i in dom it holds
it.i = (n choose (i-'1))*((D|^(n+1-'i)).x)*((D|^(i -' 1)).y);
end;
theorem :: RINGDER1:15
LBZ(D,0,x,y) = <* x*y *>;
theorem :: RINGDER1:16
LBZ(D,1,x,y) = <* y*D.x, x*D.y *>;
definition
let R,D,m;
let x,y be Element of R;
func LBZ0(D,m,x,y) -> FinSequence of the carrier of R means
:: RINGDER1:def 5
len it = m & for i st i in dom it holds
it.i = ((m choose (i-'1))+(m choose i))*((D|^(m+1 -'i)).x)*((D|^i).y);
end;
definition
let R,D,m;
let x,y be Element of R;
func LBZ1(D,m,x,y) -> FinSequence of the carrier of R means
:: RINGDER1:def 6
len it = m &
for i st i in dom it holds
it.i = (m choose (i-'1))*((D|^(m+1 -'i)).x)*((D|^i).y);
end;
definition
let R,D,m;
let x,y be Element of R;
func LBZ2(D,m,x,y) -> FinSequence of the carrier of R means
:: RINGDER1:def 7
len it = m &
for i st i in dom it holds
it.i = (m choose i)*((D|^(m +1 -'i)).x)*((D|^i).y);
end;
theorem :: RINGDER1:17
D.(Sum(LBZ0(D,n,x,y))) = Sum(D*(LBZ0(D,n,x,y)));
theorem :: RINGDER1:18
LBZ0(D,m,x,y) = LBZ1(D,m,x,y) + LBZ2(D,m,x,y);
theorem :: RINGDER1:19
Sum LBZ0(D,n,x,y) = Sum LBZ1(D,n,x,y) + Sum LBZ2(D,n,x,y);
theorem :: RINGDER1:20
D*LBZ0(D,n,x,y) = Del(LBZ2(D,n+1,x,y),n+1) + Del(LBZ1(D,n+1,x,y),1);
theorem :: RINGDER1:21
Sum(D*LBZ0(D,n,x,y)) =
- (LBZ1(D,n+1,x,y)/.1) + Sum LBZ0(D,n+1,x,y) - (LBZ2(D,n+1,x,y)/.(n+1));
theorem :: RINGDER1:22
LBZ(D,n+1,x,y) = <*((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y)*>
;
theorem :: RINGDER1:23
Sum(<* ((D|^(n+1)).x)*y *>^(LBZ0(D,n,x,y))^<* x*((D|^(n+1)).y) *>)
= ((D|^(n+1)).x)*y + Sum(LBZ0(D,n,x,y))+ x*((D|^(n+1)).y);
theorem :: RINGDER1:24
D.(Sum(LBZ(D,n+1,x,y))) = Sum(LBZ(D,n+2,x,y));
:::::::::::::::::::::::::::::::::::::::::::::::::
:: Leibniz Formula for Power of Derivation.
:::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: RINGDER1:25
(D|^n).(x*y) = Sum(LBZ(D,n,x,y));
begin
::Example of Derivation of Polynomial Ring over a Commutative Ring
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:::: formalize derivation of Polynom-Ring R.
:::: start with same fashion of poly_diff of POLYDIFF1:
:::: However resource of Def of poly_diff of POLYDIFF1 cannot be imported
:::: with the environment of this article technically.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Relations between
::: Element of the carrier of Polynom-Ring R and Polynomial of R
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R;
let f be Function of Polynom-Ring R, Polynom-Ring R;
let p be Element of the carrier of Polynom-Ring R;
redefine func f.p -> Element of the carrier of Polynom-Ring R;
end;
definition
let R be Ring;
func Der1(R) -> Function of Polynom-Ring R, Polynom-Ring R means
:: RINGDER1:def 8
for f being Element of the carrier of Polynom-Ring R
for i being Nat holds (it.f).i = (i+1)*f.(i+1);
end;
registration let R;
cluster Der1(R) -> additive;
end;
::::::::::::::::::::::::::::::::::::::
:: additive property for sequences
:: Map { f1, f2,...} -> {D_f1,D_f2,...}
:: (Der1(R))*p;
::::::::::::::::::::::::::::::::::::::::::
::::::::::::::::::::::::::::::::::::::::
:: Properties of Der1(R)
::::::::::::::::::::::::::::::::::::::::
reserve R for domRing;
reserve f,g for Element of the carrier of Polynom-Ring R;
theorem :: RINGDER1:26
for f be Element of the carrier of Polynom-Ring R, f1 be Polynomial of R
st f = f1 & f1 is constant holds (Der1(R)).f = 0_.R;
reserve a for Element of R;
theorem :: RINGDER1:27
for i be Nat, p be Element of the carrier of Polynom-Ring R
holds ((a|R)*'p).i = a*p.i;
theorem :: RINGDER1:28
for f,g being Element of the carrier of Polynom-Ring R, a be Element of R
st f = a|R holds (Der1(R)).(f*g) = (a|R)*'((Der1(R)).g);
theorem :: RINGDER1:29
for f being Element of the carrier of Polynom-Ring R, a be Element of R
st f = anpoly(a,0) holds (Der1(R)).f = 0_.R;
theorem :: RINGDER1:30
for f being Element of the carrier of Polynom-Ring R, a be Element of R
st f = anpoly(a,1) holds (Der1(R)).f = anpoly(a,0);
theorem :: RINGDER1:31
for p,q be Polynomial of R st p = anpoly(1.R,1) holds
for i be Element of NAT holds (p*'q).(i+1) = q.i &(p*'q).0 = 0.R;
theorem :: RINGDER1:32
for f,g be Element of the carrier of Polynom-Ring R
st f = anpoly(1.R,1) holds
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g);
theorem :: RINGDER1:33
for f, g be constant Element of the carrier of Polynom-Ring R holds
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g);
theorem :: RINGDER1:34
for f, g be Element of the carrier of Polynom-Ring R
st f is constant holds (Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g);
theorem :: RINGDER1:35
for x,y be Element of the carrier of Polynom-Ring R st x is non constant
holds (Der1(R)).(x*y) = ((Der1(R)).x)*y + x*((Der1(R)).y);
theorem :: RINGDER1:36
(Der1(R)).(f*g) = ((Der1(R)).f)*g + f*((Der1(R)).g);
registration let R;
cluster Der1(R) -> derivation;
end;
theorem :: RINGDER1:37
for x be Element of Polynom-Ring R, f be Polynomial of R
st x = f holds for n be Nat holds x|^n = f`^n;
theorem :: RINGDER1:38
for x be Element of Polynom-Ring R
st x = anpoly(1.R,1) holds ex y be Element of Polynom-Ring R
st y = anpoly(1.R,n) & (Der1(R)).(x|^(n+1)) = (n+1)*y;
reserve p for Polynomial of F_Real;
definition
let p;
func poly_diff(p) -> sequence of F_Real means
:: RINGDER1:def 9
for n being Nat holds it.n = p.(n+1) * (n+1);
end;
theorem :: RINGDER1:39
for p0 be Element of Polynom-Ring F_Real, p be Polynomial of F_Real
st p0 = p holds poly_diff(p) = (Der1(F_Real)).p0;