Results on triv_sq_zero_ext R M
related to the norm #
For now, this file contains results about exp
for this type.
Main results #
TODO #
- Actually define a sensible norm on
triv_sq_zero_ext R M
, so that we have access to lemmas likeexp_add
. - Generalize some of these results to non-commutative
R
.
theorem
triv_sq_zero_ext.has_sum_exp_series
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[topological_space R]
[topological_space M]
[field ๐]
[char_zero ๐]
[comm_ring R]
[add_comm_group M]
[algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
(x : triv_sq_zero_ext R M)
{e : R}
(h : has_sum (ฮป (n : โ), โ(exp_series ๐ R n) (ฮป (_x : fin n), x.fst)) e) :
has_sum (ฮป (n : โ), โ(exp_series ๐ (triv_sq_zero_ext R M) n) (ฮป (_x : fin n), x)) (triv_sq_zero_ext.inl e + triv_sq_zero_ext.inr (e โข x.snd))
If exp R x.fst
converges to e
then exp R x
converges to inl e + inr (e โข x.snd)
.
theorem
triv_sq_zero_ext.exp_def
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M) :
@[simp]
theorem
triv_sq_zero_ext.fst_exp
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M) :
@[simp]
theorem
triv_sq_zero_ext.snd_exp
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M) :
@[simp]
theorem
triv_sq_zero_ext.exp_inl
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : R) :
exp ๐ (triv_sq_zero_ext.inl x) = triv_sq_zero_ext.inl (exp ๐ x)
@[simp]
theorem
triv_sq_zero_ext.exp_inr
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(m : M) :
exp ๐ (triv_sq_zero_ext.inr m) = 1 + triv_sq_zero_ext.inr m
theorem
triv_sq_zero_ext.eq_smul_exp_of_invertible
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_comm_ring R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M)
[invertible x.fst] :
Polar form of trivial-square-zero extension.
theorem
triv_sq_zero_ext.eq_smul_exp_of_ne_zero
(๐ : Type u_1)
{R : Type u_2}
{M : Type u_3}
[is_R_or_C ๐]
[normed_field R]
[add_comm_group M]
[normed_algebra ๐ R]
[module R M]
[module Rแตแตแต M]
[is_central_scalar R M]
[module ๐ M]
[is_scalar_tower ๐ R M]
[topological_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M)
(hx : x.fst โ 0) :
More convenient version of triv_sq_zero_ext.eq_smul_exp_of_invertible
for when R
is a
field.