# Zulip Chat Archive

## 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 data.padics.padic_integers
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