# Zulip Chat Archive

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