mathlib documentation

geometry.manifold.algebra.smooth_functions

Algebraic structures over smooth functions #

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

@[protected, 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
@[protected, 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I'' I' N' G ⊀) (h : cont_mdiff_map I I'' N 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 : cont_mdiff_map I'' I' N' G ⊀) (h : cont_mdiff_map I I'' N N' ⊀) :
(f * g).comp h = f.comp h * g.comp h
@[protected, 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
@[protected, 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.

@[protected, 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
@[protected, 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
@[protected, 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
@[protected, 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] :
cont_mdiff_map I I' N G ⊀ β†’* N β†’ 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] :
cont_mdiff_map I I' N G ⊀ β†’+ N β†’ 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N G ⊀) (αΎ° : N) :
@[protected, 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
@[protected, 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
@[protected, 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
@[protected, 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N 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 : cont_mdiff_map I I' N G ⊀) :
@[protected, 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.

@[protected, 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] :
cont_mdiff_map I I' N R ⊀ β†’+* N β†’ 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 : cont_mdiff_map I I' N 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.

@[protected, 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 : cont_mdiff_map I (model_with_corners_self π•œ V) N 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 : cont_mdiff_map I'' (model_with_corners_self π•œ V) N' V ⊀) (h : cont_mdiff_map I I'' N N' ⊀) :
(r β€’ g).comp h = r β€’ g.comp h
@[protected, 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] :
cont_mdiff_map I (model_with_corners_self π•œ V) N 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 : cont_mdiff_map I (model_with_corners_self π•œ V) N 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 (model_with_corners_self π•œ A) A] :

Smooth constant functions as a ring_hom.

Equations
@[protected, 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 (model_with_corners_self π•œ 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 (model_with_corners_self π•œ A) A] :
cont_mdiff_map I (model_with_corners_self π•œ A) N 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 (model_with_corners_self π•œ A) A] (x : cont_mdiff_map I (model_with_corners_self π•œ A) N 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 π•œ.

@[protected, 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 : cont_mdiff_map I'' (model_with_corners_self π•œ π•œ) N' π•œ ⊀) (g : cont_mdiff_map I'' (model_with_corners_self π•œ V) N' V ⊀) (h : cont_mdiff_map I I'' N N' ⊀) :
(f β€’ g).comp h = f.comp h β€’ g.comp h
@[protected, 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