Smooth structures

In this file we define smooth structures that build on Lie groups. We prefer using the term smooth instead of Lie mainly because Lie ring has currently another use in mathematics.

class SmoothRing {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (R : Type u_4) [Semiring R] [TopologicalSpace R] [ChartedSpace H R] extends SmoothAdd : Prop

A smooth (semi)ring is a (semi)ring R where addition and multiplication are smooth. If R is a ring, then negation is automatically smooth, as it is multiplication with -1.

• compatible : ∀ {e e' : PartialHomeomorph R H}, e ∈ atlas H R → e' ∈ atlas H R → PartialHomeomorph.trans (PartialHomeomorph.symm e) e' ∈ contDiffGroupoid ⊤ I
• smooth_add : Smooth (ModelWithCorners.prod I I) I fun (p : R × R) => p.1 + p.2
• smooth_mul : Smooth (ModelWithCorners.prod I I) I fun (p : R × R) => p.1 * p.2

instance SmoothRing.toSmoothMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (R : Type u_4) [Semiring R] [TopologicalSpace R] [ChartedSpace H R] [h : SmoothRing I R] : SmoothMul I R

Equations

• (_ : SmoothMul I R) = (_ : SmoothMul I R)

instance SmoothRing.toLieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (R : Type u_4) [Ring R] [TopologicalSpace R] [ChartedSpace H R] [SmoothRing I R] : LieAddGroup I R

Equations

• (_ : LieAddGroup I R) = (_ : LieAddGroup I R)

instance fieldSmoothRing {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : SmoothRing (modelWithCornersSelf 𝕜 𝕜) 𝕜

Equations

• (_ : SmoothRing (modelWithCornersSelf 𝕜 𝕜) 𝕜) = (_ : SmoothRing (modelWithCornersSelf 𝕜 𝕜) 𝕜)

theorem topologicalSemiring_of_smooth {𝕜 : Type u_1} {R : Type u_2} {E : Type u_3} {H : Type u_4} [TopologicalSpace R] [TopologicalSpace H] [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ChartedSpace H R] (I : ModelWithCorners 𝕜 E H) [Semiring R] [SmoothRing I R] : TopologicalSemiring R

A smooth (semi)ring is a topological (semi)ring. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].