mathlib documentation

topology.algebra.continuous_functions

Algebraic structures over continuous functions

In this file we define instances of algebraic sturctures 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.has_coe_to_fun {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
has_coe_to_fun {f : α → β | continuous f}

Equations
@[instance]
def continuous_map.has_mul {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_mul β] [has_continuous_mul β] :

Equations
@[instance]
def continuous_map.has_add {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [has_add β] [has_continuous_add β] :

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

@[instance]
def continuous_map_add_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_monoid β] [has_continuous_add β] :

@[instance]
def continuous_map_monoid {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [monoid β] [has_continuous_mul β] :

Equations
@[instance]

@[instance]
def continuous_map_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [group β] [topological_group β] :
group C(α, β)

Equations
@[instance]
def continuous_map_add_group {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [add_group β] [topological_add_group β] :

@[instance]

Ring stucture

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

@[instance]
def continuous_subring (α : Type u_1) (R : Type u_2) [topological_space α] [topological_space R] [ring R] [topological_ring R] :
is_subring {f : α → R | continuous f}

@[instance]
def continuous_ring {α : Type u_1} {R : Type u_2} [topological_space α] [topological_space R] [ring R] [topological_ring R] :
ring {f : α → R | continuous f}

Equations
@[instance]
def continuous_comm_ring {α : Type u_1} {R : Type u_2} [topological_space α] [topological_space R] [comm_ring R] [topological_ring R] :
comm_ring {f : α → R | continuous f}

Equations

Semiodule stucture

In this section we show that continuous functions valued in a topological 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
@[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] :

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

Equations
def continuous_map.C {α : Type u_1} [topological_space α] {R : Type u_2} [comm_semiring R] {A : Type u_3} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] :
R →+* C(α, A)

Continuous constant functions as a ring_hom.

Equations

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
@[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
@[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] :

Equations