## Stream: maths

### Topic: Subset of structure

#### Ashvni Narayanan (Mar 09 2021 at 20:19):

I am trying to show that, under certain conditions, for topological spaces X and Y, the space of locally constant functions from X to Y are a subset of C(X,Y). The issue is, both locally_constant X Y and C(X,Y) are structures. In this case, how does one think of (or construct) subsets? I thought an alternative might be to show an injection. Moreover, in particular cases, there are results which show that C(X,R) is an R-semimodule, then why does has_subset C(X,R) need to be proved? Here is an mwe of what I am trying to do :

import measure_theory.integration
import algebra.group.hom
import ring_theory.int.basic
import set_theory.zfc
import topology.category.Profinite
import topology.locally_constant.algebra
import topology.algebra.continuous_functions

variables (X : Profinite)
instance semi {R : Type*} [semiring R] : semimodule R (locally_constant X R) := sorry

variables {R : Type*} [ring R]
instance uniform [topological_space R] : uniform_space C(X, R) := sorry
instance completeness [topological_space R] : complete_space C(X, R) := sorry
instance sub [topological_space R] [topological_ring R] : (locally_constant X R) ⊆ (C(X,R)) := sorry


which gives me an error :

failed to synthesize type class instance for
X : Profinite,
R : Type u_3,
_inst_4 : ring R,
_inst_6 : topological_space R,
_inst_7 : topological_ring R
⊢ has_subset (Type (max ? ?))


Any help is appreciated, thank you!

#### Heather Macbeth (Mar 09 2021 at 20:26):

You're right, you should make an injective map from locally_constant X R to C(X,R), it's not literally a subset!

#### Heather Macbeth (Mar 09 2021 at 20:26):

Probably an injective homomorphism of algebras.

#### Heather Macbeth (Mar 09 2021 at 20:29):

Maybe you could define a has_coe instance too, so that you can use the map (semi-)silently as a coercion.

#### Eric Wieser (Mar 09 2021 at 20:36):

For reference, docs#linear_map.to_add_monoid_hom and docs#linear_map.to_add_monoid_hom_injective are the types of statement you could make here

#### Eric Wieser (Mar 09 2021 at 20:37):

Where those ones say "linear_maps are a subset of add_monoid_hom"s

Last updated: May 11 2021 at 00:31 UTC