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
,
SmoothManifoldWithCorners
,
HasGroupoid
:
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.
Instances
theorem
SmoothRing.smooth_mul
{𝕜 : Type u_1}
:
∀ {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
{inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {R : Type u_4}
{inst_4 : Semiring R} {inst_5 : TopologicalSpace R} {inst_6 : ChartedSpace H R} [self : SmoothRing I R],
Smooth (I.prod I) I fun (p : R × R) => p.1 * p.2
@[instance 100]
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
- ⋯ = ⋯
@[instance 100]
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
- ⋯ = ⋯
@[instance 100]
instance
fieldSmoothRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
:
SmoothRing (modelWithCornersSelf 𝕜 𝕜) 𝕜
Equations
- ⋯ = ⋯
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]
:
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].