English
Let A be a commutative ring and L a finite extension with integral closure C in L. If L is a finite separable extension of K = Frac(A) and hb_int holds for a basis b with IsIntegrallyClosed A, then the subalgebra C is contained in the span of the trace-form dual basis elements over A.
Русский
Пусть A — коммутативное кольцо, L — конечное расширение, C — интегральное замыкание A в L. Если L — конечное сепарабельноe расширение над K = Frac(A) и для базиса b выполняются условия hb_int и A интегрально замкнуто, то C содержится в span базиса двойственной формы следа над A.
LaTeX
$$$$\\operatorname{Subalgebra.toSubmodule}(\\text{integralClosure } A L) \\subseteq \\operatorname{span}_A\\bigl(\\operatorname{Set.range}\\bigl((\\operatorname{traceForm}(K,L)).dualBasis(\\operatorname{traceForm_nondegenerate}(K,L))\\, b\\bigr)\\bigr)$$$$
Lean4
theorem integralClosure_le_span_dualBasis [Algebra.IsSeparable K L] {ι : Type*} [Fintype ι] [DecidableEq ι]
(b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
Subalgebra.toSubmodule (integralClosure A L) ≤
Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) :=
by
refine le_trans ?_ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
intro x hx
exact ⟨⟨x, hx⟩, rfl⟩
