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.

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] :
𝕜 →+* C^I, N; 𝓘(𝕜, 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