Commit 2025-02-03 10:21 65da8aa1
View on Github →feat: generalize Ideal.spanNorm
to allow non free extensions (#19244)
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