Gluing inverse semigroups into a strongly continuous group

Two strongly continuous semigroups form the positive and negative halves of a strongly continuous group when their operators at equal times are mutual inverses. This file constructs the group by using the first semigroup at nonnegative times and the second one at nonpositive times.

The construction isolates the gluing step used in generation results for two-sided groups. In particular, a Stone-type construction can generate contraction semigroups for an operator and its negative separately, prove that their operators are inverse, and then apply StronglyContinuousSemigroup.toGroupOfInverse.

Main declarations

• TauCeti.Semigroups.StronglyContinuousSemigroup.comp_comm_of_inverse: operators from the two semigroups commute, even at different times.
• TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse: glue two mutually inverse C₀-semigroups into a C₀-group.
• TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_toSemigroup: the positive half of the glued group is the first semigroup.
• TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_reflect_toSemigroup: the positive half of the reflected group is the second semigroup.
• TauCeti.Semigroups.StronglyContinuousGroup.eq_toGroupOfInverse: conversely, a C₀-group is the group glued from its own two halves, so gluing is inverse to splitting.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.11.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.comp_comm_of_inverse {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) (s t : NNReal) : S s ∘SL T t = T t ∘SL S s

The operators of mutually inverse semigroups commute, also when their time parameters differ. This is the cancellation step needed for the mixed-sign cases in the group law.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) : StronglyContinuousGroup X

Glue two strongly continuous semigroups whose equal-time operators are mutual inverses into a strongly continuous group. The first semigroup supplies nonnegative times and the second supplies negative times, with time reflected at zero.

Equations

• S.toGroupOfInverse T hST hTS = { toFun := TauCeti.Semigroups.StronglyContinuousSemigroup.inverseGluingFun✝ S T, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) {t : ℝ} (ht : 0 ≤ t) : (S.toGroupOfInverse T hST hTS) t = S.realOperator t

At nonnegative time, the group obtained by gluing inverse semigroups is the first semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_apply_of_nonpos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) {t : ℝ} (ht : t ≤ 0) : (S.toGroupOfInverse T hST hTS) t = T.realOperator (-t)

At nonpositive time, the group obtained by gluing inverse semigroups is the second semigroup at the reflected time.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) : (S.toGroupOfInverse T hST hTS).toSemigroup = S

The forward semigroup of the group obtained by gluing inverse semigroups is the first semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse_reflect_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S T : StronglyContinuousSemigroup X) (hST : ∀ (t : NNReal), S t ∘SL T t = ContinuousLinearMap.id ℝ X) (hTS : ∀ (t : NNReal), T t ∘SL S t = ContinuousLinearMap.id ℝ X) : (S.toGroupOfInverse T hST hTS).reflect.toSemigroup = T

The forward semigroup of the reflected group obtained by gluing inverse semigroups is the second semigroup.

theorem TauCeti.Semigroups.StronglyContinuousGroup.toSemigroup_comp_reflect_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : NNReal) : U.toSemigroup t ∘SL U.reflect.toSemigroup t = ContinuousLinearMap.id ℝ X

The forward semigroup of a C₀-group and the forward semigroup of its reflection satisfy the first inverse hypothesis of TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse.

theorem TauCeti.Semigroups.StronglyContinuousGroup.reflect_toSemigroup_comp_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) (t : NNReal) : U.reflect.toSemigroup t ∘SL U.toSemigroup t = ContinuousLinearMap.id ℝ X

The forward semigroup of a C₀-group and the forward semigroup of its reflection satisfy the second inverse hypothesis of TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse.

theorem TauCeti.Semigroups.StronglyContinuousGroup.eq_toGroupOfInverse {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) {S T : StronglyContinuousSemigroup X} (hS : U.toSemigroup = S) (hT : U.reflect.toSemigroup = T) : U = S.toGroupOfInverse T ⋯ ⋯

Gluing is inverse to splitting. A C₀-group whose forward semigroup is S and whose reflected forward semigroup is T is the group glued from S and T. Together with toGroupOfInverse_toSemigroup and toGroupOfInverse_reflect_toSemigroup, this identifies the gluing construction as the two-sided inverse of splitting a C₀-group into its two halves, so a group can be recognized as a glued group without repeating a sign split.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.toGroupOfInverse_toSemigroup_reflect_toSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (U : StronglyContinuousGroup X) : U.toSemigroup.toGroupOfInverse U.reflect.toSemigroup ⋯ ⋯ = U

Gluing the two halves of a C₀-group recovers the group.