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.

@[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.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]
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
@[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.coe_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
1 = 1
@[simp]
theorem continuous_map.coe_zero {α : 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.

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 α → β.

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 α → β.

@[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.

@[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(α, β)) :
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.

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 γ] [monoid γ] [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 γ] [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.coe_pow {α : 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.coe_neg {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.coe_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f : C(α, β)) :
@[simp]
theorem continuous_map.coe_div {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f g : C(α, β)) :
(f / g) = f / g
@[simp]
theorem continuous_map.coe_sub {α : 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.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.

def continuous_subsemiring (α : Type u_1) (R : Type u_2) [topological_space α] [topological_space R] [semiring R] [topological_ring 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
def ring_hom.comp_left_continuous (α : Type u_1) {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [semiring β] [topological_ring β] [topological_space γ] [semiring γ] [topological_ring γ] (g : β →+* γ) (hg : continuous g) :
C(α, β) →+* C(α, γ)

Composition on the left by a (continuous) homomorphism of topological rings, 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_ring β] [topological_space γ] [semiring γ] [topological_ring γ] (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] [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] :
submodule R (α → M)

The R-submodule of continuous maps α → M.

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.coe_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] (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
def continuous_linear_map.comp_left_continuous (R : Type u_2) [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_monoid M] {M₂ : Type u_4} [topological_space M₂] [add_comm_monoid M₂] [has_continuous_add M] [module R M] [has_continuous_smul R M] [has_continuous_add M₂] [module R M₂] [has_continuous_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_2) [semiring R] [topological_space R] {M : Type u_3} [topological_space M] [add_comm_monoid M] [has_continuous_add M] [module R M] [has_continuous_smul R M] (x : C(α, M)) (ᾰ : α) :
def continuous_map.coe_fn_linear_map {α : 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] [has_continuous_add M] [module R M] [has_continuous_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_ring.

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_ring 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_ring 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_ring A] (r : R) (a : α) :
@[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_ring A] [topological_space R] [has_continuous_smul R A] :
Equations
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_ring A] {A₂ : Type u_4} [topological_space A₂] [semiring A₂] [algebra R A₂] [topological_ring A₂] [topological_space R] [has_continuous_smul R A] [has_continuous_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_ring A] {A₂ : Type u_4} [topological_space A₂] [semiring A₂] [algebra R A₂] [topological_ring A₂] [topological_space R] [has_continuous_smul R A] [has_continuous_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_ring A] [topological_space R] [has_continuous_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_ring A] [topological_space R] [has_continuous_smul R A] (x : C(α, A)) (ᾰ : α) :
@[instance]
def continuous_map.is_scalar_tower {α : 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_ring A] [topological_space R] [has_continuous_smul 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_ring 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_ring 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_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.

@[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 - |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 + |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|)