English
Let A be a commutative ring, K a field, and L a finite separable extension of K. Suppose b is a K-basis of L with each basis element integral over A and A is integrally closed. Then the range of the A-linear map obtained by restricting scalars from C to A in L lies inside the A-span of the dual basis elements given by the trace form with respect to b.
Русский
Пусть A — коммутативное кольцо, K — поле, L — конечное сепарабельное расширение K. Пусть b — база L над K, при этом каждое её элементарное значение интегрировано над A, и A интегрально замкнуто. Тогда образ линейного отображения, полученного из отображения C в L при ограничении скаляров до A, лежит в A-распространении по двойственной базе, заданной по форме следа относительно b.
LaTeX
$$$$\\operatorname{range}((\\operatorname{Algebra.linearMap} C L).\\restrictScalars A) \\subseteq \\operatorname{span}_A\\bigl(\\operatorname{Set.range}\\bigl((\\operatorname{traceForm}(K,L)).dualBasis(\\operatorname{traceForm_nondegenerate}(K,L))\\, b\\bigr)\\bigr)$$$$
Lean4
theorem range_le_span_dualBasis [Algebra.IsSeparable K L] {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι K L)
(hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
LinearMap.range ((Algebra.linearMap C L).restrictScalars A) ≤
Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) :=
by
rw [← LinearMap.BilinForm.dualSubmodule_span_of_basis, ← LinearMap.BilinForm.le_flip_dualSubmodule, Submodule.span_le]
rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩
simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply, traceForm_apply]
refine Submodule.mem_one.mpr <| IsIntegrallyClosed.isIntegral_iff.mp ?_
exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i))
