mathlib documentation

topology.continuous_function.algebra

Algebraic structures over continuous functions #

In this file we define instances of algebraic structures over the type continuous_map α β (denoted C(α, β)) of bundled continuous maps from α to β. For example, C(α, β) is a group when β is a group, a ring when β is a ring, etc.

For each type of algebraic structure, we also define an appropriate subobject of α → β with carrier { f : α → β | continuous f }. For example, when β is a group, a subgroup continuous_subgroup α β of α → β is constructed with carrier { f : α → β | continuous f }.

Note that, rather than using the derived algebraic structures on these subobjects (for example, when β is a group, the derived group structure on continuous_subgroup α β), one should use C(α, β) with the appropriate instance of the structure.

@[protected, instance]
def continuous_functions.set_of.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
has_coe_to_fun {f : α → β | continuous f} (λ (_x : {f : α → β | continuous f}), α → β)
Equations
@[protected, instance]
def continuous_map.has_mul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] :
Equations
@[protected, instance]
def continuous_map.has_add {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_mul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] (f g : C(α, β)) :
(f * g) = f * g
@[simp, norm_cast]
theorem continuous_map.coe_add {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] (f g : C(α, β)) :
(f + g) = f + g
@[simp]
theorem continuous_map.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_mul γ] [has_continuous_mul γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ * f₂).comp g = f₁.comp g * f₂.comp g
@[simp]
theorem continuous_map.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_add γ] [has_continuous_add γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
@[protected, instance]
def continuous_map.has_zero {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
Equations
@[protected, instance]
def continuous_map.has_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
1 = 1
@[simp, norm_cast]
theorem continuous_map.coe_zero {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
0 = 0
@[simp]
theorem continuous_map.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_one γ] (g : C(α, β)) :
1.comp g = 1
@[simp]
theorem continuous_map.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_zero γ] (g : C(α, β)) :
0.comp g = 0
@[protected, instance]
def continuous_map.has_nat_cast {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_nat_cast β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_nat_cast {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_nat_cast β] (n : ) :
@[protected, instance]
def continuous_map.has_int_cast {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_int_cast β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_int_cast {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_int_cast β] (n : ) :
@[protected, instance]
def continuous_map.has_nsmul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
Equations
@[protected, instance]
def continuous_map.has_pow {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_pow {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ) :
(f ^ n) = f ^ n
@[norm_cast]
theorem continuous_map.coe_nsmul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] (f : C(α, β)) (n : ) :
(n f) = n f
@[simp]
theorem continuous_map.pow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [monoid γ] [has_continuous_mul γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(f ^ n).comp g = f.comp g ^ n
theorem continuous_map.nsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_monoid γ] [has_continuous_add γ] (f : C(β, γ)) (n : ) (g : C(α, β)) :
(n f).comp g = n f.comp g
@[protected, instance]
def continuous_map.has_neg {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
Equations
@[protected, instance]
def continuous_map.has_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_neg {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] (f : C(α, β)) :
@[simp, norm_cast]
theorem continuous_map.coe_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_group γ] [topological_add_group γ] (f : C(β, γ)) (g : C(α, β)) :
(-f).comp g = -f.comp g
@[simp]
theorem continuous_map.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [group γ] [topological_group γ] (f : C(β, γ)) (g : C(α, β)) :
@[protected, instance]
def continuous_map.has_div {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_div β] [has_continuous_div β] :
Equations
@[protected, instance]
def continuous_map.has_sub {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_sub β] [has_continuous_sub β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_div {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_div β] [has_continuous_div β] (f g : C(α, β)) :
(f / g) = f / g
@[simp, norm_cast]
theorem continuous_map.coe_sub {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_sub β] [has_continuous_sub β] (f g : C(α, β)) :
(f - g) = f - g
@[simp]
theorem continuous_map.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_sub γ] [has_continuous_sub γ] (f g : C(β, γ)) (h : C(α, β)) :
(f - g).comp h = f.comp h - g.comp h
@[simp]
theorem continuous_map.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [has_div γ] [has_continuous_div γ] (f g : C(β, γ)) (h : C(α, β)) :
(f / g).comp h = f.comp h / g.comp h
@[protected, instance]
def continuous_map.has_zsmul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
Equations
@[protected, instance]
def continuous_map.has_zpow {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
Equations
@[simp, norm_cast]
theorem continuous_map.coe_zpow {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f : C(α, β)) (z : ) :
(f ^ z) = f ^ z
@[norm_cast]
theorem continuous_map.coe_zsmul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] (f : C(α, β)) (z : ) :
(z f) = z f
theorem continuous_map.zsmul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_group γ] [topological_add_group γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(z f).comp g = z f.comp g
@[simp]
theorem continuous_map.zpow_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [group γ] [topological_group γ] (f : C(β, γ)) (z : ) (g : C(α, β)) :
(f ^ z).comp g = f.comp g ^ z

Group stucture #

In this section we show that continuous functions valued in a topological group inherit the structure of a group.

def continuous_submonoid (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
submonoid (α → β)

The submonoid of continuous maps α → β.

Equations
def continuous_add_submonoid (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
add_submonoid (α → β)

The add_submonoid of continuous maps α → β.

Equations
def continuous_subgroup (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [group β] [topological_group β] :
subgroup (α → β)

The subgroup of continuous maps α → β.

Equations
def continuous_add_subgroup (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
add_subgroup (α → β)

The add_subgroup of continuous maps α → β.

Equations
@[protected, instance]
Equations
@[protected, instance]
def continuous_map.semigroup {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [semigroup β] [has_continuous_mul β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def continuous_map.add_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
Equations
@[protected, instance]
def continuous_map.monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def continuous_map.comm_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_monoid β] [has_continuous_mul β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
theorem continuous_map.coe_fn_monoid_hom_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] (x : C(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_monoid_hom {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
C(α, β) →* α → β

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

Equations
@[simp]
theorem continuous_map.coe_fn_add_monoid_hom_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] (x : C(α, β)) (ᾰ : α) :
@[simp]
theorem add_monoid_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] [topological_space γ] [add_monoid γ] [has_continuous_add γ] (g : β →+ γ) (hg : continuous g) (f : C(α, β)) :
@[protected]
def add_monoid_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] [topological_space γ] [add_monoid γ] [has_continuous_add γ] (g : β →+ γ) (hg : continuous g) :
C(α, β) →+ C(α, γ)

Composition on the left by a (continuous) homomorphism of topological add_monoids, as an add_monoid_hom. Similar to add_monoid_hom.comp_left.

Equations
@[protected]
def monoid_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] [topological_space γ] [monoid γ] [has_continuous_mul γ] (g : β →* γ) (hg : continuous g) :
C(α, β) →* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological monoids, as a monoid_hom. Similar to monoid_hom.comp_left.

Equations
@[simp]
theorem monoid_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] [topological_space γ] [monoid γ] [has_continuous_mul γ] (g : β →* γ) (hg : continuous g) (f : C(α, β)) :
def continuous_map.comp_monoid_hom' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [mul_one_class γ] [has_continuous_mul γ] (g : C(α, β)) :
C(β, γ) →* C(α, γ)

Composition on the right as a monoid_hom. Similar to monoid_hom.comp_hom'.

Equations
@[simp]
theorem continuous_map.comp_monoid_hom'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [mul_one_class γ] [has_continuous_mul γ] (g : C(α, β)) (f : C(β, γ)) :
def continuous_map.comp_add_monoid_hom' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_zero_class γ] [has_continuous_add γ] (g : C(α, β)) :
C(β, γ) →+ C(α, γ)

Composition on the right as an add_monoid_hom. Similar to add_monoid_hom.comp_hom'.

Equations
@[simp]
theorem continuous_map.comp_add_monoid_hom'_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_zero_class γ] [has_continuous_add γ] (g : C(α, β)) (f : C(β, γ)) :
@[simp]
theorem continuous_map.coe_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [topological_space α] [topological_space β] [has_continuous_add β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp]
theorem continuous_map.coe_prod {α : Type u_1} {β : Type u_2} [comm_monoid β] [topological_space α] [topological_space β] [has_continuous_mul β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem continuous_map.sum_apply {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [topological_space α] [topological_space β] [has_continuous_add β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) (a : α) :
(s.sum (λ (i : ι), f i)) a = s.sum (λ (i : ι), (f i) a)
theorem continuous_map.prod_apply {α : Type u_1} {β : Type u_2} [comm_monoid β] [topological_space α] [topological_space β] [has_continuous_mul β] {ι : Type u_3} (s : finset ι) (f : ι → C(α, β)) (a : α) :
(s.prod (λ (i : ι), f i)) a = s.prod (λ (i : ι), (f i) a)
@[protected, instance]
def continuous_map.add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
Equations
@[protected, instance]
def continuous_map.group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
group C(α, β)
Equations
@[protected, instance]
def continuous_map.comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_group β] [topological_group β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

Ring stucture #

In this section we show that continuous functions valued in a topological semiring R inherit the structure of a ring.

def continuous_subsemiring (α : Type u_1) (R : Type u_2) [topological_space α] [topological_space R] [semiring R] [topological_semiring R] :
subsemiring (α → R)

The subsemiring of continuous maps α → β.

Equations
def continuous_subring (α : Type u_1) (R : Type u_2) [topological_space α] [topological_space R] [ring R] [topological_ring R] :
subring (α → R)

The subring of continuous maps α → β.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def continuous_map.semiring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [semiring β] [topological_semiring β] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
  • continuous_map.non_assoc_ring = function.injective.non_assoc_ring coe_fn continuous_map.coe_injective continuous_map.non_assoc_ring._proof_7 continuous_map.non_assoc_ring._proof_8 continuous_map.non_assoc_ring._proof_9 continuous_map.non_assoc_ring._proof_10 continuous_map.non_assoc_ring._proof_11 continuous_map.non_assoc_ring._proof_12 continuous_map.non_assoc_ring._proof_13 continuous_map.non_assoc_ring._proof_14 continuous_map.non_assoc_ring._proof_15 continuous_map.non_assoc_ring._proof_16
@[protected, instance]
def continuous_map.ring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [ring β] [topological_ring β] :
ring C(α, β)
Equations
  • continuous_map.ring = function.injective.ring coe_fn continuous_map.coe_injective continuous_map.ring._proof_8 continuous_map.ring._proof_9 continuous_map.ring._proof_10 continuous_map.ring._proof_11 continuous_map.ring._proof_12 continuous_map.ring._proof_13 continuous_map.ring._proof_14 continuous_map.ring._proof_15 continuous_map.ring._proof_16 continuous_map.ring._proof_17 continuous_map.ring._proof_18
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def continuous_map.comm_ring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_ring β] [topological_ring β] :
Equations
  • continuous_map.comm_ring = function.injective.comm_ring coe_fn continuous_map.coe_injective continuous_map.comm_ring._proof_8 continuous_map.comm_ring._proof_9 continuous_map.comm_ring._proof_10 continuous_map.comm_ring._proof_11 continuous_map.comm_ring._proof_12 continuous_map.comm_ring._proof_13 continuous_map.comm_ring._proof_14 continuous_map.comm_ring._proof_15 continuous_map.comm_ring._proof_16 continuous_map.comm_ring._proof_17 continuous_map.comm_ring._proof_18
@[protected]
def ring_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [semiring β] [topological_semiring β] [topological_space γ] [semiring γ] [topological_semiring γ] (g : β →+* γ) (hg : continuous g) :
C(α, β) →+* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological semirings, as a ring_hom. Similar to ring_hom.comp_left.

Equations
@[simp]
theorem ring_hom.comp_left_continuous_apply (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [semiring β] [topological_semiring β] [topological_space γ] [semiring γ] [topological_semiring γ] (g : β →+* γ) (hg : continuous g) (ᾰ : C(α, β)) :
@[simp]
theorem continuous_map.coe_fn_ring_hom_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [ring β] [topological_ring β] (x : C(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_ring_hom {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [ring β] [topological_ring β] :
C(α, β) →+* α → β

Coercion to a function as a ring_hom.

Equations

Semiodule stucture #

In this section we show that continuous functions valued in a topological module M over a topological semiring R inherit the structure of a module.

def continuous_submodule (α : Type u_1) [topological_space α] (R : Type u_2) [semiring R] (M : Type u_3) [topological_space M] [add_comm_group M] [module R M] [has_continuous_const_smul R M] [topological_add_group M] :
submodule R (α → M)

The R-submodule of continuous maps α → M.

Equations
@[protected, instance]
def continuous_map.has_smul {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] :
Equations
@[protected, instance]
def continuous_map.has_vadd {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_vadd R M] [has_continuous_const_vadd R M] :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]
theorem continuous_map.coe_smul {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] (c : R) (f : C(α, M)) :
(c f) = c f
@[simp]
theorem continuous_map.coe_vadd {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_vadd R M] [has_continuous_const_vadd R M] (c : R) (f : C(α, M)) :
(c +ᵥ f) = c +ᵥ f
theorem continuous_map.vadd_apply {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_vadd R M] [has_continuous_const_vadd R M] (c : R) (f : C(α, M)) (a : α) :
(c +ᵥ f) a = c +ᵥ f a
theorem continuous_map.smul_apply {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] (c : R) (f : C(α, M)) (a : α) :
(c f) a = c f a
@[simp]
theorem continuous_map.smul_comp {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {R : Type u_3} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r f).comp g = r f.comp g
@[simp]
theorem continuous_map.vadd_comp {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {R : Type u_3} {M : Type u_5} [topological_space M] [has_vadd R M] [has_continuous_const_vadd R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r +ᵥ f).comp g = r +ᵥ f.comp g
@[protected, instance]
def continuous_map.vadd_comm_class {α : Type u_1} [topological_space α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [topological_space M] [has_vadd R M] [has_continuous_const_vadd R M] [has_vadd R₁ M] [has_continuous_const_vadd R₁ M] [vadd_comm_class R R₁ M] :
@[protected, instance]
def continuous_map.smul_comm_class {α : Type u_1} [topological_space α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] [has_smul R₁ M] [has_continuous_const_smul R₁ M] [smul_comm_class R R₁ M] :
@[protected, instance]
def continuous_map.is_scalar_tower {α : Type u_1} [topological_space α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [topological_space M] [has_smul R M] [has_continuous_const_smul R M] [has_smul R₁ M] [has_continuous_const_smul R₁ M] [has_smul R R₁] [is_scalar_tower R R₁ M] :
@[protected, instance]
@[protected, instance]
def continuous_map.mul_action {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [monoid R] [mul_action R M] [has_continuous_const_smul R M] :
Equations
@[protected, instance]
def continuous_map.module {α : Type u_1} [topological_space α] {R : Type u_3} {M : Type u_5} [topological_space M] [semiring R] [add_comm_monoid M] [has_continuous_add M] [module R M] [has_continuous_const_smul R M] :
module R C(α, M)
Equations
@[protected]
def continuous_linear_map.comp_left_continuous (R : Type u_3) {M : Type u_5} [topological_space M] {M₂ : Type u_6} [topological_space M₂] [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [has_continuous_add M] [module R M] [has_continuous_const_smul R M] [has_continuous_add M₂] [module R M₂] [has_continuous_const_smul R M₂] (α : Type u_1) [topological_space α] (g : M →L[R] M₂) :
C(α, M) →ₗ[R] C(α, M₂)

Composition on the left by a continuous linear map, as a linear_map. Similar to linear_map.comp_left.

Equations
@[simp]
theorem continuous_map.coe_fn_linear_map_apply {α : Type u_1} [topological_space α] (R : Type u_3) {M : Type u_5} [topological_space M] [semiring R] [add_comm_monoid M] [has_continuous_add M] [module R M] [has_continuous_const_smul R M] (x : C(α, M)) (ᾰ : α) :
def continuous_map.coe_fn_linear_map {α : Type u_1} [topological_space α] (R : Type u_3) {M : Type u_5} [topological_space M] [semiring R] [add_comm_monoid M] [has_continuous_add M] [module R M] [has_continuous_const_smul R M] :
C(α, M) →ₗ[R] α → M

Coercion to a function as a linear_map.

Equations

Algebra structure #

In this section we show that continuous functions valued in a topological algebra A over a ring R inherit the structure of an algebra. Note that the hypothesis that A is a topological algebra is obtained by requiring that A be both a has_continuous_smul and a topological_semiring.

def continuous_subalgebra {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] :
subalgebra R (α → A)

The R-subalgebra of continuous maps α → A.

Equations
def continuous_map.C {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] :
R →+* C(α, A)

Continuous constant functions as a ring_hom.

Equations
@[simp]
theorem continuous_map.C_apply {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (r : R) (a : α) :
@[protected, instance]
def continuous_map.algebra {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [has_continuous_const_smul R A] :
Equations
@[protected]
def alg_hom.comp_left_continuous (R : Type u_2) [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] {A₂ : Type u_4} [topological_space A₂] [semiring A₂] [algebra R A₂] [topological_semiring A₂] [has_continuous_const_smul R A] [has_continuous_const_smul R A₂] {α : Type u_1} [topological_space α] (g : A →ₐ[R] A₂) (hg : continuous g) :
C(α, A) →ₐ[R] C(α, A₂)

Composition on the left by a (continuous) homomorphism of topological R-algebras, as an alg_hom. Similar to alg_hom.comp_left.

Equations
@[simp]
theorem alg_hom.comp_left_continuous_apply (R : Type u_2) [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] {A₂ : Type u_4} [topological_space A₂] [semiring A₂] [algebra R A₂] [topological_semiring A₂] [has_continuous_const_smul R A] [has_continuous_const_smul R A₂] {α : Type u_1} [topological_space α] (g : A →ₐ[R] A₂) (hg : continuous g) (ᾰ : C(α, A)) :
def continuous_map.coe_fn_alg_hom {α : Type u_1} [topological_space α] (R : Type u_2) [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [has_continuous_const_smul R A] :
C(α, A) →ₐ[R] α → A

Coercion to a function as an alg_hom.

Equations
@[simp]
theorem continuous_map.coe_fn_alg_hom_apply {α : Type u_1} [topological_space α] (R : Type u_2) [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [has_continuous_const_smul R A] (x : C(α, A)) (ᾰ : α) :
@[reducible]
def subalgebra.separates_points {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [has_continuous_const_smul R A] (s : subalgebra R C(α, A)) :
Prop

A version of separates_points for subalgebras of the continuous functions, used for stating the Stone-Weierstrass theorem.

@[simp]
theorem algebra_map_apply {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [has_continuous_const_smul R A] (k : R) (a : α) :
((algebra_map R C(α, A)) k) a = k 1
def set.separates_points_strongly {α : Type u_1} [topological_space α] {𝕜 : Type u_5} [topological_space 𝕜] (s : set C(α, 𝕜)) :
Prop

A set of continuous maps "separates points strongly" if for each pair of distinct points there is a function with specified values on them.

We give a slightly unusual formulation, where the specified values are given by some function v, and we ask f x = v x ∧ f y = v y. This avoids needing a hypothesis x ≠ y.

In fact, this definition would work perfectly well for a set of non-continuous functions, but as the only current use case is in the Stone-Weierstrass theorem, writing it this way avoids having to deal with casts inside the set. (This may need to change if we do Stone-Weierstrass on non-compact spaces, where the functions would be continuous functions vanishing at infinity.)

Equations
theorem subalgebra.separates_points.strongly {α : Type u_1} [topological_space α] {𝕜 : Type u_5} [topological_space 𝕜] [field 𝕜] [topological_ring 𝕜] {s : subalgebra 𝕜 C(α, 𝕜)} (h : s.separates_points) :

Working in continuous functions into a topological field, a subalgebra of functions that separates points also separates points strongly.

By the hypothesis, we can find a function f so f x ≠ f y. By an affine transformation in the field we can arrange so that f x = a and f x = b.

Structure as module over scalar functions #

If M is a module over R, then we show that the space of continuous functions from α to M is naturally a module over the ring of continuous functions from α to R.

@[protected, instance]
def continuous_map.has_smul' {α : Type u_1} [topological_space α] {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [module R M] [has_continuous_smul R M] :
Equations

We now provide formulas for f ⊓ g and f ⊔ g, where f g : C(α, β), in terms of continuous_map.abs.

theorem min_eq_half_add_sub_abs_sub {R : Type u_1} [linear_ordered_field R] {x y : R} :
linear_order.min x y = 2⁻¹ * (x + y - |x - y|)
theorem max_eq_half_add_add_abs_sub {R : Type u_1} [linear_ordered_field R] {x y : R} :
linear_order.max x y = 2⁻¹ * (x + y + |x - y|)
theorem continuous_map.inf_eq {α : Type u_1} [topological_space α] {β : Type u_2} [linear_ordered_field β] [topological_space β] [order_topology β] [topological_ring β] (f g : C(α, β)) :
f g = 2⁻¹ (f + g - |f - g|)
theorem continuous_map.sup_eq {α : Type u_1} [topological_space α] {β : Type u_2} [linear_ordered_field β] [topological_space β] [order_topology β] [topological_ring β] (f g : C(α, β)) :
f g = 2⁻¹ (f + g + |f - g|)

Star structure #

If β has a continuous star operation, we put a star structure on C(α, β) by using the star operation pointwise.

If β is a ⋆-ring, then C(α, β) inherits a ⋆-ring structure.

If β is a ⋆-ring and a ⋆-module over R, then the space of continuous functions from α to β is a ⋆-module over R.

@[protected, instance]
def continuous_map.has_star {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [has_star β] [has_continuous_star β] :
Equations
@[simp]
theorem continuous_map.coe_star {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [has_star β] [has_continuous_star β] (f : C(α, β)) :
@[simp]
theorem continuous_map.star_apply {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [has_star β] [has_continuous_star β] (f : C(α, β)) (x : α) :
@[protected, instance]
def continuous_map.star_module {R : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [topological_space β] [has_star R] [has_star β] [has_smul R β] [star_module R β] [has_continuous_star β] [has_continuous_const_smul R β] :