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.

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

Equations

• Submodule.traceDual A K I = let __spread.0 := (Algebra.traceForm K L).dualSubmodule (Submodule.restrictScalars A I); { toAddSubmonoid := __spread.0.toAddSubmonoid, smul_mem' := ⋯ }

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 ∈ Submodule.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 : Submodule B L} {J : Submodule B L} : I ≤ Submodule.traceDual A K J ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.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 : Submodule B L} {J : Submodule B L} {J' : Submodule B L} : I ≤ Submodule.traceDual A K (J * J') ↔ I * J ≤ Submodule.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 : Submodule B L} {J : Submodule B L} : I ≤ Submodule.traceDual A K J ↔ I * J ≤ Submodule.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 : Submodule B L} {J : Submodule B L} : I ≤ Submodule.traceDual A K J ↔ J ≤ Submodule.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 ≤ Submodule.traceDual A K (Submodule.traceDual A K I)

@[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] : Submodule.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] : Submodule.traceDual A K ⊤ = if Submodule.restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 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] [IsSeparable K L] [Decidable (IsField A)] : Submodule.traceDual A K ⊤ = if IsField A then ⊤ else ⊥

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 ∈ Submodule.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] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] : 1 ≤ Submodule.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] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] (I : Submodule B L) {ι : Type u_4} [DecidableEq ι] [Fintype ι] {b : Basis ι K L} (hb : ∀ (i : ι), IsIntegral A (b i)) {a : L} {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ᵛ.

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] [IsDomain A] [IsDomain B] [IsFractionRing A K] [IsFractionRing B L] [NoZeroSMulDivisors A B] (I : Submodule B (FractionRing B)) : Submodule.map (FractionRing.algEquiv B L) (Submodule.traceDual A (FractionRing A) I) = Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L) 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] [IsDomain A] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] (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 traceform.

Equations

• FractionalIdeal.dual A K I = if hI : I = 0 then 0 else ⟨Submodule.traceDual A K ↑I, ⋯⟩

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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : ↑(FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] : ↑(FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] : FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) {x : L} : x ∈ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} : FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} : FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] {I : FractionalIdeal (nonZeroDivisors B) L} {J : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) (hIJ : I * J ≤ 1) : J ≤ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] : 1 ≤ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} {J : FractionalIdeal (nonZeroDivisors B) L} (hJ : J ≠ 0) : I ≤ FractionalIdeal.dual A K J ↔ I * J ≤ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : I⁻¹ ≤ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : (FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : FractionalIdeal.dual A K I = FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} {J : FractionalIdeal (nonZeroDivisors B) L} : FractionalIdeal.dual A K J / FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : FractionalIdeal.dual A K I * I = FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) : I * FractionalIdeal.dual A K I = FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} : FractionalIdeal.dual A K I⁻¹ = FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L) : FractionalIdeal.dual A K (FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} {J : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) (hJ : J ≠ 0) : FractionalIdeal.dual A K I ≤ FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] : Function.Involutive (FractionalIdeal.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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] : Function.Injective (FractionalIdeal.dual A K)

def differentIdeal (A : Type u_1) (B : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] [NoZeroSMulDivisors 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.

Equations

• differentIdeal A B = Submodule.comap (Algebra.linearMap B (FractionRing B)) (1 / Submodule.traceDual A (FractionRing A) 1)

theorem coeSubmodule_differentIdeal_fractionRing (A : Type u_1) (B : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] (hAB : Algebra.IsIntegral A B) [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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] : 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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] : ↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹

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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L} (hI : I ≠ 0) [NoZeroSMulDivisors A B] : ↑(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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [IsFractionRing B L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] {I : Ideal B} (hI : I ≠ ⊥) [NoZeroSMulDivisors A B] : differentIdeal A B ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑(↑I)⁻¹) ≤ 1

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] [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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors 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] [IsDomain B] [IsFractionRing A K] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsDedekindDomain B] [NoZeroSMulDivisors A B] (x : B) (hx : Algebra.adjoin K {(algebraMap B L) x} = ⊤) : (Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ∈ differentIdeal A B