Zulip Chat Archive

Stream: maths

Topic: Unifying `tangent_cone_at` and `pos_tangent_cone_at`


view this post on Zulip Yury G. Kudryashov (Feb 05 2020 at 04:50):

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for tangent_cone_at, and once for pos_tangent_cone_at. I see two ways to unify these definitions:

  1. Introduce (M : submonoid 𝕜) in the definition, and require c n ∈ M. This requires coercions here and there.
  2. Define semifields and normed semifields, then pos_tangent_cone_at becomes tangent_cone_at nnreal.

The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

BTW, is there any technical reason to have module and vector_space instead of always dealing with a semimodule?

view this post on Zulip Johan Commelin (Feb 05 2020 at 07:09):

Re semimodule: No, I don't think so. It's just to create a (useful, I think?) air of familiarity for mathematicians

view this post on Zulip Sebastien Gouezel (Feb 05 2020 at 07:41):

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for tangent_cone_at, and once for pos_tangent_cone_at. I see two ways to unify these definitions:

  1. Introduce (M : submonoid 𝕜) in the definition, and require c n ∈ M. This requires coercions here and there.
  2. Define semifields and normed semifields, then pos_tangent_cone_at becomes tangent_cone_at nnreal.

The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

I would go for the first way: in any case, there will be coercions involved (in the second approach, you would need to see a real module as an nnreal semimodule), so let's keep it as simple as it can be.

view this post on Zulip Sebastien Gouezel (Feb 05 2020 at 07:45):

BTW, is there any technical reason to have module and vector_space instead of always dealing with a semimodule?

I have tried to make module and vector_space all abbreviations for semimodule, but some things became too slow. I still think this is a good move, but it will probably have to wait for Lean 4. Link to the conversation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20maps.20over.20semimodule/near/185824677


Last updated: May 09 2021 at 11:09 UTC