Zulip Chat Archive

Stream: general

Topic: Making a type a "subtype" of another


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Aug 07 2020 at 20:35):

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

view this post on Zulip Noam Atar (Aug 07 2020 at 20:35):

How do I then register it as a coercion?

view this post on Zulip Noam Atar (Aug 07 2020 at 20:36):

Or as a submodule?

view this post on Zulip Mario Carneiro (Aug 07 2020 at 20:36):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 20:37):

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

view this post on Zulip Noam Atar (Aug 07 2020 at 20:43):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Aug 08 2020 at 16:47):

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

view this post on Zulip Noam Atar (Aug 08 2020 at 20:24):

Thank you!


Last updated: May 08 2021 at 19:11 UTC