Banach-algebra exponentials as units

The exponential of an element of a complete normed rational algebra is invertible, with inverse the exponential of its negation. This file packages that fact as a units-valued map TauCeti.expUnit : R → Rˣ. For real algebras, it also bundles the exponential along a line as a continuous one-parameter subgroup.

This is the Banach-algebra model for the exponential map of a Lie group. The later abstract construction should recover expUnit when specialized to the Lie group Rˣ.

Main definitions

• TauCeti.expUnit: NormedSpace.exp x, regarded as a unit of the algebra.
• TauCeti.expUnitHom: the continuous one-parameter subgroup generated by x.

Main results

• TauCeti.expUnit_coe: coercing expUnit x back to the algebra gives NormedSpace.exp x.
• TauCeti.continuous_expUnit: the units-valued exponential is continuous.
• TauCeti.expUnit_add_of_commute: the exponential addition law as an equality of units.
• TauCeti.expUnit_zero, TauCeti.expUnit_neg: the identity and inverse laws.
• TauCeti.expUnit_add_smul: the one-parameter subgroup law as an equality of units.
• TauCeti.coe_expUnitHom_real, TauCeti.coe_expUnitHom_complex: on ℝ and ℂ, the one-parameter subgroup is t ↦ exp (t * x) for the scalar exponential.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The matrix and circle shadows".

noncomputable def TauCeti.expUnit {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] (x : R) : Rˣ

The exponential of an element of a complete normed rational algebra, regarded as a unit.

Invertibility follows from NormedSpace.isUnit_exp; TauCeti.expUnit_neg below identifies its inverse with the unit represented by NormedSpace.exp (-x).

Equations

• TauCeti.expUnit x = ⋯.unit

@[simp]

theorem TauCeti.expUnit_coe {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] (x : R) : ↑(expUnit x) = NormedSpace.exp x

Coercing expUnit x to the algebra recovers NormedSpace.exp x.

theorem TauCeti.continuous_expUnit {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] : Continuous expUnit

The Banach-algebra exponential is continuous as a map into the group of units.

theorem TauCeti.expUnit_add_of_commute {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] {x y : R} (hxy : Commute x y) : expUnit (x + y) = expUnit x * expUnit y

The exponential addition law for commuting elements, lifted to the group of units.

@[simp]

theorem TauCeti.expUnit_zero {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] : expUnit 0 = 1

The exponential of zero is the identity unit.

@[simp]

theorem TauCeti.expUnit_neg {R : Type u_1} [NormedRing R] [NormedAlgebra ℚ R] [CompleteSpace R] (x : R) : expUnit (-x) = (expUnit x)⁻¹

The exponential of a negation is the inverse unit.

@[simp]

theorem TauCeti.expUnit_add_smul {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) (s t : ℝ) : expUnit ((s + t) • x) = expUnit (s • x) * expUnit (t • x)

The one-parameter subgroup law lifted from the algebra to its group of units.

noncomputable def TauCeti.expUnitHom {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : Multiplicative ℝ →ₜ* Rˣ

The Banach-algebra exponential along the line through x, bundled as a continuous homomorphism from the additive real line (written multiplicatively) to Rˣ.

Equations

• TauCeti.expUnitHom x = { toFun := fun (t : Multiplicative ℝ) => TauCeti.expUnit (Multiplicative.toAdd t • x), map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.expUnitHom_apply {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) (t : ℝ) : (expUnitHom x) (Multiplicative.ofAdd t) = expUnit (t • x)

Evaluating expUnitHom x at time t gives expUnit (t • x).

theorem TauCeti.coe_expUnitHom_real (x t : ℝ) : ↑((expUnitHom x) (Multiplicative.ofAdd t)) = Real.exp (t * x)

On the real line, expUnitHom x is t ↦ Real.exp (t * x).

theorem TauCeti.coe_expUnitHom_complex (s : ℂ) (t : ℝ) : ↑((expUnitHom s) (Multiplicative.ofAdd t)) = Complex.exp (↑t * s)

On the complex numbers, expUnitHom s is t ↦ Complex.exp (t * s).