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]
Equations
@[protected, instance]
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]
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]
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]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
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

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

The add_subgroup of continuous maps α → β.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[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(α, β)) (ᾰ : α) :
@[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]
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]
Equations
@[protected, instance]
Equations
@[protected, instance]

Ring stucture #

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

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]
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]
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 continuous_map.coe_fn_ring_hom_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [semiring β] [topological_semiring β] (x : C(α, β)) (ᾰ : α) :

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.

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
@[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, norm_cast]
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]
Equations
@[protected]

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

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]
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₂] {α : 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₂] {α : Type u_1} [topological_space α] (g : A →ₐ[R] A₂) (hg : continuous g) (ᾰ : C(α, A)) :
@[simp]
theorem continuous_map.comp_right_alg_hom_apply (R : Type u_2) [comm_semiring R] (A : Type u_3) [topological_space A] [semiring A] [algebra R A] [topological_semiring A] {α : Type u_1} {β : Type u_4} [topological_space α] [topological_space β] (f : C(α, β)) (g : C(β, A)) :
def continuous_map.comp_right_alg_hom (R : Type u_2) [comm_semiring R] (A : Type u_3) [topological_space A] [semiring A] [algebra R A] [topological_semiring A] {α : Type u_1} {β : Type u_4} [topological_space α] [topological_space β] (f : C(α, β)) :
C(β, A) →ₐ[R] C(α, A)

Precomposition of functions into a normed ring by a continuous map is an algebra homomorphism.

Equations

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] (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] (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] (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

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]
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]
Equations
@[simp]
@[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]

The functorial map taking f : C(X, Y) to C(Y, A) →⋆ₐ[𝕜] C(X, A) given by pre-composition with the continuous function f. See continuous_map.comp_monoid_hom' and continuous_map.comp_add_monoid_hom', continuous_map.comp_right_alg_hom for bundlings of pre-composition into a monoid_hom, an add_monoid_hom and an alg_hom, respectively, under suitable assumptions on A.

Equations
@[simp]

continuous_map.comp_star_alg_hom' sends the identity continuous map to the identity star_alg_hom

continuous_map.comp_star_alg_hom is functorial.

def homeomorph.comp_star_alg_equiv' {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (𝕜 : Type u_3) [comm_semiring 𝕜] (A : Type u_4) [topological_space A] [semiring A] [topological_semiring A] [star_ring A] [has_continuous_star A] [algebra 𝕜 A] (f : X ≃ₜ Y) :

continuous_map.comp_star_alg_hom' as a star_alg_equiv when the continuous map f is actually a homeomorphism.

Equations