English
For a nonzero fractional ideal I, the submodule underlying its dual equals the traceDual submodule after taking coe.
Русский
Для ненулевого дробного идеала I соответствующая подмодульная дуальность совпадает с traceDual после приведения к подмодулю.
LaTeX
$$coeToSubmodule and traceDual alignment: dual A K I = Iᵛ as submodules.$$
Lean4
/-- The dual of a non-zero fractional ideal is the dual of the submodule under the trace form. -/
noncomputable def dual (I : FractionalIdeal B⁰ L) : FractionalIdeal B⁰ L :=
if hI : I = 0 then 0
else
⟨Iᵛ, by
classical
have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
have ⟨y, hy⟩ :=
(IsIntegralClosure.isIntegral_iff (A := B)).mp (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
· rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, RingHom.map_zero, ← (algebraMap K L).map_zero,
(algebraMap K L).injective.ne_iff]
exact discr_not_zero_of_basis K b
· convert isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
· ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
· rw [Algebra.smul_def, RingHom.map_mul, hy, ← Algebra.smul_def]⟩
