feat: generalize Ideal.spanNorm to allow non free extensions

[riccardobrasca]

We generalize Ideal.spanNorm to allow non-free extensions.

Currently, spanNorm, is defined as

def spanNorm (R : Type*) [CommRing R] {S : Type*} [CommRing S] [Algebra R S] (I : Ideal S) : Ideal R :=
    Ideal.span (Algebra.norm R '' (I : Set S))

but the definition is mathematically meaningless unless [Module.Finite R S] and [Module.Free R S]. We change this to

def spanNorm (R : Type*) [CommRing R] [IsDomain R] {S : Type*} [CommRing S] [IsDomain S]
    [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S]
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) : Ideal R :=
  Ideal.span (Algebra.intNorm R S '' (I : Set S))

that is the mathematically correct definition, notably in the case R and S are the rings of integers in an extension of number fields.

From flt-regular

Co-authored-by: Andrew Yang [email protected]

---

[github-actions]

PR summary bfa197c8cf

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Ideal.Norm.RelNorm	1692	1696	+4 (+0.24%)
Mathlib.RingTheory.Localization.Ideal	1026	1027	+1 (+0.10%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Localization.Ideal	1
Mathlib.RingTheory.Ideal.Norm.RelNorm	4

---

Declarations diff

+ _root_.NoZeroSMulDivisors_of_isLocalization
+ instance [NoZeroSMulDivisors A C] [Module.Finite A C] [IsIntegrallyClosed C] :
+ intNorm_mem_spanNorm
+ map_spanIntNorm
+ spanIntNorm_localization
- map_spanNorm
- spanNorm_localization
- spanNorm_mul_of_field

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[riccardobrasca]

This sequence of have is not very nice. I am open to any suggestion.

[faenuccio]

I have just started the review and have a couple of comments (above), I will dig into the math later on.

[faenuccio]

I might misunderstand the situation, but I would say that this lemma holds without assuming that R_p and S_p are rings, you just need to know that they are localizations of R and S at M and at the image of M (and that M is made of non-zero divisors, of course). No?

[riccardobrasca]

Do you mean I don't need addition? IsLocalization is defined only for semirings.

[faenuccio]

No, what I meant is that I do not think that you need S (and so S_p) to be R-algebras, they only need to be R-modules. I would then expect to use IsLocalizedModule instead of IsLocalization for S_p; but you would need to manually provide the morphism from R to S, and perhaps to ask that the image of M is a monoid and that it satisfies NoZeroSmulDivisors.

I agree this can look a bit strange, but since the conclusion only pertains to the R_p-module structure of S_p, it seems to me that you are only using the algebra structures involved to have nice morphisms (which can be achieved by asking that such morphisms exist), and not because you really need S or S_p to be themselves rings.

[riccardobrasca]

I get the idea, but in practice I don't see a precise statement. If S is not a ring but only an R-module, what is the morphism from R to S? And If S is a ring then any localization as R-module is automatically a ring.

[riccardobrasca]

This new import is needed because of the very recent modification #19376. It seems harmless to import Algebra.Algebra.Tower.

[faenuccio]

In reviewing the main changes (to RelNorm) I agree that the current notion is meaningless if the above algebra is not (finite, and) free over the one below, but adding that everything is integrally closed seems too much. I can very well imagine taking the norm down to Z from a ring that is not a ring of integers (and this is actually very useful if you study orders in number fields). Am I missing something?

[riccardobrasca]

In reviewing the main changes (to RelNorm) I agree that the current notion is meaningless if the above algebra is not (finite, and) free over the one below, but adding that everything is integrally closed seems too much. I can very well imagine taking the norm down to Z from a ring that is not a ring of integers (and this is actually very useful if you study orders in number fields). Am I missing something?

This is because Algebra.intNorm wants it. I agree it is not yet general enough, but I think we can generalize this later (since IsIntegrallyClosed is a class this shouldn't be a pain to do)