The different ideal

Main definition

• Submodule.traceDual: The dual L-sub B-module under the trace form.
• FractionalIdeal.dual: The dual fractional ideal under the trace form.
• differentIdeal: The different ideal of an extension of integral domains.

Main results

• conductor_mul_differentIdeal: If L = K[x], with x integral over A, then 𝔣 * 𝔇 = (f'(x)) with f being the minimal polynomial of x.
• aeval_derivative_mem_differentIdeal: If L = K[x], with x integral over A, then f'(x) ∈ 𝔇 with f being the minimal polynomial of x.
• not_dvd_differentIdeal_iff: A prime does not divide the different ideal iff it is unramified (in the sense of Algebra.IsUnramifiedAt).
• differentIdeal_eq_differentIdeal_mul_differentIdeal: Transitivity of the different ideal.

TODO

• Show properties of the different ideal

noncomputable def Submodule.traceDual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] (I : Submodule B L) : Submodule B L

Under the AKLB setting, Iᵛ := traceDual A K (I : Submodule B L) is the Submodule B L such that x ∈ Iᵛ ↔ ∀ y ∈ I, Tr(x, y) ∈ A

theorem Submodule.mem_traceDual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I : Submodule B L} {x : L} : x ∈ traceDual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range

theorem Submodule.le_traceDual_iff_map_le_one {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I J : Submodule B L} : I ≤ traceDual A K J ↔ map (↑A (Algebra.trace K L)) (restrictScalars A (I * J)) ≤ 1

theorem Submodule.le_traceDual_mul_iff {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I J J' : Submodule B L} : I ≤ traceDual A K (J * J') ↔ I * J ≤ traceDual A K J'

theorem Submodule.le_traceDual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I J : Submodule B L} : I ≤ traceDual A K J ↔ I * J ≤ traceDual A K 1

theorem Submodule.le_traceDual_comm {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I J : Submodule B L} : I ≤ traceDual A K J ↔ J ≤ traceDual A K I

theorem Submodule.le_traceDual_traceDual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I : Submodule B L} : I ≤ traceDual A K (traceDual A K I)

@[simp]

theorem Submodule.restrictScalars_traceDual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] {I : Submodule B L} : restrictScalars A (traceDual A K I) = (Algebra.traceForm K L).dualSubmodule (restrictScalars A I)

theorem Submodule.traceDual_span_of_basis (A : Type u_1) {K : Type u_2} {L : Type u} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (I : Submodule B L) {ι : Type u_3} [Finite ι] [DecidableEq ι] (b : Module.Basis ι K L) (hb : restrictScalars A I = span A (Set.range ⇑b)) : restrictScalars A (traceDual A K I) = span A (Set.range ⇑b.traceDual)

If the module I is spanned by the basis b, then its traceDual module is spanned by b.traceDual.

@[simp]

theorem Submodule.traceDual_bot {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] : traceDual A K ⊥ = ⊤

theorem Submodule.traceDual_top' {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] : traceDual A K ⊤ = if restrictScalars A (Algebra.trace K L).range ≤ 1 then ⊤ else ⊥

theorem Submodule.traceDual_top {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Decidable (IsField A)] : traceDual A K ⊤ = if IsField A then ⊤ else ⊥

theorem map_equiv_traceDual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K] [IsDomain A] [IsFractionRing B L] [IsDomain B] [FaithfulSMul A B] (I : Submodule B (FractionRing B)) : Submodule.map (FractionRing.algEquiv B L).toLinearMap (Submodule.traceDual A (FractionRing A) I) = Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L).toLinearMap I)

theorem Submodule.mem_traceDual_iff_isIntegral {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K] [IsIntegrallyClosed A] {I : Submodule B L} {x : L} : x ∈ traceDual A K I ↔ ∀ a ∈ I, IsIntegral A (((Algebra.traceForm K L) x) a)

theorem Submodule.one_le_traceDual_one {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] : 1 ≤ traceDual A K 1

theorem isIntegral_discr_mul_of_mem_traceDual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] (I : Submodule B L) {ι : Type u_4} [DecidableEq ι] [Fintype ι] {b : Module.Basis ι K L} (hb : ∀ (i : ι), IsIntegral A (b i)) {a x : L} (ha : a ∈ I) (hx : x ∈ Submodule.traceDual A K I) : IsIntegral A (Algebra.discr K ⇑b • a * x)

If b is an A-integral basis of L with discriminant b, then d • a * x is integral over A for all a ∈ I and x ∈ Iᵛ.

noncomputable def FractionalIdeal.dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsFractionRing A K] [IsIntegrallyClosed A] [FiniteDimensional K L] [IsIntegralClosure B A L] [Algebra.IsSeparable K L] [IsDomain A] [IsFractionRing B L] [Nontrivial B] [NoZeroDivisors B] (I : FractionalIdeal (nonZeroDivisors B) L) : FractionalIdeal (nonZeroDivisors B) L

The dual of a non-zero fractional ideal is the dual of the submodule under the trace form.

theorem FractionalIdeal.coe_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : ↑(dual A K I) = Submodule.traceDual A K ↑I

@[simp]

theorem FractionalIdeal.coe_dual_one (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] : ↑(dual A K 1) = Submodule.traceDual A K 1

@[simp]

theorem FractionalIdeal.dual_zero (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] : dual A K 0 = 0

theorem FractionalIdeal.mem_dual {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) {x : L} : x ∈ dual A K I ↔ ∀ a ∈ I, ((Algebra.traceForm K L) x) a ∈ (algebraMap A K).range

theorem FractionalIdeal.dual_ne_zero (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : dual A K I ≠ 0

@[simp]

theorem FractionalIdeal.dual_eq_zero_iff {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} : dual A K I = 0 ↔ I = 0

theorem FractionalIdeal.dual_ne_zero_iff {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} : dual A K I ≠ 0 ↔ I ≠ 0

theorem FractionalIdeal.le_dual_inv_aux (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) (hIJ : I * J ≤ 1) : J ≤ dual A K I

theorem FractionalIdeal.one_le_dual_one (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] : 1 ≤ dual A K 1

theorem FractionalIdeal.le_dual_iff (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L} (hJ : J ≠ 0) : I ≤ dual A K J ↔ I * J ≤ dual A K 1

theorem FractionalIdeal.inv_le_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : I⁻¹ ≤ dual A K I

theorem FractionalIdeal.dual_inv_le (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : (dual A K I)⁻¹ ≤ I

theorem FractionalIdeal.dual_eq_mul_inv (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : dual A K I = dual A K 1 * I⁻¹

theorem FractionalIdeal.dual_div_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L} : dual A K J / dual A K I = I / J

theorem FractionalIdeal.dual_mul_self (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : dual A K I * I = dual A K 1

theorem FractionalIdeal.self_mul_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : I * dual A K I = dual A K 1

theorem FractionalIdeal.dual_inv (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} : dual A K I⁻¹ = dual A K 1 * I

@[simp]

theorem FractionalIdeal.dual_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : dual A K (dual A K I) = I

@[simp]

theorem FractionalIdeal.dual_le_dual (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) (hJ : J ≠ 0) : dual A K I ≤ dual A K J ↔ J ≤ I

theorem FractionalIdeal.dual_involutive {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] : Function.Involutive (dual A K)

theorem FractionalIdeal.dual_injective {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] : Function.Injective (dual A K)

theorem FractionalIdeal.trace_mem_dual_one (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [CommRing C] [IsDedekindDomain C] [Field M] [Algebra C M] [IsFractionRing C M] [Algebra A C] [Algebra B C] [Algebra A M] [Algebra B M] [Algebra K M] [Algebra L M] [IsScalarTower A C M] [IsScalarTower A K M] [IsScalarTower B C M] [IsScalarTower B L M] [IsScalarTower K L M] [IsIntegralClosure C A M] [FiniteDimensional K M] [FiniteDimensional L M] [Algebra.IsSeparable K M] (x : M) (hx : x ∈ dual A K 1) : (Algebra.trace L M) x ∈ dual A K 1

theorem FractionalIdeal.smul_mem_dual_one (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [CommRing C] [IsDedekindDomain C] [Field M] [Algebra C M] [IsFractionRing C M] [Algebra A C] [Algebra B C] [Algebra A M] [Algebra B M] [Algebra K M] [Algebra L M] [IsScalarTower A C M] [IsScalarTower A K M] [IsScalarTower B C M] [IsScalarTower B L M] [IsScalarTower K L M] [IsIntegralClosure C A M] [FiniteDimensional K M] [FiniteDimensional L M] [Algebra.IsSeparable K M] [IsIntegralClosure C B M] [Algebra.IsSeparable L M] {x : L} (hx : x ∈ dual A K 1) {y : M} (hy : y ∈ dual B L 1) : x • y ∈ dual A K 1

theorem FractionalIdeal.dual_eq_dual_mul_dual (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsIntegrallyClosed A] [IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [CommRing C] [IsDedekindDomain C] [Field M] [Algebra C M] [IsFractionRing C M] [Algebra A C] [Algebra B C] [Algebra A M] [Algebra B M] [Algebra K M] [Algebra L M] [IsScalarTower A C M] [IsScalarTower A K M] [IsScalarTower B C M] [IsScalarTower B L M] [IsScalarTower K L M] [IsIntegralClosure C A M] [FiniteDimensional K M] [FiniteDimensional L M] [Algebra.IsSeparable K M] [IsIntegralClosure C B M] [Algebra.IsSeparable L M] [Module.IsTorsionFree B C] : dual A K 1 = dual B L 1 * (extendedHomₐ M C) (dual A K 1)

noncomputable def differentIdeal (A : Type u_1) (B : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] : Ideal B

The different ideal of an extension of integral domains B/A is the inverse of the dual of A as an ideal of B. See coeIdeal_differentIdeal and coeSubmodule_differentIdeal.

theorem coeSubmodule_differentIdeal_fractionRing (A : Type u_1) (B : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [FiniteDimensional (FractionRing A) (FractionRing B)] : IsLocalization.coeSubmodule (FractionRing B) (differentIdeal A B) = 1 / Submodule.traceDual A (FractionRing A) 1

theorem coeSubmodule_differentIdeal (A : Type u_1) (K : Type u_2) {L : Type u} (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [IsFractionRing B L] : IsLocalization.coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1

theorem coeIdeal_differentIdeal (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_3) [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [IsFractionRing B L] : ↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹

theorem differentIdeal_ne_bot {A : Type u_1} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] : differentIdeal A B ≠ ⊥

theorem differentialIdeal_le_fractionalIdeal_iff {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : ↑(differentIdeal A B) ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑I⁻¹) ≤ 1

theorem differentialIdeal_le_iff {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [IsFractionRing B L] {I : Ideal B} (hI : I ≠ ⊥) : differentIdeal A B ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑(↑I)⁻¹) ≤ 1

theorem differentIdeal_eq_differentIdeal_mul_differentIdeal (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (C : Type u_3) [IsDomain B] [CommRing C] [Algebra B C] [Algebra A C] [IsDedekindDomain C] [Module.Finite A B] [Module.Finite A C] [Module.Finite B C] [Module.IsTorsionFree A C] [Module.IsTorsionFree B C] [IsScalarTower A B C] [Algebra.IsSeparable (FractionRing A) (FractionRing C)] : differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)

Transitivity of the different ideal.

theorem traceForm_dualSubmodule_adjoin (A : Type u_1) (K : Type u_2) {L : Type u} [CommRing A] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] {x : L} (hx : Algebra.adjoin K {x} = ⊤) (hAx : IsIntegral A x) : (Algebra.traceForm K L).dualSubmodule (Subalgebra.toSubmodule (Algebra.adjoin A {x})) = ((Polynomial.aeval x) (Polynomial.derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (Algebra.adjoin A {x})

theorem conductor_mul_differentIdeal (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤) : conductor A x * differentIdeal A B = Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}

theorem aeval_derivative_mem_differentIdeal (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (x : B) (hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤) : (Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ∈ differentIdeal A B

theorem pow_sub_one_dvd_differentIdeal_aux (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] {p : Ideal A} [p.IsMaximal] (P : Ideal B) {e : ℕ} (he : e ≠ 0) (hp : p ≠ ⊥) (hP : P ^ e ∣ Ideal.map (algebraMap A B) p) : P ^ (e - 1) ∣ differentIdeal A B

theorem pow_sub_one_dvd_differentIdeal (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (hp : p ≠ ⊥) (hP : P ^ e ∣ Ideal.map (algebraMap A B) p) : P ^ (e - 1) ∣ differentIdeal A B

theorem not_dvd_differentIdeal_of_intTrace_not_mem (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} (P Q : Ideal B) (hP : P * Q = Ideal.map (algebraMap A B) p) (x : B) (hxQ : x ∈ Q) (hx : (Algebra.intTrace A B) x ∉ p) : ¬P ∣ differentIdeal A B

theorem not_dvd_differentIdeal_of_isCoprime_of_isSeparable (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (P Q : Ideal B) [P.IsMaximal] [P.LiesOver p] (hPQ : IsCoprime P Q) (hP : P * Q = Ideal.map (algebraMap A B) p) [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)] : ¬P ∣ differentIdeal A B

theorem not_dvd_differentIdeal_of_isCoprime (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] [Finite (A ⧸ p)] (P Q : Ideal B) [P.IsMaximal] (hPQ : IsCoprime P Q) (hP : P * Q = Ideal.map (algebraMap A B) p) : ¬P ∣ differentIdeal A B

theorem dvd_differentIdeal_of_not_isSeparable (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal] (hp : p ≠ ⊥) (P : Ideal B) [P.IsMaximal] [P.LiesOver p] (H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)) : P ∣ differentIdeal A B

theorem not_dvd_differentIdeal_iff {A : Type u_1} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] : ¬P ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A P

A prime does not divide the different ideal iff it is unramified.

theorem dvd_differentIdeal_iff {A : Type u_1} {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] : P ∣ differentIdeal A B ↔ ¬Algebra.IsUnramifiedAt A P

A prime divides the different ideal iff it is ramified.