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.
@[instance]
def
smooth_semiring.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]
[self : smooth_semiring I R] :
has_smooth_mul I R
@[class]
structure
smooth_semiring
{𝕜 : 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
- compatible : ∀ {e e' : local_homeomorph R H}, e ∈ atlas H R → e' ∈ atlas H R → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_add : smooth (I.prod I) I (λ (p : R × R), p.fst + p.snd)
- smooth_mul : smooth (I.prod I) I (λ (p : R × R), (p.fst) * p.snd)
A smooth semiring is a semiring where addition and multiplication are smooth.
Instances
@[instance]
def
smooth_semiring.to_has_smooth_add
{𝕜 : 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]
[self : smooth_semiring I R] :
has_smooth_add I R
@[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)
[ring R]
[topological_space R]
[charted_space H R]
[self : smooth_ring I R] :
has_smooth_mul I R
@[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]
[self : smooth_ring I R] :
lie_add_group I R
@[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)
[ring R]
[topological_space R]
[charted_space H R] :
Prop
- compatible : ∀ {e e' : local_homeomorph R H}, e ∈ atlas H R → e' ∈ atlas H R → e.symm ≫ₕ e' ∈ times_cont_diff_groupoid ⊤ I
- smooth_add : smooth (I.prod I) I (λ (p : R × R), p.fst + p.snd)
- smooth_neg : smooth I I (λ (a : R), -a)
- smooth_mul : smooth (I.prod I) I (λ (p : R × R), (p.fst) * p.snd)
A smooth ring is a ring where the ring operations are smooth.
Instances
@[instance]
def
smooth_ring.to_smooth_semiring
{𝕜 : 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]
[t : smooth_ring I R] :
smooth_semiring I R
@[instance]
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_semiring I R] :
A smooth semiring is a topological semiring. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].
theorem
topological_ring_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)
[ring R]
[smooth_ring I R] :
A smooth ring is a topological ring. This is not an instance for technical reasons, see note [Design choices about smooth algebraic structures].