Zulip Chat Archive

Stream: general

Topic: add_torsor: out_param?

Yury G. Kudryashov (Jun 05 2020 at 05:27):

I'm trying to port analysis/convex to affine spaces. Very often I have to add the vector space as an explicit parameter but convex E s looks strange. Can we use some out_param magic or some other magic to make it work?

Yury G. Kudryashov (Jun 05 2020 at 05:29):

I want to say that every affine space (should we assume the same for add_torsors?) has exactly one vector space behind it.

Johan Commelin (Jun 05 2020 at 05:29):

We used to have out_params in modules, and it was a nightmare. So I'm scared by out_params in general...

Yury G. Kudryashov (Jun 05 2020 at 05:29):

What kind of nightmare?

Yury G. Kudryashov (Jun 05 2020 at 05:30):

I think I was not there yet.

Johan Commelin (Jun 05 2020 at 05:30):

Do we want C\mathbb{C} to be a torsor for C\mathbb{C} and R2\mathbb{R}^2?

Johan Commelin (Jun 05 2020 at 05:30):

Yury G. Kudryashov said:

What kind of nightmare?

Basically, we had the definition of module/vector space, and dimension. And nothing else.

Johan Commelin (Jun 05 2020 at 05:30):

Every time someone tried to do something, you would only get a bunch of errors.

Johan Commelin (Jun 05 2020 at 05:31):

But back then I didn't understand anything of the discussions about out_param.

Yury G. Kudryashov (Jun 05 2020 at 05:31):

Then we'll have to live with convex E s.

Johan Commelin (Jun 05 2020 at 05:33):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Module.20refactor is one thread, but that's not where the story ended

Johan Commelin (Jun 05 2020 at 05:34):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/module.20refactor is another one

Johan Commelin (Jun 05 2020 at 05:39):

But those threads seem to be after the "big" module refactor, which was merged during LUG Freiburg 2018: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/LUG.20Freiburg.202018/near/147245873

Johan Commelin (Jun 05 2020 at 05:39):

I haven't found any zulip threads about the out_param pains that we had before that refactor.

Patrick Massot (Jun 05 2020 at 07:54):

Johan Commelin said:

Do we want C\mathbb{C} to be a torsor for C\mathbb{C} and R2\mathbb{R}^2?

I don't think we want that. We want C\mathbb C to be a R\mathbb R-vector space, but this is different. And convexity is a real notion, even if the vector space EE can be seen as a Q\mathbb Q-vector space, there is no notion of being Q\mathbb Q-convex (you could define something but that doesn't exists in the real world AFAIK). So it should really convex s.

Johan Commelin (Jun 05 2020 at 07:55):

Of course in o-minimal theory ...

Johan Commelin (Jun 05 2020 at 07:56):

Never mind

Johan Commelin (Jun 05 2020 at 07:56):

But I was replying to whether we want the out_param for add_torsor.

Johan Commelin (Jun 05 2020 at 07:56):

And there I think my example applies.

Johan Commelin (Jun 05 2020 at 07:58):

Whether you hardcode the reals into convex is a different question (and one that seems reasonable to me).
(All those o-minimal theorists can generalise later. They first need to get the definition of a definable set into mathlib.)

Yury G. Kudryashov (Jun 05 2020 at 08:10):

The problem is not with hardcoding reals (already done). The problem is in hardcoding the vector space associated to our affine space.

Yury G. Kudryashov (Jun 05 2020 at 08:11):

And I don't know whether we can do it for affine spaces without doing this for additive torsors

Yury G. Kudryashov (Jun 05 2020 at 08:12):

Currently some space is an abbreviation for add torsors

Last updated: Dec 20 2023 at 11:08 UTC