Derivation.ext
theorem Derivation.ext :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
{D1 D2 : Derivation R A M}, (∀ (a : A), D1 a = D2 a) → D1 = D2
This theorem states that for any types `R`, `A`, and `M`, given `R` and `A` are commutative semirings, `M` is an additive commutative monoid, and `M` is a module over both `R` and `A`, with `A` being an `R`-algebra, if you have two derivations `D1` and `D2` from `R` and `A` into `M`, and for every element `a` in `A`, `D1` applied to `a` equals `D2` applied to `a`, then `D1` and `D2` are identical. In simpler terms, if two derivations behave the same way for all elements of the algebra, then they are the same derivation.
More concisely: If `R` and `A` are commutative semirings, `M` is an additive commutative `R`-module and `A`-module, `A` is an `R`-algebra, and for all `a` in `A`, `D1 (a) = D2 (a)`, then `D1 = D2`.
|
Derivation.leibniz_of_mul_eq_one
theorem Derivation.leibniz_of_mul_eq_one :
∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
[inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) {a b : A},
a * b = 1 → D a = -a ^ 2 • D b
This theorem states that for any commutative ring `R`, ring `A`, and module `M` over `A` and `R` with a derivation `D` from `A` to `M`, if the product of two elements `a` and `b` in `A` equals 1, then the derivation of `a` is equal to the negative of `a` squared scaled by the derivation of `b`. This is a version of Leibniz rule specialized for the case when the product of `a` and `b` is 1. The theorem is a manifestation of the properties of derivations in the context of algebra.
More concisely: For any commutative rings `R`, ring `A`, module `M` over `A` and `R`, and derivation `D` from `A` to `M`, if `a` and `b` are elements of `A` with `a * b = 1`, then `D(a) = - a^2 * D(b)`.
|
Derivation.ext_of_adjoin_eq_top
theorem Derivation.ext_of_adjoin_eq_top :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
{D1 D2 : Derivation R A M} (s : Set A), Algebra.adjoin R s = ⊤ → Set.EqOn (⇑D1) (⇑D2) s → D1 = D2
The theorem `Derivation.ext_of_adjoin_eq_top` states that for any type `R` which is a commutative semiring, type `A` which is a commutative semiring, and type `M` which is an additive commutative monoid, if a set `s` of type `A` extends to form the whole algebra when adjoining with `R`, then any two derivations `D1` and `D2` from the algebra `R` to `M` that are equal on this set `s` must be equal on the whole algebra. In other words, if `D1` and `D2` have the same effect on the elements of `s`, then they have the same effect on all elements of the algebra.
More concisely: If `R` is a commutative semiring, `A` is a commutative semiring, `M` is an additive commutative monoid, `s ⊆ A` extends `R` to an algebra structure on `A`, and `D1` and `D2` are derivations from `R` to `M` agreeing on `s`, then `D1 = D2` on the whole algebra `A`.
|
Derivation.leibniz
theorem Derivation.leibniz :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
(D : Derivation R A M) (a b : A), D (a * b) = a • D b + b • D a
This theorem, named "Derivation.leibniz", states that for any types `R`, `A`, and `M` where `R` is a commutative semiring, `A` is also a commutative semiring, `M` is an additive commutative monoid, `A` is an `R`-algebra, `M` is an `A`-module and also an `R`-module, and `D` is a derivation from `A` to `M` over `R`, the Leibniz rule holds: the derivative of the product of `a` and `b` (where `a` and `b` are elements of `A`) is equal to `a` times the derivative of `b` plus `b` times the derivative of `a`. This is a formal representation of the Leibniz product rule in differential calculus.
More concisely: For a commutative semiring `R`, commutative `A`-algebra `A` over `R`, `A`-module and `R`-module `M`, and `R`-derivation `D` from `A` to `M`, the Leibniz rule holds: `D(a * b) = a * D(b) + b * D(a)`.
|
Derivation.eqOn_adjoin
theorem Derivation.eqOn_adjoin :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
{D1 D2 : Derivation R A M} {s : Set A}, Set.EqOn (⇑D1) (⇑D2) s → Set.EqOn ⇑D1 ⇑D2 ↑(Algebra.adjoin R s)
This theorem states that for any commutative semiring `R`, commutative semiring `A`, add-commutative monoid `M`, and any sets `D1` and `D2` of derivations from `R` to `A` to `M`, and any set `s` of `A`, if `D1` and `D2` are equal on `s` (i.e., for all elements `x` in `s`, applying `D1` and `D2` to `x` gives the same result), then `D1` and `D2` are also equal on `Algebra.adjoin R s` (i.e., the minimal subalgebra that includes `s`). In other words, if two derivations agree on a set, they also agree on the smallest subalgebra containing that set.
More concisely: For any commutative semirings `R` and `A`, add-commutative monoid `M`, sets `D1` and `D2` of derivations from `R` to `A` to `M`, and set `s` of `A`, if `D1` and `D2` agree on `s`, then they agree on the algebra generated by `s`.
|
Derivation.map_algebraMap
theorem Derivation.map_algebraMap :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
(D : Derivation R A M) (r : R), D ((algebraMap R A) r) = 0
The theorem `Derivation.map_algebraMap` asserts that for any commutative semiring `R`, any commutative semiring `A`, any additive commutative monoid `M`, any `R`-algebra structure on `A`, any `A`-module structure on `M`, and any `R`-module structure on `M`, for any derivation `D` from `A` to `M` over `R` and any element `r` of `R`, the derivation `D` applied to the image of `r` under the algebra map from `R` to `A` is equal to zero. In mathematical terms, if $R$ and $A$ are commutative semirings, $M$ is an additive commutative monoid, $A$ is an $R$-algebra, $M$ is an $A$-module and an $R$-module, and $D: A \rightarrow M$ is a derivation, then for all $r \in R$, $D(\phi(r)) = 0$ where $\phi: R \rightarrow A$ is the algebra map, i.e., $\phi(r)$ is the image of $r$ under the structure of the $R$-algebra.
More concisely: For any commutative semiring $R$, commutative semiring $A$, additive commutative monoid $M$, $R$-algebra structure on $A$, $A$-module and $R$-module structure on $M$, and derivation $D$ from $A$ to $M$ over $R$, $D(\phi(r)) = 0$ for all $r \in R$, where $\phi: R \rightarrow A$ is the algebra map.
|
Derivation.map_one_eq_zero
theorem Derivation.map_one_eq_zero :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
(D : Derivation R A M), D 1 = 0
This theorem states that for any derivation `D` from a commutative semiring `A` to an additive commutative monoid `M`, both with a common scalar field `R`, the derivation of the multiplicative identity (1) in `A` is the additive identity (0) in `M`. This holds under the conditions that `A` is an algebra over `R` and `M` is a module over both `R` and `A`.
More concisely: For any derivation from a commutative semiring with scalar field, into an additive commutative `R`-module, the multiplicative identity derives to the additive identity. (Assumes the semiring is an `R`-algebra and the module is an `A`-module.)
|
Derivation.map_smul
theorem Derivation.map_smul :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
(D : Derivation R A M) (r : R) (a : A), D (r • a) = r • D a
This theorem states that for any given derivation `D` from a commutative semiring `A` into an additive commutative monoid `M`, that is also an `A`-module and `R`-module, and for any scalar `r` from a commutative semiring `R` and any element `a` from `A`, the derivation of the scalar multiplication of `r` and `a` is equal to the scalar multiplication of `r` and the derivation of `a`. In formal terms, `D (r • a) = r • D a`. This property shows the compatibility of the derivation with scalar multiplication.
More concisely: For any commutative semiring homomorphism `D` from a commutative semiring `A` to an additive commutative monoid `M` that is also an `A`-module and `R`-module, `D (r * a) = r * D a` for all `r` in `R` and `a` in `A`.
|