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

Estimated changes