English
If L is a finite extension of K = Frac(A), where A is a domain, there exists a finite set S in L and a basis B of L over K such that every element of B is integral over A.
Русский
Пусть L — конечное расширение над K = Frac(A), где A — домен. Существуют конечный набор S ⊂ L и база B L над K, такая что каждый элемент B принадлежит интегрально над A.
LaTeX
$$$$\\exists\\, S \\subset L,\\; B \\text{Basis}_K(L) \\text{ with } \\forall b \\in B,\\; IsIntegral_A(b)$$$$
Lean4
/-- If `L` is a finite extension of `K = Frac(A)`,
then `L` has a basis over `A` consisting of integral elements. -/
theorem exists_is_basis_integral : ∃ (s : Finset L) (b : Basis s K L), ∀ x, IsIntegral A (b x) :=
by
letI := Classical.decEq L
letI : IsNoetherian K L := IsNoetherian.iff_fg.2 inferInstance
let s' := IsNoetherian.finsetBasisIndex K L
let bs' := IsNoetherian.finsetBasis K L
obtain ⟨y, hy, his'⟩ := exists_integral_multiples A K (Finset.univ.image bs')
have hy' : algebraMap A L y ≠ 0 :=
by
refine mt ((injective_iff_map_eq_zero (algebraMap A L)).mp ?_ _) hy
rw [IsScalarTower.algebraMap_eq A K L]
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
refine
⟨s',
bs'.map
{
Algebra.lmul _ _ (algebraMap A L
y) with
toFun := fun x => algebraMap A L y * x
invFun := fun x => (algebraMap A L y)⁻¹ * x
left_inv := ?_
right_inv := ?_ },
?_⟩
· intro x; simp only [inv_mul_cancel_left₀ hy']
· intro x; simp only [mul_inv_cancel_left₀ hy']
· rintro ⟨x', hx'⟩
simp only [Algebra.smul_def, Finset.mem_image, Finset.mem_univ, true_and] at his'
simp only [Basis.map_apply, LinearEquiv.coe_mk]
exact his' _ ⟨_, rfl⟩
