[Merged by Bors] - feat: Add exists_ideal_in_class_of_norm_le

[xroblot]

Prove that each class of the classgroup of a number field contains an integral ideal of small norm.

---

• depends on: [Merged by Bors] - feat: Generalize absNorm to fractional ideals #9613
• depends on: [Merged by Bors] - feat: Add Module.Free and Module.Finite instances for ideals #9804
• depends on: [Merged by Bors] - feat: Prove some results on bases of fractional ideals of number fields #9836
• depends on: [Merged by Bors] - feat: Generalize results of CanonicalEmbedding to fractional ideals #9837

[riccardobrasca]

If it's easy can you explicitly add the fact that if the Minkowski bound is less than 2 then the ring is principal?

[xroblot]

If it's easy can you explicitly add the fact that if the Minkowski bound is less than 2 then the ring is principal?

I added

theorem classNumber_eq_one_of_abs_discr_lt
    (h : |discr K| < (2 * (π / 4) ^ NrComplexPlaces K *
      ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) :
    classNumber K = 1 := by

[riccardobrasca]

If it's easy can you explicitly add the fact that if the Minkowski bound is less than 2 then the ring is principal?

I added

theorem classNumber_eq_one_of_abs_discr_lt
    (h : |discr K| < (2 * (π / 4) ^ NrComplexPlaces K *
      ((finrank ℚ K) ^ (finrank ℚ K) / (finrank ℚ K).factorial)) ^ 2) :
    classNumber K = 1 := by

When mathematically trivial consequences are trivial even in Lean is always a good sign!

[riccardobrasca]

@xroblot what is the status of this?

[xroblot]

@xroblot what is the status of this?

I am going to update it with the results of #9210 and fix it so that it compiles. There are still some pieces that need additional work before they find their place in Mathlib (basically everything in the file Sandbox.lean). The two points are the most important:

• First, I think it makes sense to generalise the results of CanonicalEmbedding to fractional ideals and not just integral ideals (as it is the case at the moment in this PR). For this, I opened [Merged by Bors] - feat: Generalize absNorm to fractional ideals #9613.
• Second, I need to add some Module.Free and Module.Finite instances for ideals of number fields that surely fit in a larger scheme. I'll open soon a thread on Zulip to discuss that.

[riccardobrasca]

@xroblot what is the status of this?

I am going to update it with the results of #9210 and fix it so that it compiles. There are still some pieces that need additional work before they find their place in Mathlib (basically everything in the file Sandbox.lean). The two points are the most important:

* First, I think it makes sense to generalise the results of `CanonicalEmbedding` to fractional ideals and not just integral ideals (as it is the case at the moment in this PR). For this, I opened [feat: Generalize absNorm to fractional ideals #9613](https://github.com/leanprover-community/mathlib4/pull/9613).

* Second, I need to add some `Module.Free` and `Module.Finite` instances for ideals of number fields that surely fit in a larger scheme. I'll open soon a thread on Zulip to discuss that.

I've just reviewed #9613, it is almost ready.

The fact that (fractional) ideals are free should follow immediately once we know that they're finite (we know that being torsion free and finite implies free). And finiteness should be very easy, these rings are noetherian. Am I missing something?

[xroblot]

@xroblot what is the status of this?

I am going to update it with the results of #9210 and fix it so that it compiles. There are still some pieces that need additional work before they find their place in Mathlib (basically everything in the file Sandbox.lean). The two points are the most important:

* First, I think it makes sense to generalise the results of `CanonicalEmbedding` to fractional ideals and not just integral ideals (as it is the case at the moment in this PR). For this, I opened [feat: Generalize absNorm to fractional ideals #9613](https://github.com/leanprover-community/mathlib4/pull/9613).

* Second, I need to add some `Module.Free` and `Module.Finite` instances for ideals of number fields that surely fit in a larger scheme. I'll open soon a thread on Zulip to discuss that.

I've just reviewed #9613, it is almost ready.

Thanks. I'll have a look after I am done with the merge.

The fact that (fractional) ideals are free should follow immediately once we know that they're finite (we know that being torsion free and finite implies free). And finiteness should be very easy, these rings are noetherian. Am I missing something?

No, you're right. I was not clear: it is indeed direct to see that ideals of a number field satisfy the instances that I need, what I am not sure about is if I should just add the instances for number fields or for a wider situation (and in this case, what situation?). I will probably need to add at some point an Ideal file in the number field folder for some results specific to (fractional) ideals of number fields. If you think that having the instances only in the specific case of (fractional) ideals of number fields is good enough, then it will be easy. Otherwise, I think some discussion will be necessary.

I am sorry if this is a bit vague, hopefully, it will become a bit clearer once I find the time to write things done more properly.

[xroblot]

For example, right now, I am using the following

import Mathlib.LinearAlgebra.FreeModule.PID
import Mathlib.RingTheory.DedekindDomain.Basic


section Ideal

open Module

variable {R S : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [CommRing S] [IsDomain S]
  [Algebra R S] [Module.Free R S] [Module.Finite R S] (I : Ideal S)

instance : Module.Free R I := by
  by_cases hI : I = ⊥
  · have : Subsingleton I := Submodule.subsingleton_iff_eq_bot.mpr hI
    exact Module.Free.of_subsingleton R I
  · exact Free.of_basis (I.selfBasis (Free.chooseBasis R S) hI)

instance : Module.Finite R I := by
  by_cases hI : I = ⊥
  · have : Subsingleton I := Submodule.subsingleton_iff_eq_bot.mpr hI
    exact IsNoetherian.finite R ↥I
  · exact Finite.of_basis (I.selfBasis (Free.chooseBasis R S) hI)

end Ideal

[riccardobrasca]

Of course we can think about the most general situation, but since the case you need (that is already mathematically interesting) if easy we can just add the instances and think about crazy generalizations later.

[riccardobrasca]

@xroblot I would like to test your branch in the FLTRegular project and for some reason I need the latest mathlib, so I am merging master here.

[riccardobrasca]

@xroblot I would like to test your branch in the FLTRegular project and for some reason I need the latest mathlib, so I am merging master here.

Sorry, ignore my comment.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Generalize absNorm to fractional ideals #9613
• [Merged by Bors] - feat: Add Module.Free and Module.Finite instances for ideals #9804
• [Merged by Bors] - feat: Prove some results on bases of fractional ideals of number fields #9836
• [Merged by Bors] - feat: Generalize results of CanonicalEmbedding to fractional ideals #9837
  By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

This is really great, thanks!

bors d+

[mathlib-bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style