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.

source
@[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
source
@[protected, instance]
def continuous_map.has_mul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] :
has_mul C(α, β)
Equations
source
@[protected, instance]
def continuous_map.has_add {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] :
has_add C(α, β)
Equations
source
@[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
source
@[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
source
@[protected, instance]
def continuous_map.has_zero {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
has_zero C(α, β)
Equations
source
@[protected, instance]
def continuous_map.has_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
has_one C(α, β)
Equations
source
@[simp, norm_cast]
theorem continuous_map.coe_one {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_one β] :
⇑1 = 1
source
@[simp, norm_cast]
theorem continuous_map.coe_zero {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_zero β] :
⇑0 = 0
source
@[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
source
@[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
source
@[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
source
@[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.

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

The submonoid of continuous maps α → β.

Equations
source
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
source
def continuous_subgroup (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] [group β] [topological_group β] :
subgroup (α → β)

The subgroup of continuous maps α → β.

Equations
source
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
source
@[protected, instance]
def continuous_map.add_semigroup {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_semigroup β] [has_continuous_add β] :
add_semigroup C(α, β)
Equations
source
@[protected, instance]
def continuous_map.semigroup {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [semigroup β] [has_continuous_mul β] :
semigroup C(α, β)
Equations
source
@[protected, instance]
def continuous_map.add_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :
add_monoid C(α, β)
Equations
source
@[protected, instance]
def continuous_map.monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :
monoid C(α, β)
Equations
source
@[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(α, β)) (ᾰ : α) :
⇑continuous_map.coe_fn_monoid_hom x ᾰ = ⇑x ᾰ
source
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
source
@[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(α, β)) (ᾰ : α) :
⇑continuous_map.coe_fn_add_monoid_hom x ᾰ = ⇑x ᾰ
source
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.

Equations
source
@[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(α, β)) :
⇑(add_monoid_hom.comp_left_continuous α g hg) f = {to_fun := ⇑g, continuous_to_fun := hg}.comp f
source
@[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
source
@[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
source
@[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(α, β)) :
⇑(monoid_hom.comp_left_continuous α g hg) f = {to_fun := ⇑g, continuous_to_fun := hg}.comp f
source
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
source
@[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(β, γ)) :
⇑(g.comp_monoid_hom') f = f.comp g
source
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'.

Equations
source
@[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(β, γ)) :
⇑(g.comp_add_monoid_hom') f = f.comp g
source
@[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
source
@[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
source
@[protected, instance]
def continuous_map.comm_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_monoid β] [has_continuous_mul β] :
comm_monoid C(α, β)
Equations
source
@[protected, instance]
def continuous_map.add_comm_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_comm_monoid β] [has_continuous_add β] :
add_comm_monoid C(α, β)
Equations
source
@[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)
source
@[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)
source
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
source
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
source
@[protected, instance]
def continuous_map.add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :
add_group C(α, β)
Equations
source
@[protected, instance]
def continuous_map.group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
group C(α, β)
Equations
source
@[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(α, β)) :
⇑-f = -⇑f
source
@[simp, norm_cast]
theorem continuous_map.coe_inv {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] (f : C(α, β)) :
⇑f⁻¹ = (⇑f)⁻¹
source
@[simp, norm_cast]
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
source
@[simp, norm_cast]
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
source
@[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
source
@[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(α, β)) :
f⁻¹.comp g = (f.comp g)⁻¹
source
@[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
source
@[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
source
@[protected, instance]
def continuous_map.comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_group β] [topological_group β] :
comm_group C(α, β)
Equations
source
@[protected, instance]
def continuous_map.add_comm_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_comm_group β] [topological_add_group β] :
add_comm_group C(α, β)
Equations
source
@[protected, instance]
def continuous_map.topological_add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_comm_group β] [topological_add_group β] :
topological_add_group C(α, β)
source
@[protected, instance]
def continuous_map.topological_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_group β] [topological_group β] :
topological_group C(α, β)

Ring stucture #

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

source
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
source
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
source
@[protected, instance]
def continuous_map.semiring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [semiring β] [topological_ring β] :
semiring C(α, β)
Equations
source
@[protected, instance]
def continuous_map.ring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [ring β] [topological_ring β] :
ring C(α, β)
Equations
source
@[protected, instance]
def continuous_map.comm_ring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [comm_ring β] [topological_ring β] :
comm_ring C(α, β)
Equations
source
@[protected]
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
source
@[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(α, β)) :
⇑(ring_hom.comp_left_continuous α g hg) ᾰ = (monoid_hom.comp_left_continuous α g.to_monoid_hom hg).to_fun ᾰ
source
@[simp]
theorem continuous_map.coe_fn_ring_hom_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [ring β] [topological_ring β] (x : C(α, β)) (ᾰ : α) :
⇑continuous_map.coe_fn_ring_hom x ᾰ = ⇑x ᾰ
source
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.

source
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
source
@[protected, 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] :
has_scalar R C(α, M)
Equations
source
@[simp, norm_cast]
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
source
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
source
@[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
source
@[protected, instance]
def continuous_map.module {α : 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] :
module R C(α, M)
Equations
source
@[simp]
theorem continuous_linear_map.comp_left_continuous_apply (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)) :
⇑(continuous_linear_map.comp_left_continuous R α g) ᾰ = (add_monoid_hom.comp_left_continuous α g.to_linear_map.to_add_monoid_hom _).to_fun ᾰ
source
@[protected]
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
source
@[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)) (ᾰ : α) :
⇑(continuous_map.coe_fn_linear_map R) x ᾰ = ⇑x ᾰ
source
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.

source
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
source
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
source
@[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 : α) :
⇑(⇑continuous_map.C r) a = ⇑(algebra_map R A) r
source
@[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_ring A] [topological_space R] [has_continuous_smul R A] :
algebra R C(α, A)
Equations
source
@[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_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
source
@[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)) :
⇑(alg_hom.comp_left_continuous R g hg) ᾰ = (ring_hom.comp_left_continuous α g.to_ring_hom hg).to_fun ᾰ
source
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
source
@[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)) (ᾰ : α) :
⇑(continuous_map.coe_fn_alg_hom R) x ᾰ = ⇑x ᾰ
source
@[protected, 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] :
is_scalar_tower R A C(α, A)
source
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.

source
theorem subalgebra.separates_points_monotone {α : 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] :
monotone (λ (s : subalgebra R C(α, A)), s.separates_points)
source
@[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
source
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
source
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) :
↑s.separates_points_strongly

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.

source
theorem continuous_map.subsingleton_subalgebra (α : Type u_1) [topological_space α] (R : Type u_2) [comm_semiring R] [topological_space R] [topological_ring R] [subsingleton α] :
subsingleton (subalgebra R C(α, R))

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.

source
@[protected, 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] :
has_scalar C(α, R) C(α, M)
Equations
source
@[protected, instance]
def continuous_map.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_monoid M] [has_continuous_add M] [module R M] [has_continuous_smul R M] :
module C(α, R) C(α, M)
Equations

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

source
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|)
source
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|)
source
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|)
source
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|)