mathlib documentation

geometry.manifold.algebra.structures

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} [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

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] :
@[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] :
@[protected, instance]
def field_smooth_ring {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] :
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].