Ideal norm for fractional ideals

Stream: Is there code for X?

[Xavier Roblot]

I don't think we have anything about the (absolute) norm of fractional ideals in Mathlib but maybe someone has done some work on this on the side. I am mostly interested in the analog of docs#Ideal.natAbs_det_basis_change for fractional ideals.

[Andrew Yang]

In FLT-regular we had to generalize ideal norms to non-free B/A, but we had nothing regarding fractional ideals.

[Xavier Roblot]

I have started to work on this and made some progress. So far, I have been able to prove that the norm is multiplicative and generalizes the norm of ideals. Still, I want to make sure that people are okay with two choices I made before going on. First, for the definition of the norm, I used the following:

import Mathlib.RingTheory.FractionalIdeal
import Mathlib.RingTheory.Ideal.Norm

variable {R : Type*} [CommRing R] {K : Type*} [CommRing K] [Algebra R K]

noncomputable section

namespace FractionalIdeal

open scoped Pointwise nonZeroDivisors

section Submonoid

variable {S : Submonoid R} (I : FractionalIdeal S K)

def den : S := ⟨I.2.choose, I.2.choose_spec.1⟩

def num : Ideal R := (I.den • (I : Submodule R K)).comap (Algebra.linearMap R K)

variable [IsDomain R] [Infinite R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R]
  [IsFractionRing R K] (I : FractionalIdeal R⁰ K)

abbrev absNorm : ℚ := (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)|

That is, if I is a fractional ideal, there exists d such that d • I is an ideal and the norm is defined by Norm I = Norm ( d • I) / |Norm d|. I also proved that the norm of I does not depend on the choice of d.

The second choice I made, as can be seen in the above code, is that I decided to restrict to the case of IsFractionRing. The construction could hold in a more general setting but then a lot of hypothesis have to be carried around to prove anything nontrivial like multiplicativity and I am not sure the results would be useful anyway in a larger setting.

[Kevin Buzzard]

I can't see FractionRing anywhere in the above code, only IsFractionRing. What am I doing wrong?

[Xavier Roblot]

Kevin Buzzard said:

I can't see FractionRing anywhere in the above code, only IsFractionRing. What am I doing wrong?

You're right, I meant IsFractionRing. I corrected my message. Thanks!

[Kevin Buzzard]

oh that's great! I thought you were saying "I want to restrict to FractionRing and that would have been a lousy idea in my opinion -- but restricting to IsFractionRing sounds fine -- do you know any applications of this beyond the global field theory? Oh -- wait -- are you restricting to number fields? I'm not sure the function field people will like that...

[Riccardo Brasca]

It looks very reasonable to me. Why Infinite R? CharZero R seems more natural.

[Xavier Roblot]

Riccardo Brasca said:

It looks very reasonable to me. Why Infinite R? CharZero R seems more natural.

I just copied the hypothesis of docs#Ideal.absNorm.

[Xavier Roblot]

Kevin, I think that function fields are included inasmuch as they are included in docs#deal.absNorm

[Alex J. Best]

I forget why we had infinite there :sweat_smile:

[Xavier Roblot]

Alex J. Best said:

I forget why we had infinite there :sweat_smile:

Wait, I thought that Infinite was there for the function field case actually. Am I missing something?

[Kevin Buzzard]

It was [Module.Free ℤ R] that got me worried about the function field case.

[Xavier Roblot]

Kevin Buzzard said:

It was [Module.Free ℤ R] that got me worried about the function field case.

Oh, I see :sweat_smile:

[Alex J. Best]

Yeah I also confused myself! I think originally, we tried to give more general definitions then added some assumptions as we weren't sure what the right definitions should be in complete generality, so ended up in this position.

[Riccardo Brasca]

Module.Free is the reason why I thought about CharZero :D

[Xavier Roblot]

#9613

[Antoine Chambert-Loir]

The definition of the norm looks as it is a particular case of extending a morphism of monoids by localization.

[Riccardo Brasca]

This is probably true, but docs#FractionalIdeal is not defined via localization (it uses #docsIsFractional), so this would require a refactor.

[Xavier Roblot]

It should be relatively easy to define a suitable map docs#Submonoid.LocalizationWithZeroMap to fractional ideals and then using docs#Submonoid.LocalizationWithZeroMap.lift, it should give the construction. I'll give it a try and see what happens.

[Xavier Roblot]

Well, it seems there is a lot of API missing to prove what is needed. So I guess I'll agree with Riccardo that a refactor of FractionalIdeal is needed first.

[Junyan Xu]

I think we can already put a docs#IsLocalization instance on fraction ideals (they form a docs#FractionalIdeal.semifield over the semiring of ideals; we don't seem to have the Algebra instance yet, only docs#FractionalIdeal.coeIdealHom). If we generalize docs#IsFractionRing to semirings then we can put a IsFractionRing instance.