IsAdjoinRoot.map_X
theorem IsAdjoinRoot.map_X :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f), h.map Polynomial.X = h.root
The theorem `IsAdjoinRoot.map_X` states that for any commutative ring `R`, ring `S`, polynomial `f` of `R`, and algebra structure between `R` and `S`, if `h` is a proof that the root of `f` can be adjoined to generate `S`, then the result of mapping the indeterminate `X` from the polynomial via `h` is equal to the root of `f` that can be adjoined to generate `S`. In other words, this theorem asserts that the image of the polynomial indeterminate under the map `h` is indeed the root of the polynomial in the adjunctive structure.
More concisely: Given a commutative ring R, ring S, polynomial f over R, and an algebra structure map h : R ℝ S such that the root of f can be adjoined to generate S, the image of the indeterminate X of f under h is equal to the root of f in the adjunctive structure.
|
IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq
theorem IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T},
Polynomial.eval₂ i x f = 0 →
∀ (h : IsAdjoinRoot S f) (z : S) (w : Polynomial R),
h.map w = z → Polynomial.eval₂ i x (h.repr z) = Polynomial.eval₂ i x w
This theorem states that for any commutative rings `R`, `S`, and `T`, a given polynomial `f` with coefficients in `R`, an algebra structure on `S` over `R`, a ring homomorphism `i` from `R` to `T`, and a value `x` in `T` such that the evaluation of the polynomial `f` at `x` under the homomorphism `i` is zero. If `h` is a root of the polynomial `f` adjoined to `S`, for any `z` in `S` and any polynomial `w` in `R` such that the map from `h` to `w` equals `z`, then the evaluation of the representative of `z` under `h` at `x` under the homomorphism `i` is equal to the evaluation of the polynomial `w` at `x` under the homomorphism `i`. In simpler terms, it shows a relationship between the evaluation of a polynomial and its representative in the context of adjoined roots.
More concisely: Given commutative rings R, S, T, a polynomial f over R, an algebra structure on S over R, a ring homomorphism i from R to T, a root h of f adjoined to S, and an element z in S with map h -> w = z, the evaluation of h under i at x (where f(h) = 0 and x in T) equals the evaluation of w under i at x for any polynomial w with map h -> z.
|
IsAdjoinRoot.algebraMap_apply
theorem IsAdjoinRoot.algebraMap_apply :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f) (x : R), (algebraMap R S) x = h.map (Polynomial.C x)
The theorem `IsAdjoinRoot.algebraMap_apply` states that for any commutative ring `R`, ring `S`, polynomial `f` of `R`, and element `x` of `R`, and given that `S` is an algebra over `R` where `S` adjoins a root of `f`, the application of the algebra map from `R` to `S` on `x` is equivalent to the mapping of the constant polynomial of `x` under `h`, where `h` is the function representing the root of `f` adjoined to `S`. In mathematical terms, it means that the algebra map of `x` coincides with applying the root-adjoining map `h` to the constant polynomial of `x`.
More concisely: For any commutative rings R and S, polynomial f of R, and element x of R, if S is an algebra over R extending the roots of f, then the algebra map of x from R to S equals the application of the root of f adjoined to S to the constant polynomial of x.
|
IsAdjoinRoot.aequiv.proof_1
theorem IsAdjoinRoot.aequiv.proof_1 :
∀ {R : Type u_2} [inst : CommRing R] {f : Polynomial R} {T : Type u_1} [inst_1 : CommRing T] [inst_2 : Algebra R T]
(h' : IsAdjoinRoot T f), (Polynomial.aeval h'.root) f = 0
The theorem `IsAdjoinRoot.aequiv.proof_1` states that for all commutative rings `R` and `T`, for all polynomials `f` over `R`, and for all `T` that is an `R`-algebra, if `T` is generated by adjoining a root of `f`, then applying the unique `R`-algebra homomorphism from `R[X]` to `T` (represented by `Polynomial.aeval`) to `f` results in `0`. In other words, the polynomial `f` evaluates to `0` at the root that was adjoined to generate `T`.
More concisely: For all commutative rings R and T being an R-algebra generated by adjoining a root of a polynomial f over R, the image of f under the unique R-algebra homomorphism from R[X] to T is 0.
|
IsAdjoinRoot.ext
theorem IsAdjoinRoot.ext :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h h' : IsAdjoinRoot S f), h.root = h'.root → h = h'
The theorem `IsAdjoinRoot.ext` establishes the principle of extensionality for the `IsAdjoinRoot` structure in the Lean mathematical framework. This means that for any commutative ring `R` and ring `S`, and any polynomial `f` of `R`, if we have two instances of `IsAdjoinRoot`, `h` and `h'`, pertaining to `S` and `f`, then if the roots of `h` and `h'` are the same, it follows that `h` and `h'` are also the same. This theorem does not cover the extensionality of the ring elements, which is addressed separately in `IsAdjoinRootMonic.ext_elem`.
More concisely: If `R` is a commutative ring, `S` is a ring, `f` is a polynomial over `R`, and `h` and `h'` are instances of `IsAdjoinRoot` for `S` and `f` with the same roots, then `h` and `h'` are equal.
|
IsAdjoinRoot.lift_map
theorem IsAdjoinRoot.lift_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
(h : IsAdjoinRoot S f) (z : Polynomial R), (IsAdjoinRoot.lift i x hx h) (h.map z) = Polynomial.eval₂ i x z
The theorem `IsAdjoinRoot.lift_map` states that for any two types `R` and `S` with `R` being a commutative ring and `S` a ring, a given polynomial `f` of `R`, an algebra structure on `R` and `S`, another type `T` with a commutative ring structure, a ring homomorphism `i` from `R` to `T`, and an element `x` in `T` such that the evaluation of polynomial `f` at `x` via ring homomorphism `i` is zero (`hx`), if `f` is an adjoined root in `S` (`h`), then for any polynomial `z` of `R`, the evaluation of the polynomial `z` with the lift of the adjoined root (`IsAdjoinRoot.lift i x hx h`) and its mapping (`h.map z`) is equal to the evaluation of polynomial `z` at `x` via ring homomorphism `i` (`Polynomial.eval₂ i x z`). In simpler terms, this theorem relates the operations of adjoined root lifting and polynomial evaluation.
More concisely: Given a commutative ring R, a ring S, a polynomial f in R, an algebra structure on R and S, a commutative ring T, a ring homomorphism i from R to T, an element x in T such that i(f(x)) = 0 and f is an adjoined root in S, then for any polynomial z in R, the evaluation of z at x via i is equal to the evaluation of z with the lifted adjoined root and its mapping.
|
IsAdjoinRoot.map_repr
theorem IsAdjoinRoot.map_repr :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f) (x : S), h.map (h.repr x) = x
The theorem `IsAdjoinRoot.map_repr` states that for any commutative ring `R` and any ring `S`, if `f` is a polynomial with coefficients in `R`, `S` is an `R`-algebra and `h` is an adjoined root of `f` in `S`, then when we map the representative of `x` in `S` under the function associated with `h`, we get back `x`. In other words, for every element `x` of `S`, if we take its representative in `R` under the adjoined root `h`, then map it back to `S` using `h`, we recover the original element `x`. This is essentially saying that the process of representing an element of `S` in `R` and then using the map `h` to go back to `S` is an identity operation.
More concisely: For any commutative rings R and S, any polynomial f with coefficients in R, and any adjoined root h of f in S, the application of h to the representative of any x in S in R and then the application of the representation function from S to R is equal to the identity function on S.
|
IsAdjoinRoot.mem_ker_map
theorem IsAdjoinRoot.mem_ker_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f) {p : Polynomial R}, p ∈ RingHom.ker h.map ↔ f ∣ p
This theorem states that for any commutative ring `R`, ring `S`, polynomial `f` over `R`, and an instance of `Algebra R S` that turns `S` into an `R`-algebra, if `h` is an instance of `IsAdjoinRoot` that adjoins a root of `f` to `S`, then for any polynomial `p` over `R`, `p` is in the kernel of the ring homomorphism `h.map` if and only if `f` divides `p`. In other words, the kernel of the ring homomorphism `h.map` consists exactly of those polynomials which are divisible by `f`.
More concisely: For any commutative rings `R` and `S`, an `R`-algebra homomorphism `h : S -> R` adjoining a root of a polynomial `f` over `R`, if and only if `p` is in the kernel of `h` for any polynomial `p` over `R`, then `f` divides `p`.
|
IsAdjoinRoot.aeval_root
theorem IsAdjoinRoot.aeval_root :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f), (Polynomial.aeval h.root) f = 0
The theorem `IsAdjoinRoot.aeval_root` states that for any commutative ring `R` and any ring `S`, and for any polynomial `f` over `R`, if `h` is an instance of `IsAdjoinRoot` for `S` and `f` (meaning that `S` is generated by adjoining a root of `f` to `R`), then applying the algebraic evaluation of the polynomial `f` at this root yields zero. In other words, the root defined by `IsAdjoinRoot.root h` is indeed a root of the polynomial `f`.
More concisely: For any commutative rings R and S, and polynomial f over R, if S is generated by adjoining a root of f to R (via an instance h of IsAdjoinRoot for f and S), then the algebraic evaluation of f at h.root h equals zero.
|
IsAdjoinRoot.repr_zero_mem_span
theorem IsAdjoinRoot.repr_zero_mem_span :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f), h.repr 0 ∈ Ideal.span {f}
The theorem `IsAdjoinRoot.repr_zero_mem_span` states that for any commutative ring `R` and any ring `S`, given a polynomial `f` from `R`, and assuming that `S` is an adjoined root of `f`, the zero element of `S` represented as a `Format` type (using the `repr` function) is in the ideal generated by the set containing only the polynomial `f`. In essence, the representation of zero is preserved, up to multiples of the polynomial `f` in the scenario where `S` is an extension of `R` that adjoins a root of `f`.
More concisely: For any commutative rings R and an extension S adjoining a root of polynomial f from R, the zero element of S is in the ideal generated by {f} in R.
|
IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span
theorem IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f) (x y : S), h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}
The theorem `IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span` states that, given a commutative ring `R`, a ring `S`, a polynomial `f` from `R`, and an algebra structure over `R` and `S`, if `S` is an adjoining root of the polynomial `f`, then for any two elements `x` and `y` in `S`, the difference between the representation of the sum of `x` and `y` and the sum of the individual representations of `x` and `y` is an element of the ideal generated by the set containing `f`. This essentially states that the representation function preserves addition up to multiples of the polynomial `f`.
More concisely: Given a commutative ring R, a polynomial f from R, an algebra structure over R and a ring S where S is an algebraic closure of the roots of f, for all x, y in S, the difference between the representation of x + y and the representation of x + y computed separately is an element of the ideal generated by f.
|
IsAdjoinRoot.liftHom_map
theorem IsAdjoinRoot.liftHom_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T] (hx' : (Polynomial.aeval x) f = 0)
(h : IsAdjoinRoot S f) (z : Polynomial R), (IsAdjoinRoot.liftHom x hx' h) (h.map z) = (Polynomial.aeval x) z
This theorem states that for any commutative ring `R`, ring `S`, commutative ring `T`, polynomial `f` over `R`, an algebra `S` over `R`, an algebra `T` over `R`, and an element `x` of `T`, if `x` is a root of the polynomial `f` (that is, `(Polynomial.aeval x) f = 0`) and `S` is generated by the roots of `f` (that is, `h : IsAdjoinRoot S f`), then for any polynomial `z` over `R`, the mapping of `z` under the homomorphism `IsAdjoinRoot.liftHom x hx' h` is equal to the result of evaluating `z` at `x` (that is, `(IsAdjoinRoot.liftHom x hx' h) (h.map z) = (Polynomial.aeval x) z`). Essentially, this theorem ensures the consistency between the root adjoined homomorphism and polynomial evaluation at a root.
More concisely: For any commutative rings `R`, `S`, `T`, polynomial `f` over `R`, algebra `S` over `R` generated by the roots of `f`, and element `x` of `T` being a root of `f`, the root adjoined homomorphism `IsAdjoinRoot.liftHom x h x' h` maps `z` over `R` to the value of `z` evaluated at `x`.
|
IsAdjoinRoot.ext_map
theorem IsAdjoinRoot.ext_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h h' : IsAdjoinRoot S f), (∀ (x : Polynomial R), h.map x = h'.map x) → h = h'
This theorem, `IsAdjoinRoot.ext_map`, states that for any two `IsAdjoinRoot` structures `h` and `h'` over a ring `S` and a polynomial `f` with coefficients from a commutative ring `R`, if for every polynomial `x` from `R`, the map of `x` under `h` is equal to the map of `x` under `h'`, then `h` and `h'` are equal. The underlying context here is algebra, specifically field and ring theory, and this theorem assures the extensionality of the `IsAdjoinRoot` structure.
More concisely: If two `IsAdjoinRoot` structures `h` and `h'` over a ring `S` for polynomial `f` with coefficients from a commutative ring `R` map every polynomial `x` from `R` identically, then `h` and `h'` are equal.
|
IsAdjoinRoot.apply_eq_lift
theorem IsAdjoinRoot.apply_eq_lift :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
(h : IsAdjoinRoot S f) (g : S →+* T),
(∀ (a : R), g ((algebraMap R S) a) = i a) → g h.root = x → ∀ (a : S), g a = (IsAdjoinRoot.lift i x hx h) a
This theorem, "IsAdjoinRoot.apply_eq_lift", is an auxiliary lemma for a certain "apply_eq_lift" operation. It states that for any commutative ring `R`, ring `S`, a polynomial `f` over `R`, an algebra structure over `R` and `S`, another commutative ring `T`, a ring homomorphism `i` from `R` to `T`, and an element `x` of `T` such that the evaluation of the polynomial `f` at `x` using ring homomorphism `i` equals zero, if `f` is an adjoined root in `S`, then for any ring homomorphism `g` from `S` to `T`, if `g` applied to `a` (an element of `R`) via the algebra map from `R` to `S` equals `i` applied to `a`, and `g` applied to the root of `h` equals `x`, then `g` applied to any element of `S` equals the lift of `i` at `x` with respect to `hx` and `h` applied to that element of `S`.
More concisely: If `f` is an adjoined root in `S` over a commutative ring `R`, ring `S`, polynomial `f` over `R`, algebra structures over `R` and `S`, commutative ring `T`, ring homomorphism `i` from `R` to `T`, and `x` in `T` such that `i(a) = g(a)` for all `a` in `R` and `g(h(r)) = x` for some root `h` of `f` in `S`, then `g(s) = i(s).lift(x)` for all `s` in `S`.
|
IsAdjoinRoot.aequiv_map
theorem IsAdjoinRoot.aequiv_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
{T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f)
(z : Polynomial R), (h.aequiv h') (h.map z) = h'.map z
This theorem states that for any two types `R` and `S` which are commutative rings, and an algebra `A` defined over `R` and `S`, and given a polynomial `f` over `R`, if the roots of `f` adjoin `S` and `T` (where `T` is another type with a commutative ring and an algebra over `R`), then for any polynomial `z` over `R`, the mapping of `z` under the `aequiv` function (which transforms between the adjoined roots of `S` and `T`) results in the same value as directly mapping `z` under the roots adjoined with `T`. This theorem is important as it ensures the consistency of the `aequiv` function with the `map` function of the adjoined roots when dealing with polynomials over the same ring.
More concisely: For commutative rings R, S, T, and an algebra A over R in S and T, if the roots of a polynomial f over R are the same when adjoined to S and T, then the mapping of any z over R under the aequiv function for the adjoined roots is equal to directly mapping z under the roots adjoined with T.
|
IsAdjoinRoot.eq_lift
theorem IsAdjoinRoot.eq_lift :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0)
(h : IsAdjoinRoot S f) (g : S →+* T),
(∀ (a : R), g ((algebraMap R S) a) = i a) → g h.root = x → g = IsAdjoinRoot.lift i x hx h
This theorem, named `IsAdjoinRoot.eq_lift`, states that for any commutative rings `R` and `T`, a ring `S`, a polynomial `f` over `R`, an algebra structure from `R` to `S`, a ring homomorphism `i` from `R` to `T`, and an element `x` of `T`, if `x` is a root of the polynomial `f` under the homomorphism `i` and `S` is an adjoined root of `f`, then for any ring homomorphism `g` from `S` to `T` that agrees with the ring homomorphism `i` on `R` and maps the root of `h` to `x`, `g` equals the lift of `i` by `x`, `hx` and `h`. In other words, a map that agrees on the ring `R` and the root of `h` agrees with the `lift` operation everywhere.
More concisely: If `R` and `T` are commutative rings, `S` is an adjoined root of a polynomial `f` over `R` in `S`, `i` is a ring homomorphism from `R` to `T`, `x` is a root of `f` under `i`, and `g` is a ring homomorphism from `S` to `T` agreeing with `i` on `R` and mapping the root of `f` to `x`, then `g = i ∘ hx`, where `h` is the algebra structure from `R` to `S`.
|
IsAdjoinRoot.aeval_eq
theorem IsAdjoinRoot.aeval_eq :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
(h : IsAdjoinRoot S f) (p : Polynomial R), (Polynomial.aeval h.root) p = h.map p
This theorem states that for any types `R` and `S` where `R` is a commutative ring and `S` is a ring, and `f` is a polynomial with coefficients in `R`, given the conditions that `S` is an `R`-algebra and `h` is an indication that a root can be adjoined to `S` to generate a root of `f`, for any polynomial `p` in `R`, the result of applying the algebraic evaluation map `Polynomial.aeval` (which maps `p` to `S`) at the root adjoined to `S` (`IsAdjoinRoot.root h`) is equal to the result of mapping `p` through `h`. In mathematical terms, for any polynomial `p`, we have `aeval(root(h))(p) = h(p)`, where `aeval` is the algebraic evaluation map and `root(h)` is the root associated with `h`.
More concisely: For any commutative ring R, ring S, polynomial f over R with root h, and element p in R, we have Polynomial.aeval (IsAdjoinRoot.root h) (p) = h (p).
|
IsAdjoinRoot.eq_liftHom
theorem IsAdjoinRoot.eq_liftHom :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
{T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T] (hx' : (Polynomial.aeval x) f = 0)
(h : IsAdjoinRoot S f) (g : S →ₐ[R] T), g h.root = x → g = IsAdjoinRoot.liftHom x hx' h
This theorem, named `IsAdjoinRoot.eq_liftHom`, states the uniqueness of the `liftHom` operation in the context of polynomial rings and their roots. In particular, for any commutative ring `R`, ring `S`, polynomial `f` over `R`, and an algebra from `R` to `S`, as well as a commutative ring `T`, element `x` of `T`, and an algebra from `R` to `T`, if `x` is a root of `f` under the algebra evaluation map, and `h` is an adjoined root of `f` in `S`, then for any `R`-algebra homomorphism `g` from `S` to `T` that agrees with `x` on the root of `h`, `g` is equivalent to the `liftHom` operation applied to `x`, the fact `x` is a root of `f`, and `h`. In essence, any algebra homomorphism that maps the adjoined root to the same value as `x`, must be the same as the `liftHom` operation.
More concisely: Given a commutative ring R, rings S and T, a polynomial f over R, an algebra homomorphism g from S to T, an element x in T being a root of f under the algebra evaluation map, and h an adjoined root of f in S such that g(h) = x, then g is equivalent to the `liftHom` operation applied to x, the fact x is a root of f, and h.
|