C^n structures #
In this file we define C^n structures that build on Lie groups. We prefer using the
term ContMDiffRing instead of Lie mainly because Lie ring has currently another use
in mathematics.
class
ContMDiffRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
(n : WithTop ℕ∞)
(R : Type u_4)
[Semiring R]
[TopologicalSpace R]
[ChartedSpace H R]
extends ContMDiffAdd I n R :
A C^n (semi)ring is a (semi)ring R where addition and multiplication are C^n.
If R is a ring, then negation is automatically C^n, as it is multiplication with -1.
- compatible {e e' : PartialHomeomorph R H} : e ∈ atlas H R → e' ∈ atlas H R → e.symm.trans e' ∈ contDiffGroupoid n I
- contMDiff_add : ContMDiff (I.prod I) I n fun (p : R × R) => p.1 + p.2
Instances
@[instance 100]
instance
ContMDiffRing.toContMDiffMul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : WithTop ℕ∞}
(I : ModelWithCorners 𝕜 E H)
(R : Type u_4)
[Semiring R]
[TopologicalSpace R]
[ChartedSpace H R]
[h : ContMDiffRing I n R]
:
ContMDiffMul I n R
@[instance 100]
instance
ContMDiffRing.toLieAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : WithTop ℕ∞}
(I : ModelWithCorners 𝕜 E H)
(R : Type u_4)
[Ring R]
[TopologicalSpace R]
[ChartedSpace H R]
[ContMDiffRing I n R]
:
LieAddGroup I n R
@[instance 100]
instance
instFieldContMDiffRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : WithTop ℕ∞}
:
ContMDiffRing (modelWithCornersSelf 𝕜 𝕜) n 𝕜
theorem
topologicalSemiring_of_contMDiffRing
{𝕜 : 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)
(n : WithTop ℕ∞)
[Semiring R]
[ContMDiffRing I n R]
:
A C^n (semi)ring is a topological (semi)ring. This is not an instance for technical reasons,
see note [Design choices about smooth algebraic structures].