(Absolute) Discriminant and Different Ideal

Main results

• NumberField.absNorm_differentIdeal: The norm of differentIdeal ℤ 𝒪 is the absolute discriminant.
• NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow: Formula for the absolute discriminant of L in terms of that of K in an extension L/K.
• NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow: Assume that K₁ and K₂ are two linear disjoint number fields with coprime different ideals. Then, the absolute value of the discriminant of their compositum is equal to |discr K₁| ^ [K₂ : ℚ] * |discr K₂| ^ [K₁ : ℚ].

theorem NumberField.absNorm_differentIdeal (K : Type u_1) (𝒪 : Type u_2) [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] [IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] : Ideal.absNorm (differentIdeal ℤ 𝒪) = (discr K).natAbs

theorem NumberField.discr_mem_differentIdeal (K : Type u_1) (𝒪 : Type u_2) [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] [IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] : ↑(discr K) ∈ differentIdeal ℤ 𝒪

theorem NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow (K : Type u_1) (𝒪 : Type u_2) [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] [IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] (L : Type u_3) (𝒪' : Type u_4) [Field L] [NumberField L] [CommRing 𝒪'] [Algebra 𝒪' L] [IsFractionRing 𝒪' L] [IsIntegralClosure 𝒪' ℤ L] [IsDedekindDomain 𝒪'] [CharZero 𝒪'] [Algebra K L] [Algebra 𝒪 𝒪'] [Algebra 𝒪 L] [IsScalarTower 𝒪 K L] [IsScalarTower 𝒪 𝒪' L] [Module.IsTorsionFree 𝒪 𝒪'] [Module.Free ℤ 𝒪'] [Module.Finite ℤ 𝒪'] [Module.Finite 𝒪 𝒪'] : (discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (discr K).natAbs ^ Module.finrank K L

theorem NumberField.isCoprime_differentIdeal_of_isCoprime_discr (L : Type u_3) [Field L] {K₁ : Type u_4} {K₂ : Type u_5} [Field K₁] [NumberField K₁] [Field K₂] [NumberField K₂] [Algebra K₁ L] [Algebra K₂ L] (h : IsCoprime (discr K₁) (discr K₂)) : IsCoprime (Ideal.map (algebraMap (RingOfIntegers K₁) (RingOfIntegers L)) (differentIdeal ℤ (RingOfIntegers K₁))) (Ideal.map (algebraMap (RingOfIntegers K₂) (RingOfIntegers L)) (differentIdeal ℤ (RingOfIntegers K₂)))

theorem NumberField.discr_dvd_discr (K : Type u_1) [Field K] [NumberField K] (L : Type u_3) [Field L] [NumberField L] [Algebra K L] : discr K ∣ discr L

theorem NumberField.linearDisjoint_of_isGalois_isCoprime_discr (L : Type u_3) [Field L] [NumberField L] (K₁ K₂ : IntermediateField ℚ L) [IsGalois ℚ ↥K₁] (h : IsCoprime (discr ↥K₁) (discr ↥K₂)) : K₁.LinearDisjoint ↥K₂

Let K₁ and K₂ be two number fields and assume that K₁/ℚ is Galois. If discr K₁ and discr K₂ are coprime, then they are linear disjoint over ℚ.

theorem NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow (L : Type u_3) [Field L] [NumberField L] (K₁ K₂ : IntermediateField ℚ L) (h₁ : K₁.LinearDisjoint ↥K₂) (h₂ : K₁ ⊔ K₂ = ⊤) (h₃ : IsCoprime (Ideal.map (algebraMap (RingOfIntegers ↥K₁) (RingOfIntegers L)) (differentIdeal ℤ (RingOfIntegers ↥K₁))) (Ideal.map (algebraMap (RingOfIntegers ↥K₂) (RingOfIntegers L)) (differentIdeal ℤ (RingOfIntegers ↥K₂)))) : (discr L).natAbs = (discr ↥K₁).natAbs ^ Module.finrank ℚ ↥K₂ * (discr ↥K₂).natAbs ^ Module.finrank ℚ ↥K₁

Let K₁ and K₂ be two number fields and assume that their different ideals (over ℤ) are coprime. Then, the absolute value of the discriminant of their compositum is equal to |discr K₁| ^ [K₂ : ℚ] * |discr K₂| ^ [K₁ : ℚ].

theorem NumberField.not_dvd_discr_iff_forall_liesOver (K : Type u_1) (𝒪 : Type u_2) [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] {p : ℤ} (hp : Prime p) : ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsMaximal), P.LiesOver (Ideal.span {p}) → Algebra.IsUnramifiedAt ℤ P

Also see not_dvd_discr_iff_forall_mem for a slightly easier to use RHS.

theorem NumberField.not_dvd_discr_iff_forall_mem (K : Type u_1) (𝒪 : Type u_2) [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] {p : ℤ} (hp : Prime p) : ¬p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P

Also see not_dvd_discr_iff_forall_liesOver for a slightly easier to prove RHS.