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] :
Equations
@[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โŸฏ) :
@[simp]
theorem smooth_map.add_comp {๐•œ : 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] {E'' : Type u_7} [normed_group E''] [normed_space ๐•œ E''] {H'' : Type u_8} [topological_space H''] {I'' : model_with_corners ๐•œ E'' H''} {N' : Type u_9} [topological_space N'] [charted_space H'' N'] {G : Type u_10} [has_add G] [topological_space G] [charted_space H' G] [has_smooth_add I' G] (f g : C^โŠคโŸฎI'', N'; I', GโŸฏ) (h : C^โŠคโŸฎI, N; I'', N'โŸฏ) :
(f + g).comp h = f.comp h + g.comp h
@[simp]
theorem smooth_map.mul_comp {๐•œ : 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] {E'' : Type u_7} [normed_group E''] [normed_space ๐•œ E''] {H'' : Type u_8} [topological_space H''] {I'' : model_with_corners ๐•œ E'' H''} {N' : Type u_9} [topological_space N'] [charted_space H'' N'] {G : Type u_10} [has_mul G] [topological_space G] [charted_space H' G] [has_smooth_mul I' G] (f g : C^โŠคโŸฎI'', N'; I', GโŸฏ) (h : C^โŠคโŸฎI, N; I'', N'โŸฏ) :
(f * g).comp h = (f.comp h) * g.comp h
@[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] :
Equations
@[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] :
Equations
@[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.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] :
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
def smooth_map.coe_fn_monoid_hom {๐•œ : 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] :

Coercion to a function as an monoid_hom. Similar to monoid_hom.coe_fn.

Equations
def smooth_map.coe_fn_add_monoid_hom {๐•œ : 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] :

Coercion to a function as an add_monoid_hom. Similar to add_monoid_hom.coe_fn.

Equations
@[simp]
theorem smooth_map.coe_fn_monoid_hom_apply {๐•œ : 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] (x : C^โŠคโŸฎI, N; I', GโŸฏ) (แพฐ : N) :
@[simp]
theorem smooth_map.coe_fn_add_monoid_hom_apply {๐•œ : 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] (x : C^โŠคโŸฎI, N; I', GโŸฏ) (แพฐ : N) :
@[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] :
Equations
@[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_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] :
Equations
@[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
@[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.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_ring I' R] :
Equations
def smooth_map.coe_fn_ring_hom {๐•œ : 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} [comm_ring R] [topological_space R] [charted_space H' R] [smooth_ring I' R] :

Coercion to a function as a ring_hom.

Equations
@[simp]
theorem smooth_map.coe_fn_ring_hom_apply {๐•œ : 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} [comm_ring R] [topological_space R] [charted_space H' R] [smooth_ring I' R] (x : C^โŠคโŸฎI, N; I', RโŸฏ) (แพฐ : N) :
def smooth_map.eval_ring_hom {๐•œ : 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} [comm_ring R] [topological_space R] [charted_space H' R] [smooth_ring I' R] (n : N) :

function.eval as a ring_hom on the ring of smooth functions.

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โŸฏ) :
@[simp]
theorem smooth_map.smul_comp {๐•œ : 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] {E'' : Type u_7} [normed_group E''] [normed_space ๐•œ E''] {H'' : Type u_8} [topological_space H''] {I'' : model_with_corners ๐•œ E'' H''} {N' : Type u_9} [topological_space N'] [charted_space H'' N'] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] (r : ๐•œ) (g : C^โŠคโŸฎI'', N'; ๐“˜(๐•œ, V), VโŸฏ) (h : C^โŠคโŸฎI, N; I'', N'โŸฏ) :
(r โ€ข g).comp h = r โ€ข g.comp h
@[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
def smooth_map.coe_fn_linear_map {๐•œ : 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] :
C^โŠคโŸฎI, N; ๐“˜(๐•œ, V), VโŸฏ โ†’โ‚—[๐•œ] N โ†’ V

Coercion to a function as a linear_map.

Equations
@[simp]
theorem smooth_map.coe_fn_linear_map_apply {๐•œ : 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] (x : C^โŠคโŸฎI, N; ๐“˜(๐•œ, V), VโŸฏ) (แพฐ : N) :

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_10} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] :

Smooth constant functions as a ring_hom.

Equations
@[instance]
def smooth_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_10} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] :
Equations
def smooth_map.coe_fn_alg_hom {๐•œ : 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_10} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] :
C^โŠคโŸฎI, N; ๐“˜(๐•œ, A), AโŸฏ โ†’โ‚[๐•œ] N โ†’ A

Coercion to a function as an alg_hom.

Equations
@[simp]
theorem smooth_map.coe_fn_alg_hom_apply {๐•œ : 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_10} [normed_ring A] [normed_algebra ๐•œ A] [smooth_ring ๐“˜(๐•œ, A) A] (x : C^โŠคโŸฎI, N; ๐“˜(๐•œ, A), AโŸฏ) (แพฐ : N) :

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
@[simp]
theorem smooth_map.smul_comp' {๐•œ : 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] {E'' : Type u_7} [normed_group E''] [normed_space ๐•œ E''] {H'' : Type u_8} [topological_space H''] {I'' : model_with_corners ๐•œ E'' H''} {N' : Type u_9} [topological_space N'] [charted_space H'' N'] {V : Type u_3} [normed_group V] [normed_space ๐•œ V] (f : C^โŠคโŸฎI'', N'; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ) (g : C^โŠคโŸฎI'', N'; ๐“˜(๐•œ, V), VโŸฏ) (h : C^โŠคโŸฎI, N; I'', N'โŸฏ) :
(f โ€ข g).comp h = f.comp h โ€ข g.comp h
@[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