exists_integral_multiples
theorem exists_integral_multiples :
∀ (A : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDomain A] [inst_3 : Algebra A K]
[inst_4 : IsFractionRing A K] {L : Type u_4} [inst_5 : Field L] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
[inst_8 : IsScalarTower A K L] [inst_9 : FiniteDimensional K L] (s : Finset L),
∃ y, y ≠ 0 ∧ ∀ x ∈ s, IsIntegral A (y • x)
This theorem, dubbed `exists_integral_multiples`, states that for any finite set `s` of elements `x` in a finite field extension `L` of the field of fractions `K` of an integral domain `A`, there exists a non-zero element `y` in `A` such that the scalar multiple `y • x` is integral over `A` for every `x` in `s`. Here, `y • x` being integral over `A` means that `y • x` is a root of some monic polynomial with coefficients in `A`.
In simpler terms, the theorem states that we can multiply every element of the finite set `s` by some non-zero element to obtain a set of integral elements over `A`.
More concisely: For any finite set of elements in a finite field extension of an integral domain, there exists a non-zero element such that the scalar multiples of each element are integral over the domain.
|
IsIntegralClosure.isNoetherian
theorem IsIntegralClosure.isNoetherian :
∀ (A : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDomain A] [inst_3 : Algebra A K]
[inst_4 : IsFractionRing A K] (L : Type u_4) [inst_5 : Field L] (C : Type u_5) [inst_6 : CommRing C]
[inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra C L]
[inst_11 : IsIntegralClosure C A L] [inst_12 : Algebra A C] [inst_13 : IsScalarTower A C L]
[inst_14 : FiniteDimensional K L] [inst_15 : IsSeparable K L] [inst_16 : IsIntegrallyClosed A]
[inst_17 : IsNoetherianRing A], IsNoetherian A C
The theorem `IsIntegralClosure.isNoetherian` states that for any commutative ring `A`, which is also a Noetherian ring and an integrally closed domain, if `K` is the field of fractions of `A`, and `L` is a field such that `A`, `K` and `L` form a scalar tower, and `C` is the integral closure of `A` in `L`, then `A` and `C` form a Noetherian ring. This theorem also assumes `K` and `L` form a finite dimensional, separable extension. Essentially, this theorem is about the preservation of the Noetherian property under integral closure in a separable, finite dimensional extension.
More concisely: If `A` is a Noetherian, integrally closed domain in a commutative ring, then its integral closure in a finite dimensional, separable extension field forms a Noetherian ring with `A`.
|
FiniteDimensional.exists_is_basis_integral
theorem FiniteDimensional.exists_is_basis_integral :
∀ (A : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDomain A] [inst_3 : Algebra A K]
[inst_4 : IsFractionRing A K] (L : Type u_4) [inst_5 : Field L] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
[inst_8 : IsScalarTower A K L] [inst_9 : FiniteDimensional K L],
∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
The theorem states that for any commutative ring `A` and any field `K`, where `K` is the field of fractions of `A`, if `L` is a finite extension of `K`, then there exists a basis of `L` over `A` that consists entirely of integral elements. Here, an element of an algebra is said to be integral if it is a root of some monic polynomial with coefficients in `A`. The theorem ensures that it is possible to find a basis for `L` where each basis element satisfies this property.
More concisely: Given a commutative ring `A` with field of fractions `K`, for any finite extension `L` of `K`, there exists a basis of `L` over `A` composed entirely of integral elements.
|
IsIntegralClosure.isDedekindDomain
theorem IsIntegralClosure.isDedekindDomain :
∀ (A : Type u_2) (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDomain A] [inst_3 : Algebra A K]
[inst_4 : IsFractionRing A K] (L : Type u_4) [inst_5 : Field L] (C : Type u_5) [inst_6 : CommRing C]
[inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra C L]
[inst_11 : IsIntegralClosure C A L] [inst_12 : Algebra A C] [inst_13 : IsScalarTower A C L]
[inst_14 : FiniteDimensional K L] [inst_15 : IsSeparable K L] [inst_16 : IsDomain C] [inst : IsDedekindDomain A],
IsDedekindDomain C
This theorem states that for any commutative ring `A`, field `K`, and integral domain `C` such that `K` is the field of fractions of `A`, `C` is an integral closure of `A` in a field `L`, and `L` is a finite dimensional separable field extension of `K`, if `A` is a Dedekind domain, then `C` is also a Dedekind domain. In mathematical terms, it signifies that under the given conditions, the property of being a Dedekind domain is preserved upon taking an integral closure.
More concisely: If `A` is a commutative Dedekind domain, `K` is its field of fractions, `C` is an integral closure of `A` in a finite dimensional separable field extension `L` of `K`, then `C` is a Dedekind domain.
|