Smooth structures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[nontrivially_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_add_comm_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}
[nontrivially_normed_field 𝕜]
{H : Type u_2}
[topological_space H]
{E : Type u_3}
[normed_add_comm_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}
[nontrivially_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]
[nontrivially_normed_field 𝕜]
[normed_add_comm_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].