Zulip Chat Archive

Stream: Is there code for X?

Topic: Ordered group with zero


Andrew Yang (Dec 14 2023 at 22:51):

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 (Dec 14 2023 at 22:52):

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

Adam Topaz (Dec 14 2023 at 22:59):

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

Yury G. Kudryashov (Dec 14 2023 at 23:35):

While typeclasses like docs#PosMulStrictMono help?

Yury G. Kudryashov (Dec 14 2023 at 23:35):

(not sure which one of these)

Alex J. Best (Dec 15 2023 at 02:11):

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

Yaël Dillies (Dec 15 2023 at 07:13):

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

Yaël Dillies (Dec 15 2023 at 07:13):

Are they all nonnegative?

Riccardo Brasca (Dec 15 2023 at 11:47):

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 (Dec 15 2023 at 11:55):

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 (Dec 15 2023 at 12:00):

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

Andrew Yang (Dec 15 2023 at 12:12):

Oops yes of course

Yaël Dillies (Dec 15 2023 at 12:37):

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

Yaël Dillies (Dec 15 2023 at 12:38):

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

Riccardo Brasca (Dec 15 2023 at 13:32):

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

Kevin Buzzard (Dec 15 2023 at 14:47):

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 (Dec 15 2023 at 14:54):

Well spotted!

Yaël Dillies (Dec 15 2023 at 15:15):

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 (Dec 15 2023 at 15:18):

Then can you prove they are a docs#CanonicallyOrderedAddCommMonoid ?

Andrew Yang (Dec 15 2023 at 15:28):

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 (Dec 15 2023 at 16:04):

Then can you prove they are a docs#CanonicallyOrderedAddCommMonoid ?

Yaël Dillies (Dec 15 2023 at 16:04):

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

Andrew Yang (Dec 15 2023 at 16:05):

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

Yaël Dillies (Dec 15 2023 at 16:06):

Uh, I sent those messages 50 minutes ago.

Yaël Dillies (Dec 15 2023 at 16:08):

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

Yaël Dillies (Dec 15 2023 at 16:09):

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

Andrew Yang (Dec 15 2023 at 16:13):

I believe they are, assuming [IsDomain A]

Yaël Dillies (Dec 15 2023 at 16:57):

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

Newell Jensen (Dec 24 2023 at 22:21):

I reached out to Yaël to help out with this and have an initial WIP/draft branch at #9234 which shows that a substantial amount of lemmas from Mathlib.Algebra.Order.Field.Basic can be refactored to Mathlib.Algebra.Order.Ring.Lemmas. Which begs the question if we should have a new typeclass OrderedSemiField that helps organize some of this? The next question then is for the Ring theorists: What are the properties we can expect from fractional ideals?

Andrew Yang (Dec 24 2023 at 23:06):

It is a lattice and a canonically ordered semifield. And that's about it.

Newell Jensen (Dec 24 2023 at 23:27):

By canonical do you mean a PartialOrder? The word canonical is confusing sometimes (at least for me).

Andrew Yang (Dec 24 2023 at 23:27):

It is A <= B iff exist C, A + C = B as discussed above.

Newell Jensen (Dec 24 2023 at 23:28):

Andrew Yang said:

It is A <= B iff exist C, A + C = B as discussed above.

Thanks for verifying.

Newell Jensen (Dec 24 2023 at 23:33):

@Yaël Dillies do you think we should create an OrderedSemifield typeclass that relaxes the linear order of LinearOrderedSemifield to bundle a bunch of these lemmas together?

Yaël Dillies (Dec 25 2023 at 07:18):

@Andrew Yang, the kind of properties we're after are:

  1. 0 ≤ a → b₁ ≤ b₂ → a * b₁ ≤ a * b₂
  2. 0 < a → b₁ < b₂ → a * b₁ < a * b₂
  3. 0 ≤ a → a * b₁ < a * b₂ → b₁ < b₂
  4. 0 < a → a * b₁ ≤ a * b₂ → b₁ ≤ b₂

Yaël Dillies (Dec 25 2023 at 07:19):

Because fractional ideals form a partial order and a semifield, they should all be equivalent.

Andrew Yang (Dec 25 2023 at 07:21):

Doesn't this hold for every CanonicallyOrderedCommSemiring? Anyway it indeed holds in this case.

Yaël Dillies (Dec 25 2023 at 07:22):

Okay great! So it seems fractional ideals really are the first non-linearly ordered semifield mathlib cares about :tada:

Yaël Dillies (Dec 25 2023 at 07:22):

Newell Jensen said:

Yaël Dillies do you think we should create an OrderedSemifield typeclass that relaxes the linear order of LinearOrderedSemifield to bundle a bunch of these lemmas together?

In that case, I would say yes

Kevin Buzzard (Dec 25 2023 at 10:50):

Fractional ideals of the rationals are the nonnegative rationals, with multiplication defined as usual and a+b defined as gcd(a,b) (by which I mean "multiply by some large integer N to make a and b integral, now take gcd, and then divide by N again, and note that this is independent of N". I'm not sure I've ever really internalised that this was a thing before.


Last updated: May 02 2025 at 03:31 UTC