## Stream: general

### Topic: Computable inverse of algebra_map

#### 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?

#### 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

#### Reid Barton (Nov 15 2020 at 14:37):

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

#### Eric Wieser (Nov 15 2020 at 14:39):

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

#### 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?

#### 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

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

#### Reid Barton (Nov 15 2020 at 14:41):

So I guess the proof of some_lemma is nonconstructive?

#### Eric Wieser (Nov 15 2020 at 14:41):

Honestly I have no idea

#### Eric Wieser (Nov 15 2020 at 14:41):

#print axioms will tell me?

#### Reid Barton (Nov 15 2020 at 14:42):

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

#### 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

#### 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

#### 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

#### 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?

#### Reid Barton (Nov 15 2020 at 14:48):

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

#### 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

#### 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

#### 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