mathlibdocumentation

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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [has_add G] [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.has_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [has_mul G] [ G] [ G] :
has_mul I' N G )
Equations
@[simp]
theorem smooth_map.coe_add {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [has_add G] [ G] [ G] (f g : I' N G ) :
(f + g) = f + g
@[simp]
theorem smooth_map.coe_mul {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [has_mul G] [ G] [ G] (f g : I' N G ) :
(f * g) = f * g
@[simp]
theorem smooth_map.add_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {E'' : Type u_7} [ E''] {H'' : Type u_8} [topological_space H''] {I'' : E'' H''} {N' : Type u_9} [ N'] {G : Type u_10} [has_add G] [ G] [ G] (f g : I' N' G ) (h : I'' N N' ) :
(f + g).comp h = f.comp h + g.comp h
@[simp]
theorem smooth_map.mul_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {E'' : Type u_7} [ E''] {H'' : Type u_8} [topological_space H''] {I'' : E'' H''} {N' : Type u_9} [ N'] {G : Type u_10} [has_mul G] [ G] [ G] (f g : I' N' G ) (h : I'' N N' ) :
(f * g).comp h = f.comp h * g.comp h
@[protected, instance]
def smooth_map.has_one {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [monoid G] [ G] :
has_one I' N G )
Equations
@[protected, instance]
def smooth_map.has_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_monoid G] [ G] :
has_zero I' N G )
Equations
@[simp]
theorem smooth_map.coe_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_monoid G] [ G] :
0 = 0
@[simp]
theorem smooth_map.coe_one {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [monoid G] [ G] :
1 = 1

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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.semigroup {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [semigroup G] [ G] [ G] :
semigroup I' N G )
Equations
@[protected, instance]
def smooth_map.add_monoid {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_monoid G] [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.monoid {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [monoid G] [ G] [ G] :
monoid I' N G )
Equations
def smooth_map.coe_fn_monoid_hom {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [monoid G] [ G] [ G] :
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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_monoid G] [ G] [ G] :
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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [monoid G] [ G] [ G] (x : I' N G ) (ᾰ : N) :
@[simp]
theorem smooth_map.coe_fn_add_monoid_hom_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_monoid G] [ G] [ G] (x : I' N G ) (ᾰ : N) :
@[protected, instance]
def smooth_map.add_comm_monoid {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.comm_monoid {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [comm_monoid G] [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.add_group {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_group G] [ G] [ G] :
Equations
@[protected, instance]
def smooth_map.group {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [group G] [ G] [ G] :
group I' N G )
Equations
@[simp]
theorem smooth_map.coe_inv {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [group G] [ G] [ G] (f : I' N G ) :
@[simp]
theorem smooth_map.coe_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_group G] [ G] [ G] (f : I' N G ) :
@[simp]
theorem smooth_map.coe_div {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [group G] [ G] [ G] (f g : I' N G ) :
(f / g) = f / g
@[simp]
theorem smooth_map.coe_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [add_group G] [ G] [ G] (f g : I' N G ) :
(f - g) = f - g
@[protected, instance]
def smooth_map.comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [comm_group G] [ G] [ G] :
comm_group I' N G )
Equations
@[protected, instance]
def smooth_map.add_comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {G : Type u_7} [ G] [ 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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [semiring R] [ R] [ R] :
semiring I' N R )
Equations
@[protected, instance]
def smooth_map.ring {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [ring R] [ R] [ R] :
ring I' N R )
Equations
@[protected, instance]
def smooth_map.comm_ring {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [comm_ring R] [ R] [ R] :
comm_ring I' N R )
Equations
def smooth_map.coe_fn_ring_hom {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [comm_ring R] [ R] [ R] :
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} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [comm_ring R] [ R] [ R] (x : I' N R ) (ᾰ : N) :
def smooth_map.eval_ring_hom {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_4} {I : H} {H' : Type u_5} {I' : H'} {N : Type u_6} [ N] {R : Type u_7} [comm_ring R] [ R] [ R] (n : N) :
I' N R →+* R

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_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] :
N V )
Equations
@[simp]
theorem smooth_map.coe_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] (r : 𝕜) (f : N V ) :
(r f) = r f
@[simp]
theorem smooth_map.smul_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {E'' : Type u_7} [ E''] {H'' : Type u_8} [topological_space H''] {I'' : E'' H''} {N' : Type u_9} [ N'] {V : Type u_3} [ V] (r : 𝕜) (g : N' V ) (h : I'' N N' ) :
(r g).comp h = r g.comp h
@[protected, instance]
def smooth_map.module {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] :
N V )
Equations
def smooth_map.coe_fn_linear_map {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ 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} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] (x : 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} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {A : Type u_10} [normed_ring A] [ A] [ A] :
𝕜 →+* N A

Smooth constant functions as a ring_hom.

Equations
@[protected, instance]
def smooth_map.algebra {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {A : Type u_10} [normed_ring A] [ A] [ A] :
N A )
Equations
def smooth_map.coe_fn_alg_hom {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {A : Type u_10} [normed_ring A] [ A] [ 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} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {A : Type u_10} [normed_ring A] [ A] [ A] (x : N A ) (ᾰ : N) :
= x ᾰ

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_smul' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] :
has_smul N 𝕜 ) N V )
Equations
@[simp]
theorem smooth_map.smul_comp' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {E'' : Type u_7} [ E''] {H'' : Type u_8} [topological_space H''] {I'' : E'' H''} {N' : Type u_9} [ N'] {V : Type u_3} [ V] (f : N' 𝕜 ) (g : N' V ) (h : I'' N N' ) :
(f g).comp h = f.comp h g.comp h
@[protected, instance]
def smooth_map.module' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {N : Type u_6} [ N] {V : Type u_3} [ V] :
module N 𝕜 ) N V )
Equations