Zulip Chat Archive

Stream: general

Topic: Computable inverse of algebra_map


view this post on Zulip Eric Wieser (Nov 15 2020 at 14:31):

I have a definition of a magnitude function for some specific A, which has signature def magnitude [ring R] [ring A] [algebra R A] : A → (⊥ : subalgebra R A), which is computable.

I'd like to use it to define an inverse function, def inv [field R] [ring A] [algebra R A] (a : A) := (magnitude A)⁻¹ • a.

Unfortunately, this doesn't work because I need the result of magnitude to be R not ⊥ : subalgebra R A. I can get around this with a suitable invocation of docs#classical.choice, but I'd really rather that inv _were_ computable.

My two questions are:

  • Is there an easy way to replace a classical.choice with a decidable instance of some kind, to say "assume there is an algorithm to perform this choice", which allows the caller to actually attempt to provide one?
  • Is there another way to transfer the instancehas_inv R → has_inv (⊥ : subalgebra R A) that is computable?

view this post on Zulip Reid Barton (Nov 15 2020 at 14:37):

First question doesn't seem to make much sense to me because you are basically asking the caller to provide the value you're allegedly constructing

view this post on Zulip Reid Barton (Nov 15 2020 at 14:37):

How do you construct this value magnitude a of type ⊥ : subalgebra R A?

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:39):

Roughly as ⟨f a, (some_lemma a : ∃ r, f a = algebra_map R A r)⟩

view this post on Zulip Reid Barton (Nov 15 2020 at 14:40):

I have no idea what this "magnitude" is supposed to be, but can it be a function from A to R?

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:40):

I can't work out how to define it that way unfortunately. Ideally yes, I would do that

view this post on Zulip Reid Barton (Nov 15 2020 at 14:40):

I think the answer to the second question is no basically by a "lack of imagination" argument ("how could you possibly go about doing it")?

view this post on Zulip Reid Barton (Nov 15 2020 at 14:41):

So I guess the proof of some_lemma is nonconstructive?

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:41):

Honestly I have no idea

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:41):

#print axioms will tell me?

view this post on Zulip Reid Barton (Nov 15 2020 at 14:42):

It's your lemma right? I mean the math proof... what did you do

view this post on Zulip Reid Barton (Nov 15 2020 at 14:42):

If you want stuff to be constructive you need to figure out how to compute it constructively, there are no shortcuts

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:43):

Well in this case, a shortcut would be "find a computable left_inverse of algebra_map via typeclass resolution", especially since we already have docs#ring_hom.injective to prove that there is a left_inverse

view this post on Zulip Eric Wieser (Nov 15 2020 at 14:44):

It's your lemma right? I mean the math proof... what did you do

I used submonoid.induction_on, which I guess pulled in the axiom of choice

view this post on Zulip Reid Barton (Nov 15 2020 at 14:47):

I'm not sure what you are suggesting, do you mean adding a new class whose purpose is to contain these inverses?

view this post on Zulip Reid Barton (Nov 15 2020 at 14:48):

A lot of algebras (e.g. exterior algebras, or more generally connected graded algebras) are augmented

view this post on Zulip Eric Wieser (Nov 15 2020 at 15:00):

I'm suggesting a [has_left_inverse f f_inj]typeclass, which open_locale classical would provide instance for automatically

view this post on Zulip Eric Wieser (Nov 15 2020 at 15:02):

Or perhaps more generally [choosable (∃ r, f a = algebra_map R A r)] which can either be provided by the caller or with classical.choice

view this post on Zulip Reid Barton (Nov 15 2020 at 15:14):

In general this is exactly the sort of thing mathlib tries to avoid, since it's worse to have terms depend on the provenance of these instances than it is for things to be noncomputable


Last updated: May 13 2021 at 21:12 UTC