Algebra.norm_algebraMap_of_basis
theorem Algebra.norm_algebraMap_of_basis :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type w}
[inst_3 : Fintype ι], Basis ι R S → ∀ (x : R), (Algebra.norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
The theorem `Algebra.norm_algebraMap_of_basis` states that for any base ring `R`, any ring `S` that is an algebra over `R`, any finite type `ι`, any basis of `S` over `R` indexed by `ι`, and any element `x` in `R`, the norm of the image of `x` under the algebra embedding from `R` to `S` is equal to `x` raised to the power of the number of elements in `ι`. In other words, if `x` is an element of the base ring `R`, then the norm of `x` in the algebra `S` over `R` is equal to `x` to the power of the dimension of `S` over `R`, where the dimension is defined by the card (number of elements) of the finite type indexing the basis.
More concisely: For any base ring R, algebra S over R, finite type ι, basis of S over R indexed by ι, and x in R, the norm of x under the algebra embedding from R to S equals x raised to the power of the cardinality of ι.
|
Algebra.norm_eq_zero_iff'
theorem Algebra.norm_eq_zero_iff' :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
[inst_4 : IsDomain S] [inst_5 : Module.Free R S] [inst_6 : Module.Finite R S] {x : S},
LinearMap.det ((LinearMap.mul R S) x) = 0 ↔ x = 0
The theorem `Algebra.norm_eq_zero_iff'` states that for any types `R` and `S` with the conditions that `R` is a commutative ring, `S` is a ring, `S` is an algebra over `R`, both `R` and `S` are integral domains, `S` is a free `R`-module, and `S` is a finite `R`-module, for any element `x` in `S`, the determinant of the linear map produced by multiplying `x` in the algebra `S` is zero if and only if `x` is zero. In other words, the determinant of the multiplication operation at `x` in this specific algebra context vanishes exactly when `x` is zero.
More concisely: For any commutative ring R, ring S that is a free finite R-module and algebra over R, if S is an integral domain and x in S has determinant 0 as a linear map in S, then x is the additive identity of S.
|
Algebra.norm_algebraMap
theorem Algebra.norm_algebraMap :
∀ {K : Type u_4} [inst : Field K] {L : Type u_7} [inst_1 : Ring L] [inst_2 : Algebra K L] (x : K),
(Algebra.norm K) ((algebraMap K L) x) = x ^ FiniteDimensional.finrank K L
The theorem `Algebra.norm_algebraMap` states that for any element `x` in the base field `K`, the norm (as defined by the function `Algebra.norm`) of the embedded value of `x` in an `R`-algebra `L` (where `K` is a field and `L` is a ring with an algebra structure over `K`) is equal to `x` raised to the power of the rank of `L` over `K` (`FiniteDimensional.finrank K L`).
In other words, this theorem describes the relationship between the norm of an element of the base field when embedded in an algebra, and the rank of the module constituted by the algebra over the base field. If `L` is not finite-dimensional over `K`, then the norm is `1`, since the rank is `0` and `x` to the power of `0` is `1`.
More concisely: For any field extension K into an R-algebra L, the norm of an element x in K equals x raised to the power of the finite rank of L over K.
|
Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly
theorem Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
(Algebra.norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0
This theorem states that for any power basis `pb` of a ring `S` over a commutative ring `R`, the algebraic norm of the generator of the power basis (`pb.gen`) is equal to the product of `(-1)` raised to the power of the dimension of the power basis (`pb.dim`) and the coefficient of the minimal polynomial of the generator over `R` at zero. In other words, if you consider the determinant of the linear map which multiplication by `pb.gen` induces, you will get the same value as `-1` to the power of the dimension of the basis times the constant term of the minimal polynomial of the generator.
More concisely: For any power basis `pb` over a commutative ring `R`, the norm of `pb.gen` is equal to `(-1) ^ (pb.dim) * coeff(minimal polynomial of `pb.gen` at 0)`.
|
Algebra.norm_eq_zero_iff
theorem Algebra.norm_eq_zero_iff :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
[inst_4 : IsDomain S] [inst_5 : Module.Free R S] [inst_6 : Module.Finite R S] {x : S},
(Algebra.norm R) x = 0 ↔ x = 0
This theorem states that for any types `R` and `S`, where `R` is a commutative ring, `S` is a ring, and `S` is an `R`-algebra, `R` is a domain and `S` is also a domain, `S` is a free `R`-module, and `S` is a finite `R`-module, if an element `x` of type `S` satisfies the condition that the algebraic norm of `x` (calculated as the determinant of `(*) x`) is zero, then it is equivalent to stating that the element `x` itself is zero. This theorem provides a necessary and sufficient condition for an element of an `R`-algebra to be zero in terms of the algebraic norm.
More concisely: In a commutative ring `R`, for any domain `S` that is a finite `R`-algebra, an `R`-module, and a domain, the algebraic norm of an element `x` in `S` being zero is equivalent to `x` being the additive identity in `S`.
|
Algebra.PowerBasis.norm_gen_eq_prod_roots
theorem Algebra.PowerBasis.norm_gen_eq_prod_roots :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {F : Type u_6}
[inst_3 : Field F] [inst_4 : Algebra R F] (pb : PowerBasis R S),
Polynomial.Splits (algebraMap R F) (minpoly R pb.gen) →
(algebraMap R F) ((Algebra.norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
This theorem states that given a power basis `pb` over a commutative ring `R` and a ring `S`, with `R` being an algebra over `S`, and given a field `F` where `R` is also an algebra over `F`, if the minimal polynomial of `pb.gen` over `R` splits (i.e., it is either zero or all of its irreducible factors have degree 1) when mapped from `R` to `F` via the algebra map, then the map from `R` to `F` applied to the norm of `pb.gen` equals the product of the roots of the minimal polynomial of `pb.gen` over `R` in `F`.
More concisely: If `pb` is a power basis over a commutative ring `R`, `S` is a ring with `R` being an algebra over `S`, `F` is a field where `R` is also an algebra, and the minimal polynomial of `pb.gen` over `R` splits and has all irreducible factors of degree 1 when mapped from `R` to `F`, then the norm of `pb.gen` in `F` equals the product of its roots in `F`.
|
Algebra.norm_eq_prod_embeddings
theorem Algebra.norm_eq_prod_embeddings :
∀ (K : Type u_4) {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_7)
[inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : FiniteDimensional K L] [inst_6 : IsSeparable K L]
[inst_7 : IsAlgClosed E] (x : L), (algebraMap K E) ((Algebra.norm K) x) = Finset.univ.prod fun σ => σ x
This theorem states that for a finite separable extension `L/K` of fields and an algebraically closed extension `E` of `K`, the norm (down to `K`) of an element `x` from `L` is equal to the product of the images of `x` under all `K`-embeddings `σ` of `L` into `E`.
In simpler terms, if we consider two field extensions `L/K` and `E/K`, where `L/K` is finite and separable, and `E` is algebraically closed, for any element in `L`, when we calculate its norm and map it to `E`, it is equal to the product of all its images under every possible `K`-embedding from `L` to `E`. This gives us a concrete way to understand and calculate the norm of an element in `L` with respect to the field `K`.
More concisely: For a finite separable extension `L/K` of fields and an algebraically closed extension `E/K`, the norm of an element `x` in `L` equals the product of its images under all `K`-embeddings from `L` into `E`.
|