mathlib documentation

geometry.manifold.algebra.smooth_functions

Algebraic structures over smooth functions #

In this file, we define instances of algebraic structures over smooth functions.

@[instance]
def smooth_map.has_add {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [has_add G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] :
@[instance]
def smooth_map.has_mul {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [has_mul G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] :
Equations
@[simp]
theorem smooth_map.coe_add {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [has_add G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] (f g : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[simp]
theorem smooth_map.coe_mul {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [has_mul G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] (f g : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[instance]
def smooth_map.has_one {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [monoid G] [topological_space G] [charted_space H' G] :
Equations
@[instance]
def smooth_map.has_zero {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_monoid G] [topological_space G] [charted_space H' G] :
@[simp]
theorem smooth_map.coe_zero {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_monoid G] [topological_space G] [charted_space H' G] :
@[simp]
theorem smooth_map.coe_one {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [monoid G] [topological_space G] [charted_space H' G] :

Group structure #

In this section we show that smooth functions valued in a Lie group inherit a group structure under pointwise multiplication.

@[instance]
def smooth_map_add_semigroup {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_semigroup G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] :
@[instance]
def smooth_map_semigroup {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [semigroup G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] :
Equations
@[instance]
def smooth_map_monoid {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [monoid G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] :
Equations
@[instance]
def smooth_map_add_monoid {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_monoid G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] :
@[instance]
def smooth_map_comm_monoid {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [comm_monoid G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] :
Equations
@[instance]
def smooth_map_add_comm_monoid {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_comm_monoid G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] :
@[instance]
def smooth_map_group {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [group G] [topological_space G] [charted_space H' G] [lie_group I' G] :
Equations
@[instance]
def smooth_map_add_group {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_group G] [topological_space G] [charted_space H' G] [lie_add_group I' G] :
@[simp]
theorem smooth_map.coe_inv {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [group G] [topological_space G] [charted_space H' G] [lie_group I' G] (f : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[simp]
theorem smooth_map.coe_neg {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_group G] [topological_space G] [charted_space H' G] [lie_add_group I' G] (f : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[simp]
theorem smooth_map.coe_div {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [group G] [topological_space G] [charted_space H' G] [lie_group I' G] (f g : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[simp]
theorem smooth_map.coe_sub {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_group G] [topological_space G] [charted_space H' G] [lie_add_group I' G] (f g : C^โŠคโŸฎI, N; I', GโŸฏ) :
@[instance]
def smooth_map_add_comm_group {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [add_comm_group G] [topological_space G] [charted_space H' G] [lie_add_group I' G] :
@[instance]
def smooth_map_comm_group {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {G : Type u_7} [comm_group G] [topological_space G] [charted_space H' G] [lie_group I' G] :
Equations

Ring stucture #

In this section we show that smooth functions valued in a smooth ring R inherit a ring structure under pointwise multiplication.

@[instance]
def smooth_map_semiring {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {E' : Type u_3} [normed_group E'] [normed_space ๐•œ E'] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {H' : Type u_5} [topological_space H'] {I' : model_with_corners ๐•œ E' H'} {N : Type u_6} [topological_space N] [charted_space H N] {R : Type u_7} [semiring R] [topological_space R] [charted_space H' R] [smooth_semiring I' R] :
Equations

Semiodule stucture #

In this section we show that smooth functions valued in a vector space M over a normed field ๐•œ inherit a vector space structure.

@[instance]
def smooth_map_has_scalar {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :
Equations
@[simp]
theorem smooth_map.coe_smul {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] (r : ๐•œ) (f : C^โŠคโŸฎI, N; ๐“˜(๐•œ, V), VโŸฏ) :
@[instance]
def smooth_map_module {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :
Equations

Algebra structure #

In this section we show that smooth functions valued in a normed algebra A over a normed field ๐•œ inherit an algebra structure.

def smooth_map.C {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {A : Type u_7} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] :

Smooth constant functions as a ring_hom.

Equations
@[instance]
def times_cont_mdiff_map.algebra {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {A : Type u_7} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] :
Equations

Structure as module over scalar functions #

If V is a module over ๐•œ, then we show that the space of smooth functions from N to V is naturally a vector space over the ring of smooth functions from N to ๐•œ.

@[instance]
def smooth_map_has_scalar' {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :
Equations
@[instance]
def smooth_map_module' {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] {H : Type u_4} [topological_space H] {I : model_with_corners ๐•œ E H} {N : Type u_6} [topological_space N] [charted_space H N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :
Equations