Computable inverse of algebra_map

Stream: general

[Eric Wieser]

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?

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

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")?

[Reid Barton]

So I guess the proof of some_lemma is nonconstructive?

[Eric Wieser]

Honestly I have no idea

[Eric Wieser]

#print axioms will tell me?

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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