Algebraic structures over continuous functions
In this file we define instances of algebraic structures over continuous functions. Instances are present both in the case of the subtype of continuous functions and the type of continuous bundled functions. Both implementations have advantages and disadvantages, but many experienced people in Zulip have expressed a preference towards continuous bundled maps, so when there is no particular reason to use the subtype, continuous bundled functions should be used for the sake of uniformity.
@[instance]
def
continuous_functions.set_of.has_coe_to_fun
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
has_coe_to_fun ↥{f : α → β | continuous f}
Equations
- continuous_functions.set_of.has_coe_to_fun = {F := λ (x : ↥{f : α → β | continuous f}), α → β, coe := subtype.val (λ (x : α → β), x ∈ {f : α → β | continuous f})}
@[instance]
def
continuous_map.has_mul
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_mul β]
[has_continuous_mul β] :
@[instance]
def
continuous_map.has_add
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[has_add β]
[has_continuous_add β] :
@[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
Group stucture
In this section we show that continuous functions valued in a topological group inherit the structure of a group.
@[instance]
def
continuous_submonoid
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
is_submonoid {f : α → β | continuous f}
@[instance]
def
continuous_add_submonoid
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
is_add_submonoid {f : α → β | continuous f}
@[instance]
def
continuous_subgroup
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
is_subgroup {f : α → β | continuous f}
@[instance]
def
continuous_add_subgroup
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
is_add_subgroup {f : α → β | continuous f}
@[instance]
def
continuous_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
monoid ↥{f : α → β | continuous f}
Equations
@[instance]
def
continuous_add_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
add_monoid ↥{f : α → β | continuous f}
@[instance]
def
continuous_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
group ↥{f : α → β | continuous f}
Equations
@[instance]
def
continuous_add_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_group β]
[topological_add_group β] :
add_group ↥{f : α → β | continuous f}
@[instance]
def
continuous_add_comm_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_group β]
[topological_add_group β] :
add_comm_group ↥{f : α → β | continuous f}
@[instance]
def
continuous_comm_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[comm_group β]
[topological_group β] :
comm_group ↥{f : α → β | continuous f}
Equations
@[instance]
def
continuous_map_semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semigroup β]
[has_continuous_mul β] :
Equations
@[instance]
def
continuous_map_add_semigroup
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_semigroup β]
[has_continuous_add β] :
@[instance]
def
continuous_map_add_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_monoid β]
[has_continuous_add β] :
add_monoid C(α, β)
@[instance]
def
continuous_map_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[monoid β]
[has_continuous_mul β] :
Equations
- continuous_map_monoid = {mul := semigroup.mul continuous_map_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
def
continuous_map_add_comm_monoid
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_monoid β]
[has_continuous_add β] :
@[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 = {mul := semigroup.mul continuous_map_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
@[instance]
def
continuous_map_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[group β]
[topological_group β] :
Equations
- continuous_map_group = {mul := monoid.mul continuous_map_monoid, mul_assoc := _, one := monoid.one continuous_map_monoid, one_mul := _, mul_one := _, inv := λ (f : C(α, β)), {to_fun := λ (x : α), (⇑f x)⁻¹, continuous_to_fun := _}, div := div_inv_monoid.div._default monoid.mul continuous_map_group._proof_5 monoid.one continuous_map_group._proof_6 continuous_map_group._proof_7 (λ (f : C(α, β)), {to_fun := λ (x : α), (⇑f x)⁻¹, continuous_to_fun := _}), div_eq_mul_inv := _, mul_left_inv := _}
@[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_add_comm_group
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[add_comm_group β]
[topological_add_group β] :
@[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 = {mul := group.mul continuous_map_group, mul_assoc := _, one := group.one continuous_map_group, one_mul := _, mul_one := _, inv := group.inv continuous_map_group, div := group.div continuous_map_group, div_eq_mul_inv := _, mul_left_inv := _, mul_comm := _}
Ring stucture
In this section we show that continuous functions valued in a topological ring R inherit
the structure of a ring.
@[instance]
def
continuous_subring
(α : Type u_1)
(R : Type u_2)
[topological_space α]
[topological_space R]
[ring R]
[topological_ring R] :
is_subring {f : α → R | continuous f}
@[instance]
def
continuous_ring
{α : Type u_1}
{R : Type u_2}
[topological_space α]
[topological_space R]
[ring R]
[topological_ring R] :
ring ↥{f : α → R | continuous f}
Equations
@[instance]
def
continuous_comm_ring
{α : Type u_1}
{R : Type u_2}
[topological_space α]
[topological_space R]
[comm_ring R]
[topological_ring R] :
comm_ring ↥{f : α → R | continuous f}
Equations
@[instance]
def
continuous_map_semiring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[semiring β]
[topological_semiring β] :
Equations
- continuous_map_semiring = {add := add_comm_monoid.add continuous_map_add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero continuous_map_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := monoid.mul continuous_map_monoid, mul_assoc := _, one := monoid.one continuous_map_monoid, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[instance]
def
continuous_map_ring
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[ring β]
[topological_ring β] :
Equations
- continuous_map_ring = {add := semiring.add continuous_map_semiring, add_assoc := _, zero := semiring.zero continuous_map_semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg continuous_map_add_comm_group, sub := add_comm_group.sub continuous_map_add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul continuous_map_semiring, mul_assoc := _, one := semiring.one continuous_map_semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[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 = {add := semiring.add continuous_map_semiring, add_assoc := _, zero := semiring.zero continuous_map_semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg continuous_map_add_comm_group, sub := add_comm_group.sub continuous_map_add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul continuous_map_semiring, mul_assoc := _, one := semiring.one continuous_map_semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
Semiodule stucture
In this section we show that continuous functions valued in a topological semimodule M over a
topological semiring R inherit the structure of a semimodule.
@[instance]
def
continuous_has_scalar
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[semiring R]
[topological_space R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[semimodule R M]
[topological_semimodule R M] :
has_scalar R ↥{f : α → M | continuous f}
Equations
- continuous_has_scalar = {smul := λ (r : R) (f : ↥{f : α → M | continuous f}), ⟨r • ⇑f, _⟩}
@[instance]
def
continuous_semimodule
{α : 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]
[topological_add_group M]
[semimodule R M]
[topological_semimodule R M] :
semimodule R ↥{f : α → M | continuous f}
Equations
- continuous_semimodule = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul continuous_has_scalar}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
@[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]
[semimodule R M]
[topological_semimodule R M] :
has_scalar R C(α, M)
@[instance]
def
continuous_map_semimodule
{α : 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]
[semimodule R M]
[topological_semimodule R M] :
semimodule R C(α, M)
Equations
- continuous_map_semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul continuous_map_has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_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 topological_semimodule and a topological_semiring
(by now we require topological_ring: see TODO below).
def
continuous.C
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[comm_semiring R]
{A : Type u_3}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A] :
R →+* ↥{f : α → A | continuous f}
Continuous constant functions as a ring_hom.
@[instance]
def
set_of.algebra
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[comm_semiring R]
{A : Type u_3}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A]
[topological_space R]
[topological_semimodule R A] :
algebra R ↥{f : α → A | continuous f}
Equations
- set_of.algebra = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := continuous.C _inst_6, commutes' := _, smul_def' := _}
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' := _}
@[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]
[topological_space R]
[topological_semimodule R A] :
Equations
- continuous_map_algebra = {to_has_scalar := continuous_map_has_scalar _inst_8, to_ring_hom := continuous_map.C _inst_6, commutes' := _, smul_def' := _}
Structure as module over scalar functions
If M is a module over R, then we show that the space of continuous functions from α to M
is naturally a module over the ring of continuous functions from α to M.
@[instance]
def
continuous_has_scalar'
{α : Type u_1}
[topological_space α]
{R : Type u_2}
[semiring R]
[topological_space R]
{M : Type u_3}
[topological_space M]
[add_comm_group M]
[semimodule R M]
[topological_semimodule R M] :
has_scalar ↥{f : α → R | continuous f} ↥{f : α → M | continuous f}
Equations
- continuous_has_scalar' = {smul := λ (f : ↥{f : α → R | continuous f}) (g : ↥{f : α → M | continuous f}), ⟨λ (x : α), ⇑f x • ⇑g x, _⟩}
@[instance]
def
continuous_module'
{α : Type u_1}
[topological_space α]
(R : Type u_2)
[ring R]
[topological_space R]
[topological_ring R]
(M : Type u_3)
[topological_space M]
[add_comm_group M]
[topological_add_group M]
[module R M]
[topological_module R M] :
module ↥{f : α → R | continuous f} ↥{f : α → M | continuous f}
Equations
- continuous_module' R M = semimodule.of_core {to_has_scalar := {smul := has_scalar.smul continuous_has_scalar'}, smul_add := _, add_smul := _, mul_smul := _, one_smul := _}
@[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]
[semimodule R M]
[topological_semimodule R M] :
@[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]
[semimodule R M]
[topological_semimodule R M] :
Equations
- continuous_map_module' R M = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul continuous_map_has_scalar'}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}