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 : Prop

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' : OpenPartialHomeomorph 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
• contMDiff_mul : ContMDiff (I.prod I) I n fun (p : R × R) => p.1 * p.2

@[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] : IsTopologicalSemiring 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].