Algebraic structures over continuous functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
- continuous_functions.set_of.has_coe_to_fun = {coe := subtype.val (λ (x : α → β), x ∈ {f : α → β | continuous f})}
@[protected, instance]
def
continuous_map.has_mul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_mul β]
[has_continuous_mul β] :
@[protected, instance]
def
continuous_map.has_add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_add β]
[has_continuous_add β] :
@[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(α, β)) :
@[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(α, β)) :
@[simp]
theorem
continuous_map.mul_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_mul β]
[has_continuous_mul β]
(f g : C(α, β))
(x : α) :
@[simp]
theorem
continuous_map.add_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_add β]
[has_continuous_add β]
(f g : C(α, β))
(x : α) :
@[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(α, β)) :
@[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(α, β)) :
@[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 β] :
@[simp, norm_cast]
theorem
continuous_map.coe_zero
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_zero β] :
@[simp]
theorem
continuous_map.zero_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_zero β]
(x : α) :
@[simp]
theorem
continuous_map.one_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_one β]
(x : α) :
@[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(α, β)) :
@[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(α, β)) :
@[protected, instance]
def
continuous_map.has_nat_cast
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_nat_cast β] :
has_nat_cast C(α, β)
Equations
- continuous_map.has_nat_cast = {nat_cast := λ (n : ℕ), continuous_map.const α ↑n}
@[simp, norm_cast]
theorem
continuous_map.coe_nat_cast
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_nat_cast β]
(n : ℕ) :
@[simp]
theorem
continuous_map.nat_cast_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_nat_cast β]
(n : ℕ)
(x : α) :
@[protected, instance]
def
continuous_map.has_int_cast
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_int_cast β] :
has_int_cast C(α, β)
Equations
- continuous_map.has_int_cast = {int_cast := λ (n : ℤ), continuous_map.const α ↑n}
@[simp, norm_cast]
theorem
continuous_map.coe_int_cast
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_int_cast β]
(n : ℤ) :
@[simp]
theorem
continuous_map.int_cast_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_int_cast β]
(n : ℤ)
(x : α) :
@[protected, instance]
def
continuous_map.has_nsmul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
@[protected, instance]
def
continuous_map.has_pow
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
@[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 : ℕ) :
@[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 : ℕ) :
@[simp]
theorem
continuous_map.pow_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β]
(f : C(α, β))
(n : ℕ)
(x : α) :
theorem
continuous_map.nsmul_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β]
(f : C(α, β))
(n : ℕ)
(x : α) :
@[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(α, β)) :
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(α, β)) :
@[protected, instance]
def
continuous_map.has_neg
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
@[protected, instance]
def
continuous_map.has_inv
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
@[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_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(f : C(α, β))
(x : α) :
@[simp]
theorem
continuous_map.inv_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β]
(f : C(α, β))
(x : α) :
@[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(α, β)) :
@[simp]
theorem
continuous_map.inv_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
[group γ]
[topological_group γ]
(f : C(β, γ))
(g : C(α, β)) :
@[protected, instance]
def
continuous_map.has_div
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_div β]
[has_continuous_div β] :
@[protected, instance]
def
continuous_map.has_sub
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_sub β]
[has_continuous_sub β] :
@[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(α, β)) :
@[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(α, β)) :
@[simp]
theorem
continuous_map.sub_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_sub β]
[has_continuous_sub β]
(f g : C(α, β))
(x : α) :
@[simp]
theorem
continuous_map.div_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_div β]
[has_continuous_div β]
(f g : C(α, β))
(x : α) :
@[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(α, β)) :
@[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(α, β)) :
@[protected, instance]
def
continuous_map.has_zsmul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
@[protected, instance]
def
continuous_map.has_zpow
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
@[simp, norm_cast]
theorem
continuous_map.coe_zpow
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β]
(f : C(α, β))
(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 : ℤ) :
theorem
continuous_map.zsmul_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β]
(f : C(α, β))
(z : ℤ)
(x : α) :
@[simp]
theorem
continuous_map.zpow_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β]
(f : C(α, β))
(z : ℤ)
(x : α) :
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(α, β)) :
@[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(α, β)) :
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 β]
[mul_one_class β]
[has_continuous_mul β] :
The submonoid of continuous maps α → β.
Equations
- continuous_submonoid α β = {carrier := {f : α → β | continuous f}, mul_mem' := _, one_mem' := _}
def
continuous_add_submonoid
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[add_zero_class β]
[has_continuous_add β] :
add_submonoid (α → β)
The add_submonoid of continuous maps α → β.
Equations
- continuous_add_submonoid α β = {carrier := {f : α → β | continuous f}, add_mem' := _, zero_mem' := _}
def
continuous_subgroup
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
The subgroup of continuous maps α → β.
Equations
- continuous_subgroup α β = {carrier := (continuous_submonoid α β).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}
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
- continuous_add_subgroup α β = {carrier := (continuous_add_submonoid α β).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
@[protected, instance]
def
continuous_map.add_semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_semigroup β]
[has_continuous_add β] :
Equations
- continuous_map.add_semigroup = function.injective.add_semigroup coe_fn continuous_map.coe_injective continuous_map.add_semigroup._proof_1
@[protected, instance]
def
continuous_map.semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semigroup β]
[has_continuous_mul β] :
Equations
- continuous_map.semigroup = function.injective.semigroup coe_fn continuous_map.coe_injective continuous_map.semigroup._proof_1
@[protected, instance]
def
continuous_map.add_comm_semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_semigroup β]
[has_continuous_add β] :
Equations
- continuous_map.add_comm_semigroup = function.injective.add_comm_semigroup coe_fn continuous_map.coe_injective continuous_map.add_comm_semigroup._proof_1
@[protected, instance]
def
continuous_map.comm_semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_semigroup β]
[has_continuous_mul β] :
Equations
- continuous_map.comm_semigroup = function.injective.comm_semigroup coe_fn continuous_map.coe_injective continuous_map.comm_semigroup._proof_1
@[protected, instance]
def
continuous_map.mul_one_class
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[mul_one_class β]
[has_continuous_mul β] :
Equations
- continuous_map.mul_one_class = function.injective.mul_one_class coe_fn continuous_map.coe_injective continuous_map.mul_one_class._proof_1 continuous_map.mul_one_class._proof_2
@[protected, instance]
def
continuous_map.add_zero_class
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_zero_class β]
[has_continuous_add β] :
Equations
- continuous_map.add_zero_class = function.injective.add_zero_class coe_fn continuous_map.coe_injective continuous_map.add_zero_class._proof_1 continuous_map.add_zero_class._proof_2
@[protected, instance]
def
continuous_map.mul_zero_class
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[mul_zero_class β]
[has_continuous_mul β] :
Equations
- continuous_map.mul_zero_class = function.injective.mul_zero_class coe_fn continuous_map.coe_injective continuous_map.mul_zero_class._proof_1 continuous_map.mul_zero_class._proof_2
@[protected, instance]
def
continuous_map.semigroup_with_zero
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semigroup_with_zero β]
[has_continuous_mul β] :
Equations
- continuous_map.semigroup_with_zero = function.injective.semigroup_with_zero coe_fn continuous_map.coe_injective continuous_map.semigroup_with_zero._proof_1 continuous_map.semigroup_with_zero._proof_2
@[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
- continuous_map.add_monoid = function.injective.add_monoid coe_fn continuous_map.coe_injective continuous_map.add_monoid._proof_1 continuous_map.add_monoid._proof_2 continuous_map.coe_nsmul
@[protected, instance]
def
continuous_map.monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
Equations
- continuous_map.monoid = function.injective.monoid coe_fn continuous_map.coe_injective continuous_map.monoid._proof_1 continuous_map.monoid._proof_2 continuous_map.coe_pow
@[protected, instance]
def
continuous_map.monoid_with_zero
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid_with_zero β]
[has_continuous_mul β] :
Equations
- continuous_map.monoid_with_zero = function.injective.monoid_with_zero coe_fn continuous_map.coe_injective continuous_map.monoid_with_zero._proof_1 continuous_map.monoid_with_zero._proof_2 continuous_map.monoid_with_zero._proof_3 continuous_map.monoid_with_zero._proof_4
@[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
- continuous_map.comm_monoid = function.injective.comm_monoid coe_fn continuous_map.coe_injective continuous_map.comm_monoid._proof_1 continuous_map.comm_monoid._proof_2 continuous_map.comm_monoid._proof_3
@[protected, instance]
def
continuous_map.add_comm_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β] :
Equations
- continuous_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn continuous_map.coe_injective continuous_map.add_comm_monoid._proof_1 continuous_map.add_comm_monoid._proof_2 continuous_map.add_comm_monoid._proof_3
@[protected, instance]
def
continuous_map.comm_monoid_with_zero
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_monoid_with_zero β]
[has_continuous_mul β] :
Equations
- continuous_map.comm_monoid_with_zero = function.injective.comm_monoid_with_zero coe_fn continuous_map.coe_injective continuous_map.comm_monoid_with_zero._proof_1 continuous_map.comm_monoid_with_zero._proof_2 continuous_map.comm_monoid_with_zero._proof_3 continuous_map.comm_monoid_with_zero._proof_4
@[protected, instance]
def
continuous_map.has_continuous_mul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
[has_mul β]
[has_continuous_mul β] :
@[protected, instance]
def
continuous_map.has_continuous_add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
[has_add β]
[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(α, β))
(ᾰ : α) :
⇑continuous_map.coe_fn_monoid_hom x ᾰ = ⇑x ᾰ
def
continuous_map.coe_fn_monoid_hom
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
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 β] :
Coercion to a function as an add_monoid_hom. Similar to add_monoid_hom.coe_fn.
Equations
@[simp]
theorem
add_monoid_hom.comp_left_continuous_apply
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[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
@[protected]
def
add_monoid_hom.comp_left_continuous
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[add_monoid β]
[has_continuous_add β]
[topological_space γ]
[add_monoid γ]
[has_continuous_add γ]
(g : β →+ γ)
(hg : continuous ⇑g) :
Composition on the left by a (continuous) homomorphism of topological add_monoids,
as an add_monoid_hom. Similar to add_monoid_hom.comp_left.
@[protected]
def
monoid_hom.comp_left_continuous
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[monoid β]
[has_continuous_mul β]
[topological_space γ]
[monoid γ]
[has_continuous_mul γ]
(g : β →* γ)
(hg : continuous ⇑g) :
Composition on the left by a (continuous) homomorphism of topological monoids, as a
monoid_hom. Similar to monoid_hom.comp_left.
@[simp]
theorem
monoid_hom.comp_left_continuous_apply
(α : Type u_1)
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[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
def
continuous_map.comp_monoid_hom'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[topological_space γ]
[mul_one_class γ]
[has_continuous_mul γ]
(g : C(α, β)) :
Composition on the right as a monoid_hom. Similar to monoid_hom.comp_hom'.
@[simp]
theorem
continuous_map.comp_monoid_hom'_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[topological_space γ]
[mul_one_class γ]
[has_continuous_mul γ]
(g : C(α, β))
(f : C(β, γ)) :
⇑(g.comp_monoid_hom') f = f.comp g
def
continuous_map.comp_add_monoid_hom'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[topological_space γ]
[add_zero_class γ]
[has_continuous_add γ]
(g : 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}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[topological_space γ]
[add_zero_class γ]
[has_continuous_add γ]
(g : C(α, β))
(f : C(β, γ)) :
⇑(g.comp_add_monoid_hom') f = f.comp g
@[simp]
theorem
continuous_map.coe_sum
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β]
{ι : Type u_3}
(s : finset ι)
(f : ι → C(α, β)) :
@[simp]
theorem
continuous_map.coe_prod
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_monoid β]
[has_continuous_mul β]
{ι : Type u_3}
(s : finset ι)
(f : ι → C(α, β)) :
theorem
continuous_map.sum_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β]
{ι : Type u_3}
(s : finset ι)
(f : ι → C(α, β))
(a : α) :
theorem
continuous_map.prod_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_monoid β]
[has_continuous_mul β]
{ι : Type u_3}
(s : finset ι)
(f : ι → C(α, β))
(a : α) :
@[protected, instance]
def
continuous_map.add_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
Equations
- continuous_map.add_group = function.injective.add_group coe_fn continuous_map.coe_injective continuous_map.add_group._proof_1 continuous_map.add_group._proof_2 continuous_map.coe_neg continuous_map.add_group._proof_3 continuous_map.add_group._proof_4 continuous_map.coe_zsmul
@[protected, instance]
def
continuous_map.group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
Equations
- continuous_map.group = function.injective.group coe_fn continuous_map.coe_injective continuous_map.group._proof_1 continuous_map.group._proof_2 continuous_map.coe_inv continuous_map.group._proof_3 continuous_map.group._proof_4 continuous_map.coe_zpow
@[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
- continuous_map.comm_group = function.injective.comm_group coe_fn continuous_map.coe_injective continuous_map.comm_group._proof_4 continuous_map.comm_group._proof_5 continuous_map.comm_group._proof_6 continuous_map.comm_group._proof_7 continuous_map.comm_group._proof_8 continuous_map.comm_group._proof_9
@[protected, instance]
def
continuous_map.add_comm_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_group β]
[topological_add_group β] :
Equations
- continuous_map.add_comm_group = function.injective.add_comm_group coe_fn continuous_map.coe_injective continuous_map.add_comm_group._proof_4 continuous_map.add_comm_group._proof_5 continuous_map.add_comm_group._proof_6 continuous_map.add_comm_group._proof_7 continuous_map.add_comm_group._proof_8 continuous_map.add_comm_group._proof_9
@[protected, instance]
def
continuous_map.topological_add_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_group β]
[topological_add_group β] :
@[protected, instance]
def
continuous_map.topological_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_group β]
[topological_group β] :
theorem
continuous_map.has_sum_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{γ : Type u_3}
[locally_compact_space α]
[add_comm_monoid β]
[has_continuous_add β]
{f : γ → C(α, β)}
{g : C(α, β)}
(hf : has_sum f g)
(x : α) :
If α is locally compact, and an infinite sum of functions in C(α, β)
converges to g (for the compact-open topology), then the pointwise sum converges to g x for
all x ∈ α.
theorem
continuous_map.summable_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
[add_comm_monoid β]
[has_continuous_add β]
{γ : Type u_3}
{f : γ → C(α, β)}
(hf : summable f)
(x : α) :
theorem
continuous_map.tsum_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
[t2_space β]
[add_comm_monoid β]
[has_continuous_add β]
{γ : Type u_3}
{f : γ → C(α, β)}
(hf : summable f)
(x : α) :
Ring stucture #
In this section we show that continuous functions valued in a topological semiring R inherit
the structure of a ring.
def
continuous_subsemiring
(α : Type u_1)
(R : Type u_2)
[topological_space α]
[topological_space R]
[non_assoc_semiring R]
[topological_semiring R] :
subsemiring (α → R)
The subsemiring of continuous maps α → β.
Equations
- continuous_subsemiring α R = {carrier := (continuous_add_submonoid α R).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _}
def
continuous_subring
(α : Type u_1)
(R : Type u_2)
[topological_space α]
[topological_space R]
[ring R]
[topological_ring R] :
The subring of continuous maps α → β.
@[protected, instance]
def
continuous_map.non_unital_non_assoc_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_non_assoc_semiring β]
[topological_semiring β] :
Equations
- continuous_map.non_unital_non_assoc_semiring = function.injective.non_unital_non_assoc_semiring coe_fn continuous_map.coe_injective continuous_map.non_unital_non_assoc_semiring._proof_1 continuous_map.non_unital_non_assoc_semiring._proof_2 continuous_map.non_unital_non_assoc_semiring._proof_3 continuous_map.non_unital_non_assoc_semiring._proof_4
@[protected, instance]
def
continuous_map.non_unital_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_semiring β]
[topological_semiring β] :
Equations
- continuous_map.non_unital_semiring = function.injective.non_unital_semiring coe_fn continuous_map.coe_injective continuous_map.non_unital_semiring._proof_4 continuous_map.non_unital_semiring._proof_5 continuous_map.non_unital_semiring._proof_6 continuous_map.non_unital_semiring._proof_7
@[protected, instance]
def
continuous_map.add_monoid_with_one
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_monoid_with_one β]
[has_continuous_add β] :
Equations
- continuous_map.add_monoid_with_one = function.injective.add_monoid_with_one coe_fn continuous_map.coe_injective continuous_map.add_monoid_with_one._proof_1 continuous_map.add_monoid_with_one._proof_2 continuous_map.add_monoid_with_one._proof_3 continuous_map.add_monoid_with_one._proof_4 continuous_map.add_monoid_with_one._proof_5
@[protected, instance]
def
continuous_map.non_assoc_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_assoc_semiring β]
[topological_semiring β] :
Equations
- continuous_map.non_assoc_semiring = function.injective.non_assoc_semiring coe_fn continuous_map.coe_injective continuous_map.non_assoc_semiring._proof_4 continuous_map.non_assoc_semiring._proof_5 continuous_map.non_assoc_semiring._proof_6 continuous_map.non_assoc_semiring._proof_7 continuous_map.non_assoc_semiring._proof_8 continuous_map.non_assoc_semiring._proof_9
@[protected, instance]
def
continuous_map.semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β] :
Equations
- continuous_map.semiring = function.injective.semiring coe_fn continuous_map.coe_injective continuous_map.semiring._proof_5 continuous_map.semiring._proof_6 continuous_map.semiring._proof_7 continuous_map.semiring._proof_8 continuous_map.semiring._proof_9 continuous_map.semiring._proof_10 continuous_map.semiring._proof_11
@[protected, instance]
def
continuous_map.non_unital_non_assoc_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_non_assoc_ring β]
[topological_ring β] :
Equations
- continuous_map.non_unital_non_assoc_ring = function.injective.non_unital_non_assoc_ring coe_fn continuous_map.coe_injective continuous_map.non_unital_non_assoc_ring._proof_5 continuous_map.non_unital_non_assoc_ring._proof_6 continuous_map.non_unital_non_assoc_ring._proof_7 continuous_map.non_unital_non_assoc_ring._proof_8 continuous_map.non_unital_non_assoc_ring._proof_9 continuous_map.non_unital_non_assoc_ring._proof_10 continuous_map.non_unital_non_assoc_ring._proof_11
@[protected, instance]
def
continuous_map.non_unital_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_ring β]
[topological_ring β] :
Equations
- continuous_map.non_unital_ring = function.injective.non_unital_ring coe_fn continuous_map.coe_injective continuous_map.non_unital_ring._proof_7 continuous_map.non_unital_ring._proof_8 continuous_map.non_unital_ring._proof_9 continuous_map.non_unital_ring._proof_10 continuous_map.non_unital_ring._proof_11 continuous_map.non_unital_ring._proof_12 continuous_map.non_unital_ring._proof_13
@[protected, instance]
def
continuous_map.non_assoc_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_assoc_ring β]
[topological_ring β] :
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 β] :
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]
def
continuous_map.non_unital_comm_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_comm_semiring β]
[topological_semiring β] :
Equations
- continuous_map.non_unital_comm_semiring = function.injective.non_unital_comm_semiring coe_fn continuous_map.coe_injective continuous_map.non_unital_comm_semiring._proof_4 continuous_map.non_unital_comm_semiring._proof_5 continuous_map.non_unital_comm_semiring._proof_6 continuous_map.non_unital_comm_semiring._proof_7
@[protected, instance]
def
continuous_map.comm_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_semiring β]
[topological_semiring β] :
Equations
- continuous_map.comm_semiring = function.injective.comm_semiring coe_fn continuous_map.coe_injective continuous_map.comm_semiring._proof_5 continuous_map.comm_semiring._proof_6 continuous_map.comm_semiring._proof_7 continuous_map.comm_semiring._proof_8 continuous_map.comm_semiring._proof_9 continuous_map.comm_semiring._proof_10 continuous_map.comm_semiring._proof_11
@[protected, instance]
def
continuous_map.non_unital_comm_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[non_unital_comm_ring β]
[topological_ring β] :
Equations
- continuous_map.non_unital_comm_ring = function.injective.non_unital_comm_ring coe_fn continuous_map.coe_injective continuous_map.non_unital_comm_ring._proof_7 continuous_map.non_unital_comm_ring._proof_8 continuous_map.non_unital_comm_ring._proof_9 continuous_map.non_unital_comm_ring._proof_10 continuous_map.non_unital_comm_ring._proof_11 continuous_map.non_unital_comm_ring._proof_12 continuous_map.non_unital_comm_ring._proof_13
@[protected, instance]
def
continuous_map.comm_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_ring β]
[topological_ring β] :
Equations
- continuous_map.comm_ring = function.injective.comm_ring coe_fn continuous_map.coe_injective continuous_map.comm_ring._proof_8 continuous_map.comm_ring._proof_9 continuous_map.comm_ring._proof_10 continuous_map.comm_ring._proof_11 continuous_map.comm_ring._proof_12 continuous_map.comm_ring._proof_13 continuous_map.comm_ring._proof_14 continuous_map.comm_ring._proof_15 continuous_map.comm_ring._proof_16 continuous_map.comm_ring._proof_17 continuous_map.comm_ring._proof_18
@[protected]
def
ring_hom.comp_left_continuous
(α : Type u_1)
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β]
[topological_space γ]
[semiring γ]
[topological_semiring γ]
(g : β →+* γ)
(hg : continuous ⇑g) :
Composition on the left by a (continuous) homomorphism of topological semirings, as a
ring_hom. Similar to ring_hom.comp_left.
Equations
- ring_hom.comp_left_continuous α g hg = {to_fun := (monoid_hom.comp_left_continuous α g.to_monoid_hom hg).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
ring_hom.comp_left_continuous_apply
(α : Type u_1)
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β]
[topological_space γ]
[semiring γ]
[topological_semiring γ]
(g : β →+* γ)
(hg : continuous ⇑g)
(ᾰ : C(α, β)) :
⇑(ring_hom.comp_left_continuous α g hg) ᾰ = (monoid_hom.comp_left_continuous α g.to_monoid_hom hg).to_fun ᾰ
@[simp]
theorem
continuous_map.coe_fn_ring_hom_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β]
(x : C(α, β))
(ᾰ : α) :
⇑continuous_map.coe_fn_ring_hom x ᾰ = ⇑x ᾰ
def
continuous_map.coe_fn_ring_hom
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β] :
Coercion to a function as a ring_hom.
Equations
- continuous_map.coe_fn_ring_hom = {to_fun := coe_fn continuous_map.has_coe_to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Semiodule stucture #
In this section we show that continuous functions valued in a topological module M over a
topological semiring R inherit the structure of a module.
def
continuous_submodule
(α : Type u_1)
[topological_space α]
(R : Type u_2)
[semiring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[module R M]
[has_continuous_const_smul R M]
[topological_add_group M] :
The R-submodule of continuous maps α → M.
Equations
- continuous_submodule α R M = {carrier := {f : α → M | continuous f}, add_mem' := _, zero_mem' := _, smul_mem' := _}
@[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] :
@[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] :
@[protected, instance]
def
continuous_map.has_continuous_const_smul
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[locally_compact_space α]
[has_smul R M]
[has_continuous_const_smul R M] :
@[protected, instance]
def
continuous_map.has_continuous_const_vadd
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[locally_compact_space α]
[has_vadd R M]
[has_continuous_const_vadd R M] :
@[protected, instance]
def
continuous_map.has_continuous_vadd
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[locally_compact_space α]
[topological_space R]
[has_vadd R M]
[has_continuous_vadd R M] :
has_continuous_vadd R C(α, M)
@[protected, instance]
def
continuous_map.has_continuous_smul
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[locally_compact_space α]
[topological_space R]
[has_smul R M]
[has_continuous_smul R M] :
has_continuous_smul R C(α, M)
@[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)) :
@[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)) :
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 : α) :
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 : α) :
@[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(α, β)) :
@[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(α, β)) :
@[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] :
vadd_comm_class R R₁ C(α, 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] :
smul_comm_class R R₁ C(α, 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] :
is_scalar_tower R R₁ C(α, M)
@[protected, instance]
def
continuous_map.is_central_scalar
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[has_smul R M]
[has_smul Rᵐᵒᵖ M]
[has_continuous_const_smul R M]
[is_central_scalar R M] :
is_central_scalar R C(α, M)
@[protected, instance]
def
continuous_map.mul_action
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[monoid R]
[mul_action R M]
[has_continuous_const_smul R M] :
mul_action R C(α, M)
Equations
- continuous_map.mul_action = function.injective.mul_action coe_fn continuous_map.coe_injective continuous_map.mul_action._proof_1
@[protected, instance]
def
continuous_map.distrib_mul_action
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[monoid R]
[add_monoid M]
[distrib_mul_action R M]
[has_continuous_add M]
[has_continuous_const_smul R M] :
distrib_mul_action R C(α, M)
Equations
- continuous_map.distrib_mul_action = function.injective.distrib_mul_action continuous_map.coe_fn_add_monoid_hom continuous_map.coe_injective continuous_map.distrib_mul_action._proof_1
@[protected, instance]
def
continuous_map.module
{α : Type u_1}
[topological_space α]
{R : Type u_3}
{M : Type u_5}
[topological_space M]
[semiring R]
[add_comm_monoid M]
[has_continuous_add M]
[module R M]
[has_continuous_const_smul R M] :
Equations
- continuous_map.module = function.injective.module R continuous_map.coe_fn_add_monoid_hom continuous_map.coe_injective continuous_map.module._proof_1
@[simp]
theorem
continuous_linear_map.comp_left_continuous_apply
(R : Type u_3)
{M : Type u_5}
[topological_space M]
{M₂ : Type u_6}
[topological_space M₂]
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[has_continuous_add M]
[module R M]
[has_continuous_const_smul R M]
[has_continuous_add M₂]
[module R M₂]
[has_continuous_const_smul R M₂]
(α : Type u_1)
[topological_space α]
(g : M →L[R] M₂)
(ᾰ : C(α, M)) :
@[protected]
def
continuous_linear_map.comp_left_continuous
(R : Type u_3)
{M : Type u_5}
[topological_space M]
{M₂ : Type u_6}
[topological_space M₂]
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[has_continuous_add M]
[module R M]
[has_continuous_const_smul R M]
[has_continuous_add M₂]
[module R M₂]
[has_continuous_const_smul R M₂]
(α : Type u_1)
[topological_space α]
(g : M →L[R] M₂) :
Composition on the left by a continuous linear map, as a linear_map.
Similar to linear_map.comp_left.
Equations
- continuous_linear_map.comp_left_continuous R α g = {to_fun := (add_monoid_hom.comp_left_continuous α g.to_linear_map.to_add_monoid_hom _).to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
continuous_map.coe_fn_linear_map_apply
{α : Type u_1}
[topological_space α]
(R : Type u_3)
{M : Type u_5}
[topological_space M]
[semiring R]
[add_comm_monoid M]
[has_continuous_add M]
[module R M]
[has_continuous_const_smul R M]
(x : C(α, M))
(ᾰ : α) :
⇑(continuous_map.coe_fn_linear_map R) x ᾰ = ⇑x ᾰ
def
continuous_map.coe_fn_linear_map
{α : Type u_1}
[topological_space α]
(R : Type u_3)
{M : Type u_5}
[topological_space M]
[semiring R]
[add_comm_monoid M]
[has_continuous_add M]
[module R M]
[has_continuous_const_smul R M] :
Coercion to a function as a linear_map.
Equations
- continuous_map.coe_fn_linear_map R = {to_fun := coe_fn continuous_map.has_coe_to_fun, map_add' := _, map_smul' := _}
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
- continuous_subalgebra = {carrier := {f : α → A | continuous f}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
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] :
Continuous constant functions as a ring_hom.
Equations
- continuous_map.C = {to_fun := λ (c : R), {to_fun := λ (x : α), ⇑(algebra_map R A) c, continuous_to_fun := _}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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 : α) :
⇑(⇑continuous_map.C r) a = ⇑(algebra_map R A) r
@[protected, instance]
def
continuous_map.algebra
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[comm_semiring R]
{A : Type u_3}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A] :
Equations
- continuous_map.algebra = {to_has_smul := continuous_map.has_smul continuous_map.algebra._proof_1, to_ring_hom := continuous_map.C _inst_6, commutes' := _, smul_def' := _}
@[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) :
Composition on the left by a (continuous) homomorphism of topological R-algebras, as an
alg_hom. Similar to alg_hom.comp_left.
Equations
- alg_hom.comp_left_continuous R g hg = {to_fun := (ring_hom.comp_left_continuous α g.to_ring_hom hg).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[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)) :
⇑(alg_hom.comp_left_continuous R g hg) ᾰ = (ring_hom.comp_left_continuous α g.to_ring_hom hg).to_fun ᾰ
@[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)) :
⇑(continuous_map.comp_right_alg_hom R A f) g = g.comp f
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(α, β)) :
Precomposition of functions into a normed ring by a continuous map is an algebra homomorphism.
def
continuous_map.coe_fn_alg_hom
{α : Type u_1}
[topological_space α]
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A] :
Coercion to a function as an alg_hom.
@[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))
(ᾰ : α) :
⇑(continuous_map.coe_fn_alg_hom R) x ᾰ = ⇑x ᾰ
@[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.
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_semiring A] :
monotone (λ (s : subalgebra R C(α, A)), s.separates_points)
@[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 : α) :
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.)
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.
@[protected, instance]
def
continuous_map.subsingleton_subalgebra
(α : Type u_1)
[topological_space α]
(R : Type u_2)
[comm_semiring R]
[topological_space R]
[topological_semiring 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.
@[protected, instance]
def
continuous_map.has_smul'
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[semiring R]
[topological_space R]
{M : Type u_3}
[topological_space M]
[add_comm_monoid M]
[module R M]
[has_continuous_smul R M] :
@[protected, instance]
def
continuous_map.module'
{α : Type u_1}
[topological_space α]
(R : Type u_2)
[semiring R]
[topological_space R]
[topological_semiring R]
(M : Type u_3)
[topological_space M]
[add_comm_monoid M]
[has_continuous_add M]
[module R M]
[has_continuous_smul R M] :
Equations
- continuous_map.module' R M = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul continuous_map.has_smul'}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
We now provide formulas for f ⊓ g and f ⊔ g, where f g : C(α, β),
in terms of continuous_map.abs.
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(α, β)) :
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(α, β)) :
Star structure #
If β has a continuous star operation, we put a star structure on C(α, β) by using the
star operation pointwise.
If β is a ⋆-ring, then C(α, β) inherits a ⋆-ring structure.
If β is a ⋆-ring and a ⋆-module over R, then the space of continuous functions from α to β
is a ⋆-module over R.
@[protected, instance]
def
continuous_map.has_star
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[has_star β]
[has_continuous_star β] :
Equations
- continuous_map.has_star = {star := λ (f : C(α, β)), star_continuous_map.comp f}
@[simp]
theorem
continuous_map.coe_star
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[has_star β]
[has_continuous_star β]
(f : C(α, β)) :
⇑(has_star.star f) = has_star.star ⇑f
@[simp]
theorem
continuous_map.star_apply
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[has_star β]
[has_continuous_star β]
(f : C(α, β))
(x : α) :
⇑(has_star.star f) x = has_star.star (⇑f x)
@[protected, instance]
def
continuous_map.has_involutive_star
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[has_involutive_star β]
[has_continuous_star β] :
Equations
- continuous_map.has_involutive_star = {to_has_star := continuous_map.has_star _inst_4, star_involutive := _}
@[protected, instance]
def
continuous_map.star_add_monoid
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β]
[star_add_monoid β]
[has_continuous_star β] :
Equations
@[protected, instance]
def
continuous_map.star_semigroup
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[semigroup β]
[has_continuous_mul β]
[star_semigroup β]
[has_continuous_star β] :
Equations
@[protected, instance]
def
continuous_map.star_ring
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[non_unital_semiring β]
[topological_semiring β]
[star_ring β]
[has_continuous_star β] :
Equations
- continuous_map.star_ring = {to_star_semigroup := continuous_map.star_semigroup _inst_6, star_add := _}
@[protected, instance]
def
continuous_map.star_module
{R : Type u_1}
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[topological_space β]
[has_star R]
[has_star β]
[has_smul R β]
[star_module R β]
[has_continuous_star β]
[has_continuous_const_smul R β] :
star_module R C(α, β)
def
continuous_map.comp_star_alg_hom'
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(𝕜 : Type u_4)
[comm_semiring 𝕜]
(A : Type u_5)
[topological_space A]
[semiring A]
[topological_semiring A]
[star_ring A]
[has_continuous_star A]
[algebra 𝕜 A]
(f : C(X, Y)) :
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.
@[simp]
theorem
continuous_map.comp_star_alg_hom'_apply
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
(𝕜 : Type u_4)
[comm_semiring 𝕜]
(A : Type u_5)
[topological_space A]
[semiring A]
[topological_semiring A]
[star_ring A]
[has_continuous_star A]
[algebra 𝕜 A]
(f : C(X, Y))
(g : C(Y, A)) :
⇑(continuous_map.comp_star_alg_hom' 𝕜 A f) g = g.comp f
theorem
continuous_map.comp_star_alg_hom'_id
{X : Type u_1}
[topological_space X]
(𝕜 : Type u_4)
[comm_semiring 𝕜]
(A : Type u_5)
[topological_space A]
[semiring A]
[topological_semiring A]
[star_ring A]
[has_continuous_star A]
[algebra 𝕜 A] :
continuous_map.comp_star_alg_hom' sends the identity continuous map to the identity
star_alg_hom
theorem
continuous_map.comp_star_alg_hom'_comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[topological_space X]
[topological_space Y]
[topological_space Z]
(𝕜 : Type u_4)
[comm_semiring 𝕜]
(A : Type u_5)
[topological_space A]
[semiring A]
[topological_semiring A]
[star_ring A]
[has_continuous_star A]
[algebra 𝕜 A]
(g : C(Y, Z))
(f : C(X, Y)) :
continuous_map.comp_star_alg_hom' 𝕜 A (g.comp f) = (continuous_map.comp_star_alg_hom' 𝕜 A f).comp (continuous_map.comp_star_alg_hom' 𝕜 A g)
continuous_map.comp_star_alg_hom is functorial.
Summing translates of a function #
theorem
continuous_map.periodic_tsum_comp_add_zsmul
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
[locally_compact_space X]
[add_comm_group X]
[topological_add_group X]
[add_comm_monoid Y]
[has_continuous_add Y]
[t2_space Y]
(f : C(X, Y))
(p : X) :
function.periodic (⇑∑' (n : ℤ), f.comp (continuous_map.add_right (n • p))) p
Summing the translates of f by ℤ • p gives a map which is periodic with period p.
(This is true without any convergence conditions, since if the sum doesn't converge it is taken to
be the zero map, which is periodic.)
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.
@[simp]
theorem
homeomorph.comp_star_alg_equiv'_symm_apply
{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)
(ᾰ : C(X, A)) :
⇑((homeomorph.comp_star_alg_equiv' 𝕜 A f).symm) ᾰ = ⇑(continuous_map.comp_star_alg_hom' 𝕜 A ↑(f.symm)) ᾰ
@[simp]
theorem
homeomorph.comp_star_alg_equiv'_apply
{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)
(ᾰ : C(Y, A)) :
⇑(homeomorph.comp_star_alg_equiv' 𝕜 A f) ᾰ = ⇑(continuous_map.comp_star_alg_hom' 𝕜 A ↑f) ᾰ