IsIntegrallyClosed.algebraMap_eq_of_integral
theorem IsIntegrallyClosed.algebraMap_eq_of_integral :
∀ {R : Type u_1} [inst : CommRing R] [iic : IsIntegrallyClosed R] {K : Type u_3} [inst_1 : CommRing K]
[inst_2 : Algebra R K] [ifr : IsFractionRing R K] {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x
The theorem `IsIntegrallyClosed.algebraMap_eq_of_integral` states that for any commutative ring `R` that is integrally closed, and any field of fractions `K` of `R`, if an element `x` in `K` is integral over `R`, then there exists an element `y` in `R` such that `y` maps to `x` under the algebra map from `R` to `K`. In other words, if `R` is integrally closed and `K` is its field of fractions, any element in `K` that is a root of some monic polynomial with coefficients in `R` is actually the image of some element of `R` under the algebra map to `K`.
More concisely: If `R` is an integrally closed commutative ring and `K` is its field of fractions, then every integral element in `K` is the image of some element in `R` under the algebra map from `R` to `K`.
|
IsIntegrallyClosed.isIntegral_iff
theorem IsIntegrallyClosed.isIntegral_iff :
∀ {R : Type u_1} [inst : CommRing R] [iic : IsIntegrallyClosed R] {K : Type u_3} [inst_1 : CommRing K]
[inst_2 : Algebra R K] [ifr : IsFractionRing R K] {x : K}, IsIntegral R x ↔ ∃ y, (algebraMap R K) y = x
This theorem, `IsIntegrallyClosed.isIntegral_iff`, establishes a condition under which an element `x` of a field of fractions `K` of an integrally closed integral domain `R` is integral over `R`. Specifically, an element `x` is integral over `R` if and only if there exists an element `y` in `R` such that the algebraic embedding of `y` into `K` (given by the `algebraMap` function) equals `x`. In other words, `x` is a root of some monic polynomial with coefficients in `R` if and only if `x` can be obtained by embedding some element of `R` into `K`.
More concisely: An element $x$ in the field of fractions $K$ of an integrally closed integral domain $R$ is integral over $R$ if and only if there exists an element $y$ in $R$ such that $x$ is the algebraic image of $y$ in $K$.
|
IsIntegrallyClosed.integralClosure_eq_bot_iff
theorem IsIntegrallyClosed.integralClosure_eq_bot_iff :
∀ {R : Type u_1} [inst : CommRing R] (K : Type u_3) [inst_1 : CommRing K] [inst_2 : Algebra R K]
[ifr : IsFractionRing R K], integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
The theorem `IsIntegrallyClosed.integralClosure_eq_bot_iff` states that for any commutative ring `R` and for any field of fractions `K` of `R`, the integral closure of `R` in `K` is the trivial (or bottom) subalgebra if and only if `R` is integrally closed. Here, a ring is said to be integrally closed if any element in its field of fractions that is integral over the ring is actually an element of the ring.
More concisely: A commutative ring is integrally closed if and only if its integral closure in its field of fractions is the trivial subalgebra.
|
isIntegrallyClosed_iff
theorem isIntegrallyClosed_iff :
∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K], IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x
The theorem states that an integral domain `R` is integrally closed if and only if every integral element of the fraction field `K` of `R` is also an element of `R`. In other words, for every `x` in `K` that is integral over `R`, there exists a `y` in `R` such that the image of `y` under the algebraic embedding from `R` to `K` is `x`. Here, being "integral" means that the element is a root of some monic polynomial with coefficients in `R`, and being "integrally closed" means that every element of `K` that is integral over `R` actually lies in `R`.
More concisely: An integral domain is integrally closed if and only if every element in its fraction field that is integral over it lies in the domain itself.
|
IsIntegralClosure.of_isIntegrallyClosed
theorem IsIntegralClosure.of_isIntegrallyClosed :
∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [iic : IsIntegrallyClosed R]
(K : Type u_3) [inst_2 : CommRing K] [inst_3 : Algebra R K] [ifr : IsFractionRing R K] [inst_4 : Algebra S R]
[inst_5 : Algebra S K] [inst_6 : IsScalarTower S R K], Algebra.IsIntegral S R → IsIntegralClosure R S K
The theorem `IsIntegralClosure.of_isIntegrallyClosed` states that for any three types `R`, `S`, and `K` along with the relevant algebraic structures (where `R` is a commutative ring, `S` is another commutative ring, `K` is a commutative ring that is also an algebra over `R` and `S`, and `R` is the field of fractions of `K`), if `R` is integrally closed, `S` is an integral extension of `R`, and there is a scalar tower `S` `R` `K`, then `S` is the integral closure of `R` in `K`.
In other words, if every element of `S` is integral over `R` and `R` satisfies the property of being integrally closed, then `S` is considered the 'integral closure' of `R` in `K`, meaning it is the smallest algebraic extension of `R` in `K` in which every element is integral over `R`.
More concisely: If `R` is a commutative ring, `S` is an integral extension of `R` with a scalar tower `S` `R` `K`, and `R` is integrally closed, then `S` is the integral closure of `R` in `K`.
|
isIntegrallyClosed_iff_isIntegralClosure
theorem isIntegrallyClosed_iff_isIntegralClosure :
∀ {R : Type u_1} [inst : CommRing R] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K], IsIntegrallyClosed R ↔ IsIntegralClosure R R K
The theorem `isIntegrallyClosed_iff_isIntegralClosure` states that an integral domain `R` is integrally closed if and only if it is the integral closure of itself in its field of fractions `K`. Here, `R` is equipped with a commutative ring structure, and `K` is a field which is also a commutative ring and an algebra over `R`. The term "integrally closed" refers to the property that all integral elements of the field of fractions (denoted as `Frac(R)`) are also elements of `R`. The term "integral closure" refers to the set of all elements in `K` that are integral over `R`. The theorem is saying that these two notions coincide for an integral domain and its field of fractions.
More concisely: An integral domain is integrally closed if and only if it is equal to its integral closure in the field of fractions.
|