TrivSqZeroExt.eq_smul_exp_of_ne_zero
theorem TrivSqZeroExt.eq_smul_exp_of_ne_zero :
β (π : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field π] [inst_1 : CharZero π] [inst_2 : Field R]
[inst_3 : AddCommGroup M] [inst_4 : Algebra π R] [inst_5 : Module π M] [inst_6 : Module R M]
[inst_7 : Module Rα΅α΅α΅ M] [inst_8 : IsCentralScalar R M] [inst_9 : IsScalarTower π R M]
[inst_10 : TopologicalSpace R] [inst_11 : TopologicalSpace M] [inst_12 : TopologicalRing R]
[inst_13 : TopologicalAddGroup M] [inst_14 : ContinuousSMul R M] [inst_15 : ContinuousSMul Rα΅α΅α΅ M]
[inst_16 : T2Space R] [inst_17 : T2Space M] (x : TrivSqZeroExt R M),
x.fst β 0 β x = x.fst β’ NormedSpace.exp π (x.fstβ»ΒΉ β’ TrivSqZeroExt.inr x.snd)
This theorem, `TrivSqZeroExt.eq_smul_exp_of_ne_zero`, provides a more convenient version of `TrivSqZeroExt.eq_smul_exp_of_invertible` when `R` is a field. It states that for any `π`, a field, and for any extensions `R` and `M` with additional properties (e.g., `R` and `M` are both topological spaces, `R` is a topological ring, `M` is a topological additive group, scalar multiplication in `R` and `M` is continuous, etc.), if `x` is an element of the trivial square-zero extension of `M` over `R` and the first component of `x` is non-zero, then `x` can be represented as the scalar multiplication of the first component of `x` and the exponential of the scalar multiplication of the inverse of the first component of `x` and the second component of `x` via the canonical inclusion map into the trivial square-zero extension.
More concisely: If `R` is a field and `x` is in the trivial square-zero extension of a field `M` over `R` with non-zero first component, then `x` can be represented as the product of the first component and the exponential of the second component multiplied by the inverse of the first component in the extension.
|
TrivSqZeroExt.norm_def
theorem TrivSqZeroExt.norm_def :
β {R : Type u_3} {M : Type u_4} [inst : SeminormedRing R] [inst_1 : SeminormedAddCommGroup M]
(x : TrivSqZeroExt R M), βxβ = βx.fstβ + βx.sndβ
The theorem `TrivSqZeroExt.norm_def` states that for any type `R` which is a seminormed ring, and any type `M` which is a seminormed additive commutative group, the norm of an element `x` in the trivial square-zero extension of `M` over `R` is equal to the sum of the norms of the first and the second components of `x`. In other words, if `x` is an element from the trivial square-zero extension `R Γ M`, then `βxβ = βTrivSqZeroExt.fst xβ + βTrivSqZeroExt.snd xβ`, where β Β· β denotes the norm, `TrivSqZeroExt.fst x` retrieves the `R` component of `x`, and `TrivSqZeroExt.snd x` retrieves the `M` component of `x`.
More concisely: For any element `x` in the trivial square-zero extension of a seminormed additive commutative group `M` over a seminormed ring `R`, the norm of `x` is equal to the sum of the norms of its `R` and `M` components.
|
TrivSqZeroExt.eq_smul_exp_of_invertible
theorem TrivSqZeroExt.eq_smul_exp_of_invertible :
β (π : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field π] [inst_1 : CharZero π] [inst_2 : CommRing R]
[inst_3 : AddCommGroup M] [inst_4 : Algebra π R] [inst_5 : Module π M] [inst_6 : Module R M]
[inst_7 : Module Rα΅α΅α΅ M] [inst_8 : IsCentralScalar R M] [inst_9 : IsScalarTower π R M]
[inst_10 : TopologicalSpace R] [inst_11 : TopologicalSpace M] [inst_12 : TopologicalRing R]
[inst_13 : TopologicalAddGroup M] [inst_14 : ContinuousSMul R M] [inst_15 : ContinuousSMul Rα΅α΅α΅ M]
[inst_16 : T2Space R] [inst_17 : T2Space M] (x : TrivSqZeroExt R M) [inst_18 : Invertible x.fst],
x = x.fst β’ NormedSpace.exp π (β
x.fst β’ TrivSqZeroExt.inr x.snd)
The theorem `TrivSqZeroExt.eq_smul_exp_of_invertible` states that for any field π and types R and M representing a commutative ring and an additive commutative group respectively, given an algebra structure on R over π, a module structure on M over π and R, and assuming M is a central scalar and there's a scalar tower of π over R and M, if R and M are also topological spaces and R is a topological ring while M is a topological additive group, and the scalar multiplication in M is continuous, then for any element x of the Trivial Square-Zero Extension of M over R, if the first component of x is invertible, then x can be expressed as the scalar multiplication of the first component of x with the exponential of the product of the multiplicative inverse of the first component of x and the canonical embedding of the second component of x into the Trivial Square-Zero Extension. This is essentially expressing the element of the trivial square-zero extension in a polar form.
More concisely: Given a commutative ring R with algebra structure over a field π, an additive commutative group M with module and scalar tower structures over R and π, assuming M is central, R and M are topological spaces with continuous scalar multiplication, and the first component of an element x in the Trivial Square-Zero Extension of M over R is invertible, then x can be expressed as the scalar multiplication of the first component of x with the exponential of the product of its multiplicative inverse and the canonical embedding of the second component of x.
|
TrivSqZeroExt.hasSum_expSeries_of_smul_comm
theorem TrivSqZeroExt.hasSum_expSeries_of_smul_comm :
β (π : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field π] [inst_1 : CharZero π] [inst_2 : Ring R]
[inst_3 : AddCommGroup M] [inst_4 : Algebra π R] [inst_5 : Module π M] [inst_6 : Module R M]
[inst_7 : Module Rα΅α΅α΅ M] [inst_8 : SMulCommClass R Rα΅α΅α΅ M] [inst_9 : IsScalarTower π R M]
[inst_10 : IsScalarTower π Rα΅α΅α΅ M] [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M]
[inst_13 : TopologicalRing R] [inst_14 : TopologicalAddGroup M] [inst_15 : ContinuousSMul R M]
[inst_16 : ContinuousSMul Rα΅α΅α΅ M] (x : TrivSqZeroExt R M),
MulOpposite.op x.fst β’ x.snd = x.fst β’ x.snd β
β {e : R},
HasSum (fun n => (NormedSpace.expSeries π R n) fun x_1 => x.fst) e β
HasSum (fun n => (NormedSpace.expSeries π (TrivSqZeroExt R M) n) fun x_1 => x)
(TrivSqZeroExt.inl e + TrivSqZeroExt.inr (e β’ x.snd))
The theorem `TrivSqZeroExt.hasSum_expSeries_of_smul_comm` states that for any element `x` in the trivial square-zero extension of a ring `R` over a module `M`, if the product of `x.fst` (the first element of the pair in `x`) with `x.snd` (the second element of the pair in `x`) is equal to the product of the "opposite" of `x.fst` with `x.snd`, then for any element `e` in `R` such that the series given by applying the `n`-th term of the exponential series to `x.fst` converges to `e`, the series given by applying the `n`-th term of the exponential series to `x` converges to the sum of `inl e` and `inr (e β’ x.snd)`. Here, `inl` and `inr` are the canonical inclusion functions for `R` and `M` into the trivial square-zero extension of `R` over `M`, and `β’` denotes scalar multiplication.
More concisely: If `x` is an element in the trivial square-zero extension of a ring `R` over a module `M` such that `x.fst * x.snd = (-\textit{x.fst}) * x.snd`, then for any `e` in `R` for which the exponential series of `x.fst` converges to `e`, the exponential series of `x` converges to `inl e + inr (e * x.snd)`.
|
TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm
theorem TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm :
β (π : Type u_1) {R : Type u_3} {M : Type u_4} [inst : Field π] [inst_1 : CharZero π] [inst_2 : Ring R]
[inst_3 : AddCommGroup M] [inst_4 : Algebra π R] [inst_5 : Module π M] [inst_6 : Module R M]
[inst_7 : Module Rα΅α΅α΅ M] [inst_8 : SMulCommClass R Rα΅α΅α΅ M] [inst_9 : IsScalarTower π R M]
[inst_10 : IsScalarTower π Rα΅α΅α΅ M] [inst_11 : TopologicalSpace R] [inst_12 : TopologicalSpace M]
[inst_13 : TopologicalRing R] [inst_14 : TopologicalAddGroup M] [inst_15 : ContinuousSMul R M]
[inst_16 : ContinuousSMul Rα΅α΅α΅ M] (x : TrivSqZeroExt R M),
MulOpposite.op x.fst β’ x.snd = x.fst β’ x.snd β
β {e : R},
HasSum (fun n => (NormedSpace.expSeries π R n) fun x_1 => x.fst) e β
HasSum (fun n => ((NormedSpace.expSeries π (TrivSqZeroExt R M) n) fun x_1 => x).snd) (e β’ x.snd)
The theorem `TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm` states that for a field `π`, a ring `R`, and a module `M`, given certain conditions including commutativity of scalar multiplication, if the exponential series `exp R x.fst` converges to a value `e`, then the second element of the exponential series applied to the trivial square-zero extension `(exp R x).snd` converges to the scalar multiplication of `e` and `x.snd`. This theorem essentially connects the convergence of the exponential series in a ring with the convergence of the exponential series in a trivial square-zero extension of a module over the ring.
More concisely: Given a commutative ring `R`, a field extension `π/R`, a module `M` over `R`, and a convergent exponential series `exp R x`, the second element of the exponential series of the trivial square-zero extension `(exp R x).snd` equals the scalar multiplication of the first element `e` by `x.snd`.
|