English
If L is a finite separable extension and hb_int holds for a basis of L over K with A integrally closed, the integral closure of A in L is contained in the span of the dual-basis elements under the trace form.
Русский
Пусть L — конечное сепарабельноe расширение и hb_int выполняется для базы L над K, при этом A интегрально замкнуто; интегральное замыкание A в L лежит внутри span двойственной базы относительно формы следа.
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
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
Noetherian over `A`. -/
theorem isNoetherian [IsIntegrallyClosed A] [IsNoetherianRing A] : IsNoetherian A C :=
by
haveI := Classical.decEq L
obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
let b' := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
letI := isNoetherian_span_of_finite A (Set.finite_range b')
let f : C →ₗ[A] Submodule.span A (Set.range b') :=
(Submodule.inclusion (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp
((Algebra.linearMap C L).restrictScalars A).rangeRestrict
refine isNoetherian_of_ker_bot f ?_
rw [LinearMap.ker_comp, Submodule.ker_inclusion, Submodule.comap_bot, LinearMap.ker_codRestrict]
exact LinearMap.ker_eq_bot_of_injective (IsIntegralClosure.algebraMap_injective C A L)
