## Stream: maths

### Topic: Defining has_inv when only some elements have an inverse

#### Anne Baanen (Nov 06 2020 at 11:54):

For fractional ideals, we currently have definitions for docs#ring.fractional_ideal.fractional_ideal_has_div and docs#ring.fractional_ideal.has_inv, defined as I⁻¹ = 1 / I. @Filippo A. E. Nuccio pointed out that has_inv can be confusing, as the notation I⁻¹ in maths typically means the J such that I * J = 1, and this does not exist in general for all fractional ideals I. It just so happens to be equal to 1 / I if such a J exists. Should we change has_inv to take an extra (instance?) parameter stating that all fractional ideals (except 0) are invertible? Or just clarify this in the documentation for fractional_ideal.has_inv?

#### Anne Baanen (Nov 06 2020 at 11:54):

For comparison:

• submodules have a has_div and a 1, but no has_inv
• matrices have a has_inv (which returns 0 for matrices without a two-sided inverse)

#### Johan Commelin (Nov 06 2020 at 12:33):

I'm inclined to just document this...

#### Filippo A. E. Nuccio (Nov 06 2020 at 17:57):

The reason why I am sceptical is that the equation $I * I^{-1} = 1$ is false for non-invertible ideals (without being trivially false, as if it were $0$ by definition).

#### Johan Commelin (Nov 06 2020 at 18:00):

Ok, so if $I^{-1}$ were defined to be equal to 0 for non-invertible ideals? Would that make it better?

#### Filippo A. E. Nuccio (Nov 06 2020 at 18:02):

Well, yes; the problem is that this is in contrast with $I^{-1} = 1/ I$ because for $I = 0$ the submodule $1 / 0$ is, by definition, the whole ambient algebra $K$ , because every element $x \in K$ satisfies $x \cdot 0 \in 1$. On the other hand, for invertible ones, $I^{-1} = 1 / I$ is true. This is why I was suggesting to only introduce inverses for invertible ideals.

#### Johan Commelin (Nov 06 2020 at 18:04):

Right, but what should $(0)^{-1}$ be? It has to be something...

#### Johan Commelin (Nov 06 2020 at 18:05):

One option is to define

inv (I : fractional_ideal) :=
if I * (1 / I) = 1 then 1 / I else 0


#### Johan Commelin (Nov 06 2020 at 18:05):

That way, $I * I^{-1} = 1$ will be trivially false for non-invertible ideals.

#### Filippo A. E. Nuccio (Nov 06 2020 at 18:06):

This is one option; the other, is to define has_inv only for Dedekind domains, where every non-zero is invertible (and your definition would work as it would have a unique exception); and to let is_inv : (fractional_ideal g)-> Prop be simply a property

#### Johan Commelin (Nov 06 2020 at 18:07):

Ok, maybe that's the best option. But it means that for general number rings, we will always have to work with 1 / I instead of $I^{-1}$.

#### Johan Commelin (Nov 06 2020 at 18:07):

And so there will probably be some lemmas that have to be restated.

#### Filippo A. E. Nuccio (Nov 06 2020 at 18:08):

Yes, but this seems OK to me; for instance, the equality $I * 1/J = I / J$ is false when $J$ is not invertible, so I wouldn't push it too far with the notation $I^{-1}$.

#### Johan Commelin (Nov 06 2020 at 18:08):

Ok, let's go with your suggestion.

#### Johan Commelin (Nov 06 2020 at 18:09):

Does this mean that we can also put a group_with_zero instance on fractional_ideal assuming dedekind_domain R?

#### Johan Commelin (Nov 06 2020 at 18:09):

Or is the fact that every nonzero is invertible (assuming DD) not yet in mathlib? (I lost track.)

#### Filippo A. E. Nuccio (Nov 06 2020 at 18:09):

OK, I'll make a PR soon checking that everything is OK both in fractional_ideals, in dedekind_domain and in submodules

#### Filippo A. E. Nuccio (Nov 06 2020 at 18:10):

Johan Commelin said:

Or is the fact that every nonzero is invertible (assuming DD) not yet in mathlib? (I lost track.)

It is almost in mathlib (we are working on this and hope to be done soon). Indeed, the idea would be then to put a group_with_zero structure on the fractional ideals of a DD.

#### Alex J. Best (Nov 06 2020 at 19:07):

Its even a docs#linear_ordered_comm_group_with_zero right? With respect to inclusion? Oh wait inclusion isn't total, so it isn't! Sad

#### Johan Commelin (Nov 06 2020 at 19:11):

I guess we need to create ordered_comm_group_with_zero?

#### Johan Commelin (Nov 06 2020 at 19:11):

Maybe ordered_semifield?

Last updated: May 12 2021 at 08:14 UTC