The trace different annihilates Kähler differentials

For a finite free extension B / A of integrally closed domains whose fraction-field extension is separable, this file proves

differentIdeal A B ≤ Module.annihilator B Ω[B⁄A].

The proof clears denominators in the trace-dual separability element. If b₁, ..., bₙ is an integral basis with trace-dual basis b₁^dual, ..., bₙ^dual and d lies in the different, then every d bᵢ^dual is integral. Thus

e_d = ∑ i, bᵢ ⊗ d bᵢ^dual

lies in B ⊗[A] B, has product d, and is killed by the kernel of the multiplication map. It follows that multiplication by d sends this kernel into its square, hence kills its cotangent module I / I² = Ω[B⁄A].

noncomputable def BGS.CorvajaZannier.traceSeparabilityElement {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) : TensorProduct K L L

The separability element attached to a basis and its trace-dual basis.

Equations

• BGS.CorvajaZannier.traceSeparabilityElement b = ∑ i : ι, b i ⊗ₜ[K] b.traceDual i

theorem BGS.CorvajaZannier.traceSeparabilityElement_central {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) (x : L) : x ⊗ₜ[K] 1 * traceSeparabilityElement b = 1 ⊗ₜ[K] x * traceSeparabilityElement b

The trace-dual separability element commutes with the two copies of the field extension in the tensor product.

theorem BGS.CorvajaZannier.traceSeparabilityElement_mul {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) : (Algebra.TensorProduct.lmul' K) (traceSeparabilityElement b) = 1

Multiplication sends the trace-dual separability element to one.

theorem BGS.CorvajaZannier.mem_kaehlerAnnihilator_of_separabilityElement {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (d : S) (e : TensorProduct R S S) (hcentral : ∀ (s : S), s ⊗ₜ[R] 1 * e = 1 ⊗ₜ[R] s * e) (hmul : (Algebra.TensorProduct.lmul' R) e = d) : d ∈ Module.annihilator S Ω[S⁄R]

A denominator-cleared separability element with product d proves that d annihilates the relative Kähler differentials.

theorem BGS.CorvajaZannier.differentIdeal_le_kaehlerDifferentialAnnihilator {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra (FractionRing A) (FractionRing B)] [IsScalarTower A (FractionRing A) (FractionRing B)] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [Module.Free A B] : differentIdeal A B ≤ Module.annihilator B Ω[B⁄A]

The trace different is contained in the annihilator of the relative Kähler differentials.

theorem BGS.CorvajaZannier.exists_differentIdeal_generator_mem_kaehlerAnnihilator {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra (FractionRing A) (FractionRing B)] [IsScalarTower A (FractionRing A) (FractionRing B)] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [Module.Free A B] [IsPrincipalIdealRing B] : ∃ (c : B), Ideal.span {c} = differentIdeal A B ∧ c ∈ Module.annihilator B Ω[B⁄A]

In a principal target, a generator of the trace different is also a Kähler-annihilating scalar. This applies to a localized DVR whenever the localized extension is finite free.