Defining `has_inv` when only some elements have an inverse

Stream: maths

[Anne Baanen]

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]

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]

I'm inclined to just document this...

[Filippo A. E. Nuccio]

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]

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]

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]

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

[Johan Commelin]

One option is to define

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

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]

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

[Filippo A. E. Nuccio]

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]

Ok, let's go with your suggestion.

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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]

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]

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]

I guess we need to create ordered_comm_group_with_zero?

[Johan Commelin]

Maybe ordered_semifield?