Subset of `structure`

Stream: maths

[Ashvni Narayanan]

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]

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]

Probably an injective homomorphism of algebras.

[Heather Macbeth]

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

[Eric Wieser]

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]

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