Making a type a "subtype" of another

Stream: general

[Noam Atar]

I have created a type of continuous functions with compact support. In mathlib there is a type of bounded continuous functions, and it is shown that they are a normed group, ring, etc.
I would like to show that compact support functions are a substructure of these algebraic structures. What is the right way to do this?
I think the relevant term here is "coercion" but I'm not really sure how to use that properly.

[Mario Carneiro]

You define the type of compact support functions, and then define a function from compact support function to BCF, and register it as a coercion. You will want to prove it preserves a bunch of properties, for example it is a metric embedding, respects addition and so on

[Mario Carneiro]

It might be clearer to start with to not have it be a coercion and just make it a plain function like to_BCF : compact_support A B -> BCF A B

[Sebastien Gouezel]

Or maybe define it as a submodule, to inherit automatically the norm.

[Noam Atar]

How do I then register it as a coercion?

[Noam Atar]

Or as a submodule?

[Mario Carneiro]

instance : has_coe (compact_support A B) (BCF A B) := \<to_BCF\>

[Mario Carneiro]

for the submodule approach you don't have to define the coe as you get that for free with submodule coercing to a type

[Mario Carneiro]

but you will have to prove it's a submodule of course

[Noam Atar]

I see there is a submodule type, but no subalgebra and subring

[Noam Atar]

So should I define it as a module and then prove separately that it is also an algebra and ring using coe?

[Kevin Buzzard]

Just define your functions and and prove that the canonical map between your functions and lean's is an injective ring Hom. You don't have to worry about subtypes at all that way and you will have proved all the results that people will need if they want to use subtypes. We have unbundled subrings but soon we'll have bundled subrings and so subtype code might need to be rewritten

[Yury G. Kudryashov]

Once you define an injective function from continuous functions with compact support to bounded continuous functions and has_zero etc, you can use docs#function.injective.ring to avoid proofs of add_comm etc.

[Yury G. Kudryashov]

You can also use docs#metric_space.induced to get a metric_space instance.

[Noam Atar]

Thank you!