Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Nov 06 2020 at 12:33):

I'm inclined to just document this...

view this post on Zulip Filippo A. E. Nuccio (Nov 06 2020 at 17:57):

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

view this post on Zulip Johan Commelin (Nov 06 2020 at 18:00):

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

view this post on Zulip Filippo A. E. Nuccio (Nov 06 2020 at 18:02):

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

view this post on Zulip Johan Commelin (Nov 06 2020 at 18:04):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 06 2020 at 18:05):

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

view this post on Zulip 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

view this post on Zulip 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 I1I^{-1}.

view this post on Zulip Johan Commelin (Nov 06 2020 at 18:07):

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

view this post on Zulip Filippo A. E. Nuccio (Nov 06 2020 at 18:08):

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

view this post on Zulip Johan Commelin (Nov 06 2020 at 18:08):

Ok, let's go with your suggestion.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:11):

I guess we need to create ordered_comm_group_with_zero?

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:11):

Maybe ordered_semifield?


Last updated: May 12 2021 at 08:14 UTC