## Stream: general

### Topic: Making a type a "subtype" of another

#### Noam Atar (Aug 07 2020 at 20:27):

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 (Aug 07 2020 at 20:33):

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 (Aug 07 2020 at 20:34):

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 (Aug 07 2020 at 20:35):

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

#### Noam Atar (Aug 07 2020 at 20:35):

How do I then register it as a coercion?

#### Noam Atar (Aug 07 2020 at 20:36):

Or as a submodule?

#### Mario Carneiro (Aug 07 2020 at 20:36):

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

#### Mario Carneiro (Aug 07 2020 at 20:37):

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 (Aug 07 2020 at 20:37):

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

#### Noam Atar (Aug 07 2020 at 20:43):

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

#### Noam Atar (Aug 07 2020 at 20:43):

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

#### Kevin Buzzard (Aug 08 2020 at 16:36):

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 (Aug 08 2020 at 16:46):

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 (Aug 08 2020 at 16:47):

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

#### Noam Atar (Aug 08 2020 at 20:24):

Thank you!

Last updated: May 08 2021 at 19:11 UTC