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]
structure
smooth_ring
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(R : Type u_4)
[semiring R]
[topological_space R]
[charted_space H R] :
Prop
- to_has_smooth_add : has_smooth_add I R
- smooth_mul : smooth (I.prod I) I (λ (p : R × R), p.fst * p.snd)
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 of this typeclass
@[protected, instance]
def
smooth_ring.to_has_smooth_mul
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(R : Type u_4)
[semiring R]
[topological_space R]
[charted_space H R]
[h : smooth_ring I R] :
has_smooth_mul I R
@[protected, instance]
def
smooth_ring.to_lie_add_group
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_group E]
[normed_space 𝕜 E]
(I : model_with_corners 𝕜 E H)
(R : Type u_4)
[ring R]
[topological_space R]
[charted_space H R]
[smooth_ring I R] :
lie_add_group I R
@[protected, instance]
def
field_smooth_ring
{𝕜 : Type u_1}
[nondiscrete_normed_field 𝕜] :
smooth_ring (model_with_corners_self 𝕜 𝕜) 𝕜
theorem
topological_semiring_of_smooth
{𝕜 : Type u_1}
{R : Type u_2}
{E : Type u_3}
{H : Type u_4}
[topological_space R]
[topological_space H]
[nondiscrete_normed_field 𝕜]
[normed_group E]
[normed_space 𝕜 E]
[charted_space H R]
(I : model_with_corners 𝕜 E H)
[semiring R]
[smooth_ring 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].