English
Relates the dual of the trace form to a submodule generated by an adjoint subalgebra under separability/integrality hypotheses.
Русский
Связь двойственной формы трасс и подмодуля, порождаемого смежной подалгеброй, при сепарабельности и интегральности.
LaTeX
$$\text{traceForm}_{K,L}^\!*\!\dualmodule = \text{dual-submodule under adjoint}$$
Lean4
theorem traceForm_dualSubmodule_adjoin {x : L} (hx : Algebra.adjoin K { x } = ⊤) (hAx : IsIntegral A x) :
(traceForm K L).dualSubmodule (Subalgebra.toSubmodule (Algebra.adjoin A { x })) =
(aeval x (derivative <| minpoly K x) : L)⁻¹ • (Subalgebra.toSubmodule (Algebra.adjoin A { x })) :=
by
classical
have hKx : IsIntegral K x := Algebra.IsIntegral.isIntegral x
let pb := (Algebra.adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq _ _ hx).trans (Subalgebra.topEquiv))
have pbgen : pb.gen = x := by simp [pb]
have hnondeg : (traceForm K L).Nondegenerate := traceForm_nondegenerate K L
have hpb : ⇑(LinearMap.BilinForm.dualBasis (traceForm K L) hnondeg pb.basis) = _ :=
_root_.funext (traceForm_dualBasis_powerBasis_eq pb)
have : (Subalgebra.toSubmodule (Algebra.adjoin A { x })) = Submodule.span A (Set.range pb.basis) :=
by
rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]
congr; ext y
have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range, pb.basis_eq_pow, pbgen]
simp only [this]
exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩
clear_value pb
conv_lhs => rw [this]
rw [← span_coeff_minpolyDiv hAx, LinearMap.BilinForm.dualSubmodule_span_of_basis _ hnondeg, Submodule.smul_span, hpb]
change _ = Submodule.span A (_ '' _)
simp only [← Set.range_comp, smul_eq_mul, div_eq_inv_mul, pbgen, minpolyDiv_eq_of_isIntegrallyClosed K hAx]
apply le_antisymm <;> rw [Submodule.span_le]
· rintro _ ⟨i, rfl⟩; exact Submodule.subset_span ⟨i, rfl⟩
· rintro _ ⟨i, rfl⟩
by_cases hi : i < pb.dim
· exact Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩
· rw [Function.comp_apply, coeff_eq_zero_of_natDegree_lt, mul_zero]
· exact zero_mem _
rw [← pb.natDegree_minpoly, pbgen, ← natDegree_minpolyDiv_succ hKx, ← Nat.succ_eq_add_one] at hi
exact le_of_not_gt hi
