mathlib documentation

topology.continuous_function.algebra

Algebraic structures over continuous functions #

In this file we define instances of algebraic structures over continuous functions. Instances are present both in the case of the subtype of continuous functions and the type of continuous bundled functions. Both implementations have advantages and disadvantages, but many experienced people in Zulip have expressed a preference towards continuous bundled maps, so when there is no particular reason to use the subtype, continuous bundled functions should be used for the sake of uniformity.

@[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}
Equations
@[instance]
def continuous_map.has_mul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] :
Equations
@[instance]
def continuous_map.has_add {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] :
@[simp]
theorem continuous_map.mul_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] (f g : C(α, β)) :
f * g = (f) * g
@[simp]
theorem continuous_map.add_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] (f g : C(α, β)) :
(f + g) = f + g
@[instance]
def continuous_map.has_zero {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
@[instance]
def continuous_map.has_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
Equations
@[simp]
theorem continuous_map.one_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
1 = 1
@[simp]
theorem continuous_map.zero_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
0 = 0
@[simp]
theorem continuous_map.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [semigroup γ] [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 γ] [add_semigroup γ] [has_continuous_add γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
@[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

Group stucture #

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

@[instance]
def continuous_submonoid (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
is_submonoid {f : α → β | continuous f}
@[instance]
def continuous_add_submonoid (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
is_add_submonoid {f : α → β | continuous f}
@[instance]
def continuous_subgroup (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [group β] [topological_group β] :
is_subgroup {f : α → β | continuous f}
@[instance]
def continuous_add_subgroup (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
is_add_subgroup {f : α → β | continuous f}
@[instance]
def continuous_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
monoid {f : α → β | continuous f}
Equations
@[instance]
def continuous_add_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
add_monoid {f : α → β | continuous f}
@[instance]
def continuous_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
group {f : α → β | continuous f}
Equations
@[instance]
def continuous_add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
add_group {f : α → β | continuous f}
@[instance]
def continuous_add_comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_comm_group β] [topological_add_group β] :
add_comm_group {f : α → β | continuous f}
@[instance]
def continuous_comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_group β] [topological_group β] :
comm_group {f : α → β | continuous f}
Equations
@[instance]
@[instance]
def continuous_map.add_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
@[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(α, β)) (ᾰ : α) :
def continuous_map.coe_fn_add_monoid_hom {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
C(α, β) →+ α → β

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

def continuous_map.comp_monoid_hom' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [monoid γ] [has_continuous_mul γ] (g : C(α, β)) :
C(β, γ) →* C(α, γ)

Composition on the right as an 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 γ] [monoid γ] [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_monoid γ] [has_continuous_add γ] (g : C(α, β)) :
C(β, γ) →+ C(α, γ)

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

@[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_monoid γ] [has_continuous_add γ] (g : C(α, β)) (f : C(β, γ)) :
@[simp]
theorem continuous_map.pow_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] (f : C(α, β)) (n : ) :
(f ^ n) = f ^ n
@[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
@[instance]
def continuous_map.comm_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_monoid β] [has_continuous_mul β] :
Equations
@[instance]
@[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(α, β)) :
∑ (i : ι) in s, f i = ∑ (i : ι) in s, (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(α, β)) :
∏ (i : ι) in s, f i = ∏ (i : ι) in s, (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 : α) :
(∑ (i : ι) in s, f i) a = ∑ (i : ι) in s, (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 : α) :
(∏ (i : ι) in s, f i) a = ∏ (i : ι) in s, (f i) a
@[instance]
def continuous_map.add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
@[instance]
def continuous_map.group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
group C(α, β)
Equations
@[simp]
theorem continuous_map.neg_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.inv_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.sub_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] (f g : C(α, β)) :
(f - g) = f - g
@[simp]
theorem continuous_map.div_coe {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f g : C(α, β)) :
(f / g) = f / g
@[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(α, β)) :
@[simp]
theorem continuous_map.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [add_group γ] [topological_add_group γ] (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 γ] [group γ] [topological_group γ] (f g : C(β, γ)) (h : C(α, β)) :
(f / g).comp h = f.comp h / g.comp h
@[instance]

Ring stucture #

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

@[instance]
def continuous_subring (α : Type u_1) (R : Type u_2) [topological_space α] [topological_space R] [ring R] [topological_ring R] :
is_subring {f : α → R | continuous f}
@[instance]
def continuous_ring {α : Type u_1} {R : Type u_2} [topological_space α] [topological_space R] [ring R] [topological_ring R] :
ring {f : α → R | continuous f}
Equations
@[instance]
def continuous_comm_ring {α : Type u_1} {R : Type u_2} [topological_space α] [topological_space R] [comm_ring R] [topological_ring R] :
comm_ring {f : α → R | continuous f}
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.

@[instance]
def continuous_has_scalar {α : Type u_1} [topological_space α] {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [has_continuous_smul R M] :
has_scalar R {f : α → M | continuous f}
Equations
@[simp]
theorem continuous_functions.smul_coe {α : Type u_1} [topological_space α] {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [has_continuous_smul R M] (f : {f : α → M | continuous f}) (r : R) :
(r f) = r f
@[instance]
def continuous_module {α : Type u_1} [topological_space α] {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [has_continuous_smul R M] [topological_add_group M] :
module R {f : α → M | continuous f}
Equations
@[instance]
def continuous_map.has_scalar {α : 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
@[simp]
theorem continuous_map.smul_coe {α : 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] (c : R) (f : C(α, M)) :
(c f) = c f
theorem continuous_map.smul_apply {α : 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] (c : R) (f : C(α, M)) (a : α) :
(c f) a = c f a
@[simp]
theorem continuous_map.smul_comp {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_monoid M] {α : Type u_1} {β : Type u_4} [topological_space α] [topological_space β] [module R M] [has_continuous_smul R M] (r : R) (f : C(β, M)) (g : C(α, β)) :
(r f).comp g = r f.comp g

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 (by now we require topological_ring: see TODO below).

def continuous.C {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [ring A] [algebra R A] [topological_ring A] :
R →+* {f : α → A | continuous f}

Continuous constant functions as a ring_hom.

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 : α) :
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] [topological_space R] [has_continuous_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] [topological_space R] [has_continuous_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_4} [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_4} [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 M.

@[instance]
def continuous_has_scalar' {α : Type u_1} [topological_space α] {R : Type u_2} [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_group M] [module R M] [has_continuous_smul R M] :
has_scalar {f : α → R | continuous f} {f : α → M | continuous f}
Equations
@[instance]
def continuous_module' {α : Type u_1} [topological_space α] (R : Type u_2) [ring R] [topological_space R] [topological_ring R] (M : Type u_3) [topological_space M] [add_comm_group M] [topological_add_group M] [module R M] [has_continuous_smul R M] :
module {f : α → R | continuous f} {f : α → M | continuous f}
Equations
@[instance]
def continuous_map.has_scalar' {α : 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} :
min x y = 2⁻¹ * (x + y - abs (x - y))
theorem max_eq_half_add_add_abs_sub {R : Type u_1} [linear_ordered_field R] {x y : R} :
max x y = 2⁻¹ * (x + y + abs (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).abs)
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).abs)