Star operations on completions

A star operation extends to the completion through UniformSpace.Completion.map, and the extension is continuous. An additive, continuous star operation on a uniform additive group is uniformly continuous, TauCeti.uniformContinuous_star, so its extension agrees with it on the image of the group, UniformSpace.Completion.coe_star. The star monoid and star module laws then pass to the completion. No ring structure is involved; the star ring structure on completions of nonunital rings is UniformSpace.Completion.instStarRing in TauCeti.Topology.Algebra.UniformRing.

Main results

• TauCeti.uniformContinuous_star: an additive, continuous star operation on a uniform additive group is uniformly continuous.
• UniformSpace.Completion.instStar and UniformSpace.Completion.instContinuousStar: the continuous star operation on the completion.
• UniformSpace.Completion.coe_star: the inclusion into the completion commutes with star.
• UniformSpace.Completion.instStarAddMonoid and UniformSpace.Completion.instStarModule: the star additive monoid and star module laws pass to the completion.

theorem TauCeti.uniformContinuous_star {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [StarAddMonoid α] [ContinuousStar α] : UniformContinuous star

An additive, continuous star operation on a uniform additive group is uniformly continuous.

@[instance_reducible]

noncomputable instance UniformSpace.Completion.instStar {α : Type u_1} [UniformSpace α] [Star α] : Star (Completion α)

The star operation on the completion: the completion of the star operation of α.

instance UniformSpace.Completion.instContinuousStar {α : Type u_1} [UniformSpace α] [Star α] : ContinuousStar (Completion α)

The extended star operation is continuous, whatever the star operation of α.

@[simp]

theorem UniformSpace.Completion.coe_star {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [StarAddMonoid α] [ContinuousStar α] (a : α) : ↑(star a) = star ↑a

The inclusion into the completion commutes with an additive, continuous star operation.

@[instance_reducible]

noncomputable instance UniformSpace.Completion.instStarAddMonoid {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [StarAddMonoid α] [ContinuousStar α] : StarAddMonoid (Completion α)

The completion of a uniform additive group with an additive, continuous star operation is a star additive monoid.

instance UniformSpace.Completion.instStarModule {α : Type u_1} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [StarAddMonoid α] [ContinuousStar α] {R : Type u_2} [Monoid R] [Star R] [DistribMulAction R α] [UniformContinuousConstSMul R α] [StarModule R α] : StarModule R (Completion α)

A star module structure on α passes to the completion.