One-parameter subgroups from the Banach algebra exponential

For an element x of a complete normed real algebra, TauCeti.expUnitHom bundles t ↦ expUnit (t • x) as a continuous one-parameter subgroup. This file records the smoothness and initial velocity of its underlying curve, and characterizes the subgroup by that velocity.

This is the concrete Banach-algebra model for the one-parameter subgroups associated to a future abstract Lie-group exponential map.

Main results

• TauCeti.contDiff_exp_smul: the algebra-valued exponential curve is real analytic.
• TauCeti.contMDiff_expUnit_smul: the corresponding units-valued curve is real analytic.
• TauCeti.contMDiff_expUnitHom: the bundled subgroup's underlying curve is real analytic.
• TauCeti.hasDerivAt_expUnitHom_val_zero: its initial velocity is x.
• TauCeti.continuousMonoidHom_eq_expUnitHom_of_hasDerivAt: it is the unique continuous one-parameter subgroup with that initial velocity.
• TauCeti.expUnitHom_injective: distinct velocities generate distinct one-parameter subgroups.
• TauCeti.expUnitHom_inj: the resulting equality normal form.
• TauCeti.eq_of_forall_exp_smul_eq: agreeing exponential lines have equal generators.
• TauCeti.existsUnique_eq_expUnitHom: a continuous one-parameter subgroup of Rˣ whose underlying curve is differentiable at 0 is expUnitHom x for a unique x : R.

References

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

theorem TauCeti.contDiff_exp_smul {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : ContDiff ℝ ⊤ fun (t : ℝ) => NormedSpace.exp (t • x)

The algebra-valued exponential curve t ↦ exp (t • x) is real analytic.

theorem TauCeti.contMDiff_expUnit_smul {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ R) ⊤ fun (t : ℝ) => expUnit (t • x)

The units-valued exponential curve t ↦ expUnit (t • x) is real analytic.

theorem TauCeti.contMDiff_expUnitHom {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ R) ⊤ fun (t : ℝ) => (expUnitHom x) (Multiplicative.ofAdd t)

The curve underlying expUnitHom x is real analytic.

theorem TauCeti.hasDerivAt_expUnitHom_val_zero {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (x : R) : HasDerivAt (fun (t : ℝ) => ↑((expUnitHom x) (Multiplicative.ofAdd t))) x 0

After embedding Rˣ in its model space R, the initial velocity of expUnitHom x is x.

Since the manifold structure on Rˣ is induced by this open embedding, this is the concrete tangent-space statement for the one-parameter subgroup.

theorem TauCeti.continuousMonoidHom_eq_expUnitHom_of_hasDerivAt {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (φ : Multiplicative ℝ →ₜ* Rˣ) (x : R) (hφ : HasDerivAt (fun (t : ℝ) => ↑(φ (Multiplicative.ofAdd t))) x 0) : φ = expUnitHom x

A continuous one-parameter subgroup of Rˣ is determined by its initial velocity in R.

theorem TauCeti.expUnitHom_injective {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] : Function.Injective expUnitHom

Distinct velocities generate distinct one-parameter subgroups: the generator is recovered from expUnitHom x as the initial velocity of its underlying curve.

@[simp]

theorem TauCeti.expUnitHom_inj {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] {x y : R} : expUnitHom x = expUnitHom y ↔ x = y

Two exponential one-parameter subgroups agree exactly when their velocities do.

theorem TauCeti.eq_of_forall_exp_smul_eq {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] {x y : R} (h : ∀ (t : ℝ), NormedSpace.exp (t • x) = NormedSpace.exp (t • y)) : x = y

Exponential lines determine their generators. If exp (t • x) = exp (t • y) for every real t then x = y. Comparing an exponential line with a known one therefore identifies its generator.

theorem TauCeti.existsUnique_eq_expUnitHom {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] [CompleteSpace R] (φ : Multiplicative ℝ →ₜ* Rˣ) (hφ : DifferentiableAt ℝ (fun (t : ℝ) => ↑(φ (Multiplicative.ofAdd t))) 0) : ∃! x : R, φ = expUnitHom x

The differentiable one-parameter subgroups of Rˣ are exactly the exponentials. A continuous one-parameter subgroup whose underlying curve is differentiable at 0 is expUnitHom x for a unique x : R. Together with expUnitHom_injective this identifies the one-parameter subgroups satisfying that differentiability hypothesis with R, the Lie algebra of Rˣ. The unrestricted bijection between all of ContinuousMonoidHom (Multiplicative ℝ) Rˣ and R needs the automatic-smoothness theorem that a merely continuous one-parameter subgroup is already differentiable, which is not proved here. The differentiability hypothesis is stated for the R-valued curve, since that is where the Banach-space derivative lives.