Algebra.finite_iff_isIntegral_and_finiteType
theorem Algebra.finite_iff_isIntegral_and_finiteType :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A
This theorem states that, for any given types `R` and `A` which are commutative rings, and `A` is an algebra over `R`, a module `A` is finite over the ring `R` if and only if `A` is an integral algebra over `R` and `A` is of finite type over `R`. Here, an algebra `A` is said to be integral over `R` if every element of the extension `A` is integral over the base ring `R`, and `A` is said to be of finite type over `R` if it is generated by a finite set of elements from `R`.
More concisely: A commutative `R`-algebra `A` is finite as an `R`-module if and only if it is integral and of finite type over `R`.
|
fg_adjoin_of_finite
theorem fg_adjoin_of_finite :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
s.Finite → (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
The theorem `fg_adjoin_of_finite` states that for every commutative ring `R`, a commutative ring `A`, and a set `s` of `A`, if `s` is finite and every element `x` in `s` is integral over `R`, then the submodule obtained by applying the function `Subalgebra.toSubmodule` to the subalgebra generated by `s` over `R` (represented as `Algebra.adjoin R s`) is finitely generated. In other words, this theorem states that the subalgebra formed by adjoining a finite set of integral elements to a commutative ring forms a finitely generated submodule.
More concisely: If `R` is a commutative ring, `A` is a commutative `R`-algebra, and `s` is a finite set of elements in `A` integral over `R`, then the submodule of `A` generated by `s` is finitely generated.
|
Algebra.IsIntegral.trans
theorem Algebra.IsIntegral.trans :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R A B],
Algebra.IsIntegral R A → Algebra.IsIntegral A B → Algebra.IsIntegral R B
The theorem `Algebra.IsIntegral.trans` states that if you have two algebra extensions R → A → B (where R, A and B denote Commutative rings), such that A is an R-algebra and all of its elements are integral over R, and B is an A-algebra and all of its elements are integral over A, then all elements of B are also integral over R. That is, integrality is transitive over the tower of field extensions R → A → B. This theorem is under the assumption that R, A, and B form a scalar tower, which means the actions of multiplication by scalars in these algebras are compatible.
More concisely: If R ⇒ A ⇒ B is a scalar tower of commutative ring extensions with A and B being integral over R, then B is integral over R.
|
IsIntegral.of_mem_closure'
theorem IsIntegral.of_mem_closure' :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (G : Set A),
(∀ x ∈ G, IsIntegral R x) → ∀ x ∈ Subring.closure G, IsIntegral R x
This theorem, `IsIntegral.of_mem_closure'`, states that for any set `G` of elements `x` from an algebra `A` over a commutative ring `R`, if every element in `G` is integral over `R` (i.e., each element is a root of some monic polynomial with coefficients in `R`), then every element `x` in the subring generated by `G` (i.e., the smallest subring of `A` containing `G`) is also integral over `R`. This can be interpreted as a generalization of the `IsIntegral.of_mem_closure` theorem.
More concisely: If every element in a set `G` of an algebra `A` over a commutative ring `R` is integral over `R`, then every element in the subring generated by `G` is also integral over `R`.
|
isIntegral_algebraMap
theorem isIntegral_algebraMap :
∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : R},
IsIntegral R ((algebraMap R A) x)
The theorem `isIntegral_algebraMap` asserts that for any commutative ring `R`, ring `A`, and algebra structure from `R` to `A`, any element `x` from `R` is integral over `R` when it is mapped to `A` using the algebra map. In other words, if you take any element from the commutative ring `R`, and map it into the ring `A` using the mapping defined by the algebra structure between `R` and `A`, the resulting element in `A` will always be a root of some monic polynomial `p : R[X]`.
More concisely: For any commutative rings R and A, and algebra structure from R to A, every element x in R is integral over R if and only if its image in A is a root of some monic polynomial in R[X].
|
RingHom.Finite.of_isIntegral_of_finiteType
theorem RingHom.Finite.of_isIntegral_of_finiteType :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
f.IsIntegral → f.FiniteType → f.Finite
This theorem states that for any two types `R` and `S` which are both commutative rings, and a ring homomorphism `f` from `R` to `S`, if `f` is integral and of finite type, then `f` is finite. In mathematical terms, given a ring homomorphism between two commutative rings, if it maps to an element that is a root of some monic polynomial (i.e., it's integral), and if it's of finite type (it maps to a ring that is finitely generated as an algebra), then it's finite (the ring it maps to is finitely generated as a module), which is a stronger condition.
More concisely: If `f` is a commutative ring homomorphism from a commutative ring `R` to `S`, is integral and of finite type, then `S` is a finitely generated `R`-module.
|
RingHom.IsIntegral.of_finite
theorem RingHom.IsIntegral.of_finite :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Finite → f.IsIntegral
The theorem `RingHom.IsIntegral.of_finite` states that for any commutative rings `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, if `f` is finite, then `f` is integral. Here, a ring homomorphism `f` is said to be *finite* if the induced ring `S` is finitely-generated as an `R`-algebra via `f`. It is said to be *integral* if each element of `S` is integral over `R` with respect to `f`, meaning it's a root of some monic polynomial with coefficients in `R`.
More concisely: If `R` and `S` are commutative rings, and `f` is a finite ring homomorphism from `R` to `S`, then every element of `S` is integral over `R` with respect to `f`.
|
RingHom.isIntegral_of_surjective
theorem RingHom.isIntegral_of_surjective :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
Function.Surjective ⇑f → f.IsIntegral
This theorem states that for any two types `R` and `S` which are both commutative rings, if a ring homomorphism `f` from `R` to `S` is surjective (meaning that every element of `S` is the image of some element of `R` under `f`), then `f` is integral. In other words, every element of `S` is integral with respect to the map `f`. In mathematical terms, this theorem states that if every element of a commutative ring `S` is the image of an element of another commutative ring `R` under a ring homomorphism `f`, then every element of `S` satisfies a polynomial equation with coefficients in `R` via `f`.
More concisely: If `f` is a surjective ring homomorphism from a commutative ring `R` to another commutative ring `S`, then every element of `S` is integral over `R` via `f`.
|
IsIntegral.add
theorem IsIntegral.add :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y : A},
IsIntegral R x → IsIntegral R y → IsIntegral R (x + y)
The theorem `IsIntegral.add` states that for any commutative ring `R` and any commutative ring `A` with an algebra structure over `R`, if elements `x` and `y` of `A` are both integral over `R`, then their sum `x + y` is also integral over `R`. In other words, the property of being integral is preserved under the operation of addition.
More concisely: If `R` is a commutative ring, `A` is a commutative `R`-algebra, and `x` and `y` are integral elements of `A` over `R`, then `x + y` is also integral over `R`.
|
IsIntegralClosure.isIntegral
theorem IsIntegralClosure.isIntegral :
∀ (R : Type u_1) {A : Type u_2} (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] [inst_6 : Algebra R A]
[inst_7 : IsScalarTower R A B] (x : A), IsIntegral R x
The theorem `IsIntegralClosure.isIntegral` states that for any type `R` which is a commutative ring, any type `A` which is a commutative ring, and any type `B` which is a commutative ring, if `A` is an integral closure of `R` in `B`, then for every element `x` of type `A`, `x` is integral over `R`. This means that `x` is a root of some monic polynomial with coefficients in `R`. The structures `[inst_3 : Algebra R B]`, `[inst_4 : Algebra A B]`, `[inst_6 : Algebra R A]` and `[inst_7 : IsScalarTower R A B]` ensure the algebraic structure needed to define integral elements and the integral closure.
More concisely: If `A` is the integral closure of `R` in `B`, then every element `x` in `A` is integral over `R`.
|
IsIntegral.of_mem_of_fg
theorem IsIntegral.of_mem_of_fg :
∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
(Subalgebra.toSubmodule S).FG → ∀ x ∈ S, IsIntegral R x
The theorem `IsIntegral.of_mem_of_fg` states that if `S` is a sub-algebra of an algebra `A` over a commutative ring `R`, and `S` is finitely generated as an `R`-module, then every element `x` of `S` is an integral element over `R`. In other words, for any `x` in `S`, there exists a monic polynomial `p` in `R[X]` such that `x` is a root of `p`. This is equivalent to saying that each element `x` in `S` is integral with respect to the induced `algebraMap` from `R` to `A`.
More concisely: If `S` is a finitely generated sub-algebra of a commutative ring `R` and an `R`-algebra `A`, then every element in `S` is integral over `R`.
|
RingHom.IsIntegral.trans
theorem RingHom.IsIntegral.trans :
∀ {R : Type u_1} {S : Type u_4} {T : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
(f : R →+* S) (g : S →+* T), f.IsIntegral → g.IsIntegral → (g.comp f).IsIntegral
The theorem `RingHom.IsIntegral.trans` states that given three commutative rings `R`, `S`, and `T`, and two ring homomorphisms `f : R →+* S` and `g : S →+* T`, if `f` is integral (every element in `S` is integral with respect to `f`) and `g` is integral (every element in `T` is integral with respect to `g`), then the composition of `g` and `f` is also integral (every element in `T` is integral with respect to the composition of `g` and `f`). In other words, the integrality property of ring homomorphisms is preserved under composition.
More concisely: If homomorphisms `f : R → S` and `g : S → T` are integral, then their composition `g ∘ f : R → T` is also integral.
|
isField_of_isIntegral_of_isField
theorem isField_of_isIntegral_of_isField :
∀ {R : Type u_6} {S : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
Algebra.IsIntegral R S → Function.Injective ⇑(algebraMap R S) → IsField S → IsField R
The theorem `isField_of_isIntegral_of_isIntegral_of_isField` states that given two types `R` and `S`, where both `R` and `S` are commutative rings and `S` is an algebra over `R`, if the algebra extension from `R` to `S` is integral, and the algebra morphism (which maps elements from `R` to `S`) is injective, and `S` is a field, then `R` is also a field. In other words, if every element of `S` is integral over `R`, and there are no different elements in `R` mapped to the same element in `S` under the algebra map, and `S` contains multiplicative inverses for all non-zero elements, then `R` must also contain multiplicative inverses for all its non-zero elements, i.e., `R` is also a field.
More concisely: If `R` is a commutative ring, `S` is an algebra over `R` with an integral extension and injective algebra morphism, and `S` is a field, then `R` is also a field.
|
IsIntegral.fg_adjoin_singleton
theorem IsIntegral.fg_adjoin_singleton :
∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
IsIntegral R x → (Subalgebra.toSubmodule (Algebra.adjoin R {x})).FG
The theorem `IsIntegral.fg_adjoin_singleton` states that for any commutative ring `R`, a ring `B`, and an algebra structure over `B` with coefficients in `R`, if an element `x` of `B` is integral over `R`, then the submodule generated by adjoining `x` to `R` is finitely generated. In other words, if `x` is a root of some monic polynomial with coefficients in `R`, then the smallest subalgebra of `B` that contains both `R` and `x` can be written as the span of a finite subset of `B`.
More concisely: If `x` is an element integral over a commutative ring `R` in an algebra structure over another ring `B`, then the subalgebra of `B` generated by `R` and `x` is finitely generated.
|
IsIntegral.smul
theorem IsIntegral.smul :
∀ {B : Type u_3} {S : Type u_4} [inst : Ring B] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : CommRing S]
[inst_3 : Algebra R B] [inst_4 : Algebra S B] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S B] {x : B}
(r : R), IsIntegral S x → IsIntegral S (r • x)
The theorem `IsIntegral.smul` states that for any types `B`, `S` and `R`, assuming `B` is a ring, `R` is a commutative semiring, and `S` is a commutative ring. Moreover, we have defined the algebra structures from `R` to `B`, from `S` to `B` and from `R` to `S`, and that these algebra structures form a scalar tower (meaning, the scalar multiplication is compatible over these rings). Then given an element `x` of `B`, and another element `r` of `R`, if `x` is integral over `S`, then the scalar multiple, `r • x`, is also integral over `S`. In other words, given an element of an algebra that is a root of some monic polynomial, multiplying this element by a scalar from the underlying ring results in another element that is also a root of some monic polynomial.
More concisely: If `x` is an integral element of the commutative ring `B` over the commutative ring `S`, then for any scalar `r` in the commutative semiring `R` with compatible algebra structures to `B` and `S`, the scalar multiple `r • x` is also an integral element of `S`.
|
IsIntegral.mul
theorem IsIntegral.mul :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y : A},
IsIntegral R x → IsIntegral R y → IsIntegral R (x * y)
The theorem `IsIntegral.mul` states that for any commutative ring `R` and for any commutative ring `A` equipped with a ring homomorphism from `R` to `A` (i.e., `A` is an `R`-algebra), if elements `x` and `y` of `A` are both integral over `R`, then their product `x * y` is also integral over `R`. In mathematical terms, this means that if `x` and `y` are roots of some monic polynomial with coefficients from `R`, then their product is also a root of some monic polynomial with coefficients from `R`.
More concisely: If `R` is a commutative ring and `A` is an `R`-algebra with `x` and `y` in `A` being integral over `R`, then their product `x * y` is also integral over `R`. Alternatively, if `x` and `y` are roots of monic polynomials with coefficients from `R`, then their product is a root of a monic polynomial with coefficients from `R`.
|
RingHom.isIntegralElem_map
theorem RingHom.isIntegralElem_map :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] (f : R →+* S) {x : R},
f.IsIntegralElem (f x)
The theorem `RingHom.isIntegralElem_map` states that for any types `R` and `S`, given the preconditions that `R` is a commutative ring and `S` is a ring, and given a ring homomorphism `f` from `R` to `S` and an element `x` from `R`, then the image of `x` under `f` is integral over `R` with respect to `f`. In terms of algebra, this means that there exists a monic polynomial `p` over `R` such that when `p` is evaluated at the image of `x` under `f`, the result is zero.
More concisely: For any commutative rings R and S, ring homomorphism f : R -> S, and element x in R, the image of x under f is integral over R with respect to f, i.e., there exists a monic polynomial p(t) in R[t] such that p(f(x)) = 0.
|
Algebra.IsIntegral.of_finite
theorem Algebra.IsIntegral.of_finite :
∀ (R : Type u_1) (B : Type u_3) [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B]
[inst_3 : Module.Finite R B], Algebra.IsIntegral R B
The theorem `Algebra.IsIntegral.of_finite` states that for any commutative ring `R` and any ring `B`, where `B` is an `R`-algebra and is also a finite `R`-module, every element of `B` is integral over `R`. In other words, if `B` is a finite extension of `R` as an algebra, then every element in `B` satisfies a monic polynomial equation with coefficients in `R` (which is the definition of being "integral").
More concisely: If `R` is a commutative ring and `B` is an `R`-algebra that is also a finite `R`-module, then every element in `B` is integral over `R`.
|
IsIntegral.tower_bot
theorem IsIntegral.tower_bot :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R A B],
Function.Injective ⇑(algebraMap A B) → ∀ {x : A}, IsIntegral R ((algebraMap A B) x) → IsIntegral R x
The theorem `IsIntegral.tower_bot` states that if we have an algebra tower `R → A → B` where the mapping `A → B` is injective, then if the entire tower `R → B` is an integral extension, the sub-extension `R → A` is also integral. Here, an algebra tower is a sequence of algebraic structures where each one is an algebra over the previous one, an integral extension is a ring extension where every element of the larger ring is a root of some monic polynomial with coefficients in the smaller ring, and injective refers to a function that preserves distinctness: distinct inputs produce distinct outputs.
More concisely: If `R → A → B` is an algebra tower with injective `A → B` and `R → B` is an integral extension, then `R → A` is an integral extension.
|
IsIntegralClosure.algebraMap_lift
theorem IsIntegralClosure.algebraMap_lift :
∀ {R : Type u_1} (A : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] {S : Type u_4}
[inst_6 : CommRing S] [inst_7 : Algebra R S] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R S B]
[inst_10 : Algebra R A] [inst_11 : IsScalarTower R A B] (h : Algebra.IsIntegral R S) (x : S),
(algebraMap A B) ((IsIntegralClosure.lift A B h) x) = (algebraMap S B) x
The theorem, `IsIntegralClosure.algebraMap_lift`, states that for all types `R`, `A`, `B`, and `S` with certain properties and relations (specifically, `R`, `A`, `B`, and `S` being types of commutative rings having algebra structures, and `B` being an integral closure of `A` in `R`, with `R`, `A`, and `S` being scalar towers over `B`), if all elements of `S` are integral over `R`, then for any element `x` of `S`, the algebraic mapping of the lift of `x` from `A` to `B` is equal to the algebraic mapping of `x` from `S` to `B`.
In other words, lifting `x` to the integral closure and then applying the algebraic mapping results in the same value as directly applying the algebraic mapping to `x`.
More concisely: For any commutative rings `R`, `A`, `B`, and `S` with algebra structures, if `B` is the integral closure of `A` in `R`, `R`, `A`, and `S` are scalar towers over `B`, and all elements of `S` are integral over `R`, then for any `x` in `S`, the algebraic mapping of the lift of `x` from `A` to `B` equals the algebraic mapping of `x` from `S` to `B`.
|
RingHom.finite_iff_isIntegral_and_finiteType
theorem RingHom.finite_iff_isIntegral_and_finiteType :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
f.Finite ↔ f.IsIntegral ∧ f.FiniteType
The theorem `RingHom.finite_iff_isIntegral_and_finiteType` states that for any commutative rings `R` and `S`, and a ring homomorphism `f` from `R` to `S`, `f` is finite if and only if `f` is integral and `f` is of finite type. In other words, a ring homomorphism between two commutative rings is finite exactly when it satisfies two properties: being integral, i.e., being a root of some monic polynomial, and being of finite type, i.e., generated by a finite set.
More concisely: A ring homomorphism between commutative rings is finite if and only if it is integral and of finite type.
|
Algebra.IsIntegral.finite
theorem Algebra.IsIntegral.finite :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
Algebra.IsIntegral R A → ∀ [h' : Algebra.FiniteType R A], Module.Finite R A
The theorem `Algebra.IsIntegral.finite` addresses the Kurosh problem, asking whether every element of an algebra extension is integral over the base ring, even when the algebra extension is not necessarily commutative and the base ring is a field. The theorem states that for any commutative rings `R` and `A`, and `A` being an algebra over `R`, if `A` is an integral algebra over `R`, and `A` is of finite type over `R`, then `A` is finite dimensional over `R`. Note, however, the Kurosh problem was solved in the negative, and criteria for a finitely generated algebraic (or integral) algebra over a field to be finite dimensional are provided in the referenced paper (https://arxiv.org/pdf/1706.02383.pdf).
More concisely: If `R` is a commutative ring, `A` is a finite type algebra over `R` that is integral over `R`, then `A` is finite dimensional over `R`.
|
isIntegral_leadingCoeff_smul
theorem isIntegral_leadingCoeff_smul :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (p : Polynomial R) (x : S)
[inst_2 : Algebra R S], (Polynomial.aeval x) p = 0 → IsIntegral R (p.leadingCoeff • x)
The theorem `isIntegral_leadingCoeff_smul` states that for any given polynomial `p` of type `R[X]` and a root `x` of type `S`, if `x` is a root of the polynomial (i.e., `(Polynomial.aeval x) p = 0`), then the scaled version of `x` by the leading coefficient of the polynomial, denoted as `p.leadingCoeff • x`, is integral over `R`. Here, being "integral" means that the scaled root is itself a root of some monic polynomial with coefficients in `R`.
More concisely: If a root x of polynomial p in R[X] satisfies (Polynomial.aeval x) p = 0, then p.leadingCoeff * x is a root of some monic polynomial in R[X].
|
isIntegral_algebraMap_iff
theorem isIntegral_algebraMap_iff :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B] {x : A},
Function.Injective ⇑(algebraMap A B) → (IsIntegral R ((algebraMap A B) x) ↔ IsIntegral R x)
This theorem states that for any commutative rings `R` and `A`, and any ring `B`, where `A` and `B` are algebras over `R` and `A` is an algebra over `B` forming a scalar tower, given any element `x` from `A`, if the algebra map from `A` to `B` is injective, then `x` is integral over `R` with respect to the induced algebra map from `A` to `B` if and only if `x` is integral over `R`. In other words, an element is integral over `R` via the algebra map from `A` to `B` if and only if it is integral over `R` directly, given that the algebra map is injective.
More concisely: For commutative rings R, A, and B, where A and B are algebras over R with A an algebra over B forming a scalar tower, if the algebra map from A to B is injective, then an element x in A is integral over R with respect to this map if and only if x is integral over R directly.
|
isIntegral_algHom_iff
theorem isIntegral_algHom_iff :
∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
Function.Injective ⇑f → ∀ {x : A}, IsIntegral R (f x) ↔ IsIntegral R x
The theorem `isIntegral_algHom_iff` has the following statement:
For all commutative rings `R`, rings `A` and `B`, and algebras `A` and `B` over `R`, suppose `f` is an algebra homomorphism from `A` to `B`. If the function `f` is injective, then for any element `x` in `A`, `x` is integral over `R` if and only if the image of `x` under `f` is integral over `R`. In other words, the property of being integral is preserved under the action of an injective algebra homomorphism.
More concisely: If `f` is an injective algebra homomorphism between commutative rings `R`, algebras `A` and `B`, then for all `x` in `A`, `x` is integral over `R` if and only if the image of `x` under `f` is integral over `R`.
|
isIntegral_zero
theorem isIntegral_zero :
∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B], IsIntegral R 0 := by
sorry
This theorem states that for any algebra `B` over a commutative ring `R`, the element `0` is always integral over `R`. In other words, `0` is a root of some monic polynomial with coefficients in `R`. This property holds irrespective of the specific structures of the commutative ring `R` and the algebra `B`.
More concisely: For any commutative ring R and algebra B over R, the element 0 in B is integral over R.
|
IsIntegral.algebraMap
theorem IsIntegral.algebraMap :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B] {x : A},
IsIntegral R x → IsIntegral R ((algebraMap A B) x)
The theorem `IsIntegral.algebraMap` states that for any commutative rings `R` and `A`, a ring `B`, and algebras over `R` of `A` and `B`, as well as an algebra over `A` of `B`, if the algebra structures form a scalar tower, then any element `x` of `A` that is integral over `R` (i.e., it is a root of some monic polynomial with coefficients in `R`) remains integral when mapped from `A` to `B` using the algebra embedding (denoted by `algebraMap`). Here, the scalar tower property ensures the compatibility of the algebra structures.
More concisely: If `R` is a commutative ring, `A` and `B` are algebras over `R`, `A` is an algebra over `B`, and `x` is an element of `A` integral over `R` with compatible algebra structures forming a scalar tower, then `x` is also integral over `R` in `B`.
|
RingHom.isIntegralElem_leadingCoeff_mul
theorem RingHom.isIntegralElem_leadingCoeff_mul :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Polynomial R) (x : S),
Polynomial.eval₂ f x p = 0 → f.IsIntegralElem (f p.leadingCoeff * x)
The theorem `RingHom.isIntegralElem_leadingCoeff_mul` states that for any commutative rings `R` and `S`, a ring homomorphism `f` from `R` to `S`, a polynomial `p` over `R`, and an element `x` of `S`, if the value of the polynomial `p` evaluated at `x` under the ring homomorphism `f` is zero (i.e., `Polynomial.eval₂ f x p = 0`), then the product of the image under `f` of the leading coefficient of `p` and `x` is an integral element of `S` with respect to the ring homomorphism `f` (i.e., `f.IsIntegralElem (f p.leadingCoeff * x)`).
More concisely: If a ring homomorphism maps a polynomial's leading coefficient to zero and evaluates the polynomial to zero at an element, then the product of the leading coefficient and the element is an integral element with respect to the homomorphism.
|
IsIntegralClosure.algebraMap_injective
theorem IsIntegralClosure.algebraMap_injective :
∀ (A : Type u_1) (R : Type u_2) (B : Type u_3) [inst : CommRing R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
[inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst : IsIntegralClosure A R B],
Function.Injective ⇑(algebraMap A B)
The theorem `IsIntegralClosure.algebraMap_injective` states that for any types `A`, `R`, and `B`, with `R` being a commutative ring, `A` being a commutative semiring, and `B` being a ring. Additionally, `B` has two algebra structures over `R` and `A`, and `A` is an integral closure of `R` in `B`. Under these conditions, the algebra map from `A` to `B` is injective. In mathematical terms, this means if `f` is the algebra map from `A` to `B`, for any elements `x` and `y` in `A`, if `f(x) = f(y)`, then `x = y`. This property is crucial in certain areas of algebra and number theory.
More concisely: If `A` is an integral closure of a commutative ring `R` in a commutative ring `B`, then the algebra map from `A` to `B` is injective.
|
isIntegral_one
theorem isIntegral_one :
∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B], IsIntegral R 1 := by
sorry
The theorem `isIntegral_one` states that for any commutative ring `R` and any ring `B` that has an algebra structure over `R`, the element 1 in `B` is integral over `R`. Here, being integral means that it is a root of some monic polynomial with coefficients in `R`. In other words, the number 1 satisfies a certain polynomial equation whose coefficients are chosen from the ring `R`.
More concisely: In a commutative ring `R` and a commutative `R`-algebra `B`, the element 1 in `B` is a root of some monic polynomial with coefficients in `R`.
|
isIntegral_trans
theorem isIntegral_trans :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra A B] [inst_4 : Algebra R B] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R A B],
Algebra.IsIntegral R A → ∀ (x : B), IsIntegral A x → IsIntegral R x
The theorem `isIntegral_trans` states that if `A` is an `R`-algebra in which all elements are integral over `R` (that is, each element of `A` is a root of some monic polynomial with coefficients in `R`), and if `x` is an element of an `A`-algebra that is integral over `A` (meaning `x` is a root of some monic polynomial with coefficients in `A`), then `x` is also integral over `R`. In simpler terms, if elements of an extension algebra are integral over the base ring, and an element of a further extension is integral over the intermediate algebra, then that element is integral over the base ring. This theorem is valid under the conditions that `R`, `A`, and `B` form a scalar tower, which means that the algebra structures are compatible with each other.
More concisely: If `A` is an `R`-algebra with all elements integral over `R`, and `x` is an element of an `A`-algebra that is integral over `A`, then `x` is integral over `R`.
|
IsIntegral.map
theorem IsIntegral.map :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_5}
{C : Type u_6} {F : Type u_7} [inst_3 : Ring B] [inst_4 : Ring C] [inst_5 : Algebra R B] [inst_6 : Algebra A B]
[inst_7 : Algebra R C] [inst_8 : IsScalarTower R A B] [inst_9 : Algebra A C] [inst_10 : IsScalarTower R A C]
{b : B} [inst_11 : FunLike F B C] [inst_12 : AlgHomClass F A B C] (f : F), IsIntegral R b → IsIntegral R (f b)
The theorem `IsIntegral.map` states that for any types `R`, `A`, `B`, `C`, and `F`, if `R` and `A` are commutative rings, `B` and `C` are rings, `R` and `A` are algebras over `B` and `C`, and there exists a scalar tower of `R`, `A`, `B` and another scalar tower of `R`, `A`, `C`. Moreover, if `B` and `C` have a function-like property `F` and there is an algebra homomorphism class `AlgHomClass` between `A`, `B`, `C` with a function `f` of type `F`, then if an element `b` of the algebra `B` over the commutative ring `R` is integral (that is, it is a root of some monic polynomial), then the result of applying the function `f` to `b`, `(f b)`, is also integral over `R`.
More concisely: If `R` is a commutative ring, `B` and `C` are rings, `A` is an `R`-algebra over both `B` and `C`, `F` is a function-like property of `B` and `C`, `AlgHomClass` is an algebra homomorphism class between `A`, `B`, and `C`, `f` is a homomorphism of type `F`, and `b` is an integral element of `B` over `R`, then `(f b)` is integral over `R`.
|
Mathlib.RingTheory.IntegralClosure._auxLemma.7
theorem Mathlib.RingTheory.IntegralClosure._auxLemma.7 :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, (n ∈ p.support) = (p.coeff n ≠ 0)
This theorem states that for any semiring `R`, natural number `n`, and polynomial `p` over `R`, the number `n` is in the support of polynomial `p` if and only if the coefficient of `X^n` in `p` is not zero. In the context of polynomials, the support of a polynomial is the set of all powers of `X` that have a non-zero coefficient. Therefore, this theorem is essentially a characterization of the support of a polynomial in terms of its non-zero coefficients.
More concisely: For any semiring `R`, natural number `n`, and polynomial `p` over `R`, the power `X^n` is in the support of `p` if and only if the coefficient of `X^n` in `p` is non-zero.
|
isIntegral_of_smul_mem_submodule
theorem isIntegral_of_smul_mem_submodule :
∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_5}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
[inst_7 : NoZeroSMulDivisors A M] (N : Submodule R M),
N ≠ ⊥ → N.FG → ∀ (x : A), (∀ n ∈ N, x • n ∈ N) → IsIntegral R x
Suppose `A` is an algebra over a commutative ring `R`, and `M` is a module over `A` such that for all non-zero elements `a` from `A` and `m` from `M`, the scalar product `a • m` is not equal to zero. If there exists an element `x` from `A` that leaves invariant a nontrivial finitely generated `R`-submodule `N` of `M` (meaning for all `n` in `N`, `x • n` is still in `N`), then `x` is integral over `R`. In other words, `x` is a root of some monic polynomial with coefficients in `R`.
More concisely: If `A` is an algebra over a commutative ring `R`, `M` is a non-zero `A`-module, and there exists an element `x` in `A` that fixes a non-trivial finitely generated `R`-submodule of `M`, then `x` is integral over `R`.
|
IsIntegral.tower_top
theorem IsIntegral.tower_top :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B] {x : B},
IsIntegral R x → IsIntegral A x
The theorem `IsIntegral.tower_top` states that, in the context of an algebra tower from `R` to `A` to `B` where `R` is a commutative ring, `A` is a commutative ring, and `B` is a ring, if the element `x` of `B` is integral over `R` (meaning that `x` is a root of some monic polynomial with coefficients in `R`), then `x` is also integral over `A`. This corresponds to the property that if the entire algebra tower is an integral extension, then the sub-extension from `A` to `B` is also integral.
More concisely: If `x` is integral over a commutative ring `R`, then `x` is also integral over any commutative subring `A` contained in the ring `R` where `x` is an element.
|
IsIntegralClosure.isIntegral_algebra
theorem IsIntegralClosure.isIntegral_algebra :
∀ (R : Type u_1) {A : Type u_2} (B : Type u_3) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] [inst_6 : Algebra R A]
[inst_7 : IsScalarTower R A B], Algebra.IsIntegral R A
The theorem `IsIntegralClosure.isIntegral_algebra` states that for any types `R`, `A`, and `B` where `R` is a commutative ring, `A` and `B` are also commutative rings, `B` is an algebra over both `R` and `A`, `A` is an integral closure of `R` in `B`, and `A` is an algebra over `R` with `A` forming a scalar tower with `R` and `B`, then `A` is an integral algebra over `R`. In simpler terms, every element of `A` is integral over the base ring `R`.
More concisely: If `R` is a commutative ring, `A` and `B` are commutative rings with `B` an algebra over both `R` and `A`, `A` an integral closure of `R` in `B`, and `A` forming a scalar tower with `R` and `B`, then every element of `A` is integral over `R`.
|
RingHom.IsIntegralElem.of_mem_closure
theorem RingHom.IsIntegralElem.of_mem_closure :
∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x y z : S},
f.IsIntegralElem x → f.IsIntegralElem y → z ∈ Subring.closure {x, y} → f.IsIntegralElem z
This theorem states that if we have two elements `x` and `y` of a commutative ring `S` that are integral over a commutative ring `R` with respect to a ring homomorphism `f` from `R` to `S`, then any element `z` that is in the subring of `S` generated by `{x, y}` is also integral over `R` with respect to `f`. In other words, `z` is a root of a monic polynomial `p` from `R[X]` when evaluated under `f`.
More concisely: If `x` and `y` are elements of a commutative ring `S` that are integral over a commutative ring `R` with respect to a ring homomorphism `f` from `R` to `S`, then any element `z` in the subring generated by `{x, y}` is also integral over `R` with respect to `f`.
|
IsIntegral.of_finite
theorem IsIntegral.of_finite :
∀ (R : Type u_1) {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B]
[inst_3 : Module.Finite R B] (x : B), IsIntegral R x
The theorem `IsIntegral.of_finite` states that for any commutative ring `R` and any ring `B` that is a `R`-algebra, if `B` is a finite `R`-module, then every element `x` of `B` is integral over `R`. In other words, for any element `x` in `B`, there exists a monic polynomial `p` with coefficients in `R` such that `x` is a root of `p`. Equivalently, the element `x` is integral with respect to the induced `algebraMap` from `R` to `B`.
More concisely: If `R` is a commutative ring and `B` is an `R`-algebra such that `B` is a finite `R`-module, then every element in `B` is integral over `R`.
|
integralClosure_map_algEquiv
theorem integralClosure_map_algEquiv :
∀ {R : Type u_1} {A : Type u_2} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
[inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : A ≃ₐ[R] S),
Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S
This theorem states that if you have an algebraic equivalence (denoted by `A ≃ₐ[R] S`) between two R-algebras A and S, then mapping the integral closure of R in A, using this equivalence, will give you the integral closure of R in S. In other words, the integral closure operation is preserved under algebraic equivalence (or isomorphism). This property is important for understanding how integral closures behave in different algebraic contexts.
More concisely: If A and S are R-algebras related by an algebraic equivalence, then the integral closure of R in A is equal to the integral closure of R in S.
|
IsIntegralClosure.algebraMap_mk'
theorem IsIntegralClosure.algebraMap_mk' :
∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
[inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x),
(algebraMap A B) (IsIntegralClosure.mk' A x hx) = x
The theorem `IsIntegralClosure.algebraMap_mk'` states that for all types `R`, `A`, and `B` with the instances of `R`, `A`, and `B` being commutative rings, `R` and `A` being algebras over `B`, and `A` being an integral closure of `R` in `B`, for any element `x` in `B` that is integral over `R`, the algebra map from 'A' to 'B' applied to the integral closure of `x` in `A` is equal to `x`. This essentially means that the map preserves the integral elements of an integral closure when it's applied to them.
More concisely: For any commutative rings R, A, B with A an integral closure of R in B, the algebra map from A to B maps the integral closure of any element x in B integral over R to x itself.
|