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.
Equations
- continuous_functions.set_of.has_coe_to_fun = {F := λ (x : ↥{f : α → β | continuous f}), α → β, coe := subtype.val (λ (x : α → β), x ∈ {f : α → β | continuous f})}
Equations
Group stucture
In this section we show that continuous functions valued in a topological group inherit the structure of a group.
Equations
Equations
Equations
Equations
Equations
- continuous_map_monoid = {mul := semigroup.mul continuous_map_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _}
Equations
- continuous_map_comm_monoid = {mul := semigroup.mul continuous_map_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
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 := _}
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.
Equations
Equations
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 := _}
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 := _}
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.
Equations
- continuous_has_scalar = {smul := λ (r : R) (f : ↥{f : α → M | continuous f}), ⟨r • ⇑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 := _}
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).
Continuous constant functions as a ring_hom
.
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' := _}
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' := _}
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
.
Equations
- continuous_has_scalar' = {smul := λ (f : ↥{f : α → R | continuous f}) (g : ↥{f : α → M | continuous f}), ⟨λ (x : α), ⇑f x • ⇑g x, _⟩}
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 := _}
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 := _}