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] [smooth_manifold_with_corners I N] {G : Type u_7} [has_add G] [topological_space G] [has_continuous_add 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] [smooth_manifold_with_corners I N] {G : Type u_7} [has_mul G] [topological_space G] [has_continuous_mul G] [charted_space H' G] [has_smooth_mul I' G] :

Equations
@[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] [smooth_manifold_with_corners I N] {G : Type u_7} [monoid G] [topological_space G] [charted_space H' G] [smooth_manifold_with_corners I' 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_monoid G] [topological_space G] [charted_space H' G] [smooth_manifold_with_corners I' 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_semigroup G] [topological_space G] [has_continuous_add 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] [smooth_manifold_with_corners I N] {G : Type u_7} [semigroup G] [topological_space G] [has_continuous_mul 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] [smooth_manifold_with_corners I N] {G : Type u_7} [monoid G] [topological_space G] [has_continuous_mul 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_monoid G] [topological_space G] [has_continuous_add 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] [smooth_manifold_with_corners I N] {G : Type u_7} [comm_monoid G] [topological_space G] [has_continuous_mul 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_comm_monoid G] [topological_space G] [has_continuous_add 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] [smooth_manifold_with_corners I N] {G : Type u_7} [group G] [topological_space G] [topological_group G] [charted_space H' G] [smooth_manifold_with_corners I' 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_group G] [topological_space G] [topological_add_group G] [charted_space H' G] [smooth_manifold_with_corners I' G] [lie_add_group 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] [smooth_manifold_with_corners I N] {G : Type u_7} [add_comm_group G] [topological_space G] [topological_add_group 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] [smooth_manifold_with_corners I N] {G : Type u_7} [comm_group G] [topological_space G] [topological_group 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] [smooth_manifold_with_corners I N] {R : Type u_7} [semiring R] [topological_space R] [topological_semiring R] [charted_space H' R] [smooth_semiring I' R] :

Equations
@[instance]
def smooth_map_ring {๐•œ : 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] [smooth_manifold_with_corners I N] {R : Type u_7} [ring R] [topological_space R] [topological_ring R] [charted_space H' R] [smooth_ring I' R] :

Equations
@[instance]
def smooth_map_comm_ring {๐•œ : 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] [smooth_manifold_with_corners I N] {R : Type u_7} [comm_ring R] [topological_space R] [topological_ring R] [charted_space H' R] [smooth_ring 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] [smooth_manifold_with_corners I N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :

Equations
@[instance]
def smooth_map_semimodule {๐•œ : 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] [smooth_manifold_with_corners I 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] [smooth_manifold_with_corners I 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] [smooth_manifold_with_corners I 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] [smooth_manifold_with_corners I 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] [smooth_manifold_with_corners I N] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] :

Equations