AlgebraicIndependent.restrictScalars
theorem AlgebraicIndependent.restrictScalars :
∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
[inst_2 : Algebra R A] {K : Type u_9} [inst_3 : CommRing K] [inst_4 : Algebra R K] [inst_5 : Algebra K A]
[inst_6 : IsScalarTower R K A],
Function.Injective ⇑(algebraMap R K) → AlgebraicIndependent K x → AlgebraicIndependent R x
The theorem `AlgebraicIndependent.restrictScalars` states that if a set of elements in an algebra `A` is algebraically independent over a ring `K`, then this set is also algebraically independent over any subring `R` of `K`. Here, "algebraically independent" means that the canonical mapping from the multivariable polynomial ring to `A` is injective. The theorem requires the conditions that `R`, `A`, and `K` are commutative rings, `A` and `K` are algebras over `R`, and `A` is also an algebra over `K` such that there exists a scalar tower from `R` to `K` to `A`. A scalar tower exists if the scalar multiplication in `A` by an element of `R` is the same as the scalar multiplication by the same element viewed as an element of `K`. The theorem also requires the mapping by the algebra structure from `R` to `K` to be injective.
More concisely: If a set of elements is algebraically independent over a ring K, then it is also algebraically independent over any subring R of K such that the scalar multiplication in A by elements of R is the same as that by the same elements viewed as in K, and the mapping from R to K by the algebra structure is injective.
|
AlgebraicIndependent.injective
theorem AlgebraicIndependent.injective :
∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
[inst_2 : Algebra R A], AlgebraicIndependent R x → ∀ [inst : Nontrivial R], Function.Injective x
This theorem states that, for every type `ι`, every type `R` being a commutative ring, every type `A` being a commutative ring with an algebra structure over `R`, and every function `x` from `ι` to `A`, if the function `x` is algebraically independent over `R` (i.e., the canonical map from the multivariable polynomial ring in the elements of `x` to `A` is injective), then, under the assumption that `R` is nontrivial, the function `x` itself is injective. In other words, no two distinct elements in the domain `ι` map to the same value in `A` under `x` when `x` is algebraically independent and `R` is nontrivial.
More concisely: If `R` is a nontrivial commutative ring, `A` is a commutative `R`-algebra, `x : ι → A` is an algebraically independent function, then `x` is injective.
|
algebraicIndependent_finset_map_embedding_subtype
theorem algebraicIndependent_finset_map_embedding_subtype :
∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : Set A),
AlgebraicIndependent R Subtype.val → ∀ (t : Finset ↑s), AlgebraicIndependent R Subtype.val
This theorem states that for any commutative ring `R` and any algebra `A` over `R`, if a set `s` of elements in `A` is algebraically independent over `R`, then every finite subset `t` of `s` is also algebraically independent over `R`. Here, 'algebraically independent' means that the canonical map from the multivariable polynomial ring to `A` is injective when evaluated at the elements of the set. The set `s` is considered as a set of subtypes, where each subtype is a pair of an element and a proof that the element belongs to `s`. The underlying elements in `s` and `t` are extracted using the function `Subtype.val`.
More concisely: If `s` is a set of algebraically independent elements over a commutative ring `R` in an algebra `A`, then every finite subset `t` of `s` is also algebraically independent over `R`.
|
algebraicIndependent_equiv'
theorem algebraicIndependent_equiv' :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
[inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A} {g : ι → A},
f ∘ ⇑e = g → (AlgebraicIndependent R g ↔ AlgebraicIndependent R f)
The theorem `algebraicIndependent_equiv'` states that for any types `ι`, `ι'`, `R`, and `A`, with `R` and `A` being commutative rings and `A` being an `R`-algebra, given a bijective function `e` from `ι` to `ι'`, and functions `f` from `ι'` to `A` and `g` from `ι` to `A` such that `f` is the composition of `g` and `e`, then `g` is algebraically independent over `R` if and only if `f` is algebraically independent over `R`. In other words, the algebraic independence of a family of elements in an `R`-algebra is preserved under a change of indexing set by a bijection.
More concisely: If `e: ι --> ι'` is a bijection, `g: ι --> A` and `f: ι' --> A` are such that `f = g ∘ e`, and `R` is a commutative ring with `A` being an `R`-algebra, then `g` is algebraically independent over `R` if and only if `f` is algebraically independent over `R`.
|
AlgebraicIndependent.comp
theorem AlgebraicIndependent.comp :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
[inst_2 : Algebra R A],
AlgebraicIndependent R x → ∀ (f : ι' → ι), Function.Injective f → AlgebraicIndependent R (x ∘ f)
The theorem `AlgebraicIndependent.comp` states that for any types `ι`, `ι'`, `R`, and `A`; any function `x` from `ι` to `A`; if `x` is algebraically independent over `R` (meaning that the canonical map out of the multivariable polynomial ring is injective), then for any function `f` from `ι'` to `ι` that is injective, the composition of `x` and `f`, denoted by `(x ∘ f)`, is also algebraically independent over `R`. This is under the preconditions that `R` and `A` are commutative rings and `A` is an algebra over `R`.
More concisely: If `x: ι → A` is an algebraically independent function from a type `ι` to a commutative `R`-algebra `A`, then the composition `x ∘ f` is algebraically independent over `R` for any injective function `f: ι' → ι`.
|
AlgebraicIndependent.of_subtype_range
theorem AlgebraicIndependent.of_subtype_range :
∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_9}
{f : ι → A}, Function.Injective f → AlgebraicIndependent R Subtype.val → AlgebraicIndependent R f
This theorem, referred to as `AlgebraicIndependent.of_subtype_range`, states that for any types `R`, `A`, and `ι`, and any function `f` from `ι` to `A`, if `f` is injective and the subtype value (`.val`) function is algebraically independent over `R`, then `f` is also algebraically independent over `R`. Here, `R` is a commutative ring, `A` is a commutative ring which is an `R`-algebra, and `ι` is any type. Algebraic independence in this context means that the map from the multivariable polynomial ring to `A` given by evaluating a polynomial at a point is injective. In simpler terms, it means that no nontrivial polynomial relation exists among the elements of `f`.
More concisely: If `f : ι -> A` is an injective function from a type `ι` to an `R-`algebra `A` over a commutative ring `R`, and the subtype values of `f` are algebraically independent over `R`, then `f` itself is algebraically independent over `R`.
|
algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded
theorem algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded :
∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {n : ℕ},
(∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n) →
∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
This theorem states that if every finite set of algebraically independent elements over a commutative ring R in a commutative ring A has a cardinality at most `n`, then this same upper bound `n` applies to the cardinality of any set of algebraically independent elements. In other words, if a property holds for all finite sets of algebraically independent elements, then it also holds for all sets, possibly infinite, of such elements. Here, an element is considered algebraically independent if the multivariable polynomial mapping on it is injective.
More concisely: If every finite set of algebraically independent elements in a commutative ring has cardinality bounded by some natural number `n`, then every set of algebraically independent elements in the ring also has cardinality at most `n`.
|