Ordered group with zero

Stream: Is there code for X?

[Andrew Yang]

Is there an ordered group-with-zero class that I can put on FractionalIdeal A⁰ K for a dedekind domain A?
In particular I would like the lemma I ≠ 0 → J ≠ 0 → I⁻¹ ≤ J ↔ J⁻¹ ≤ I for free.

[Andrew Yang]

Or maybe 0 < I → 0 < J → I⁻¹ ≤ J ↔ J⁻¹ ≤ I

[Adam Topaz]

I think the answer is no -- we only have linearly ordered groups with zero.

[Yury G. Kudryashov]

While typeclasses like docs#PosMulStrictMono help?

[Yury G. Kudryashov]

(not sure which one of these)

[Alex J. Best]

don't you need fractional ideals here to talk about inverses?

[Yaël Dillies]

Seems like we don't. What algebraic order properties do fractional ideals have? They are a semifield, right?

[Yaël Dillies]

Are they all nonnegative?

[Riccardo Brasca]

Yaël Dillies said:

Seems like we don't. What algebraic order properties do fractional ideals have? They are a semifield, right?

I think they're a semifield, yes.

[Andrew Yang]

I ≠ 0 → J ≠ 0 → I⁻¹ ≤ J ↔ J⁻¹ ≤ I should follow from [OrderedCommMonoid M] [GroupWithZero M]. As for fractional ideals, it is a lattice and a semifield with monotone addition and multiplication and 0 ≤ I for all I.

[Kevin Buzzard]

Fractional ideals are not all <= 1, are they?

[Andrew Yang]

Oops yes of course

[Yaël Dillies]

Are they canonically ordered? A <= B iff exist C, A + C = B

[Yaël Dillies]

If you tell me enough info about them, I will refactor the algebraic order hierarchy so that lemmas apply to them.

[Riccardo Brasca]

I am afraid fractional ideals don't have a lot of nice properties wrt to the sum

[Kevin Buzzard]

I should think that this is true though, isn't it? If A<=B then just set C=B. Yael the simple mental model is additive subgroups of a field, with 1 being the subgroup generated by 1.

[Riccardo Brasca]

Well spotted!

[Yaël Dillies]

That's precisely the argument I had in mind but I wasn't sure whether my mental model of fractional ideals was correct!

[Yaël Dillies]

Then can you prove they are a docs#CanonicallyOrderedAddCommMonoid ?

[Andrew Yang]

Yes:

import Mathlib

variable {A} (K) [CommRing A] [CommRing K] [Algebra A K] (S : Submonoid A)

open FractionalIdeal

instance : CanonicallyOrderedAddCommMonoid (FractionalIdeal S K) where
  add_le_add_left J J' e I := add_le_add_left e I
  exists_add_of_le {I} {J} e := ⟨J, by rwa [← sup_eq_add, right_eq_sup]⟩
  le_self_add I J := by simpa using add_le_add_left (zero_le J) I

I'm not sure if this helps though, since my original question is about the multiplicative structure.

[Yaël Dillies]

Then can you prove they are a docs#CanonicallyOrderedAddCommMonoid ?

[Yaël Dillies]

It should be easy given that we have docs#Submodule.instCanonicallyOrderedAddCommMonoidSubmodule

[Andrew Yang]

Isn't that what I proved above? Or do you mean docs#CanonicallyOrderedCommSemiring?

[Yaël Dillies]

Uh, I sent those messages 50 minutes ago.

[Yaël Dillies]

Yes it would be interesting to know whether they are a CanonicallyOrderedCommSemiring.

[Yaël Dillies]

If they are, then we could consider adding a CanonicallyOrderedSemifield typeclass.

[Andrew Yang]

I believe they are, assuming [IsDomain A]

[Yaël Dillies]

I think I spotted what was wrong with our current theorems. Expect a PR soon.