NumberField.InfinitePlace.isReal_iff
theorem NumberField.InfinitePlace.isReal_iff :
∀ {K : Type u_2} [inst : Field K] {w : NumberField.InfinitePlace K},
w.IsReal ↔ NumberField.ComplexEmbedding.IsReal w.embedding
This theorem states that, for any given field `K` and an infinite place `w` of that field, `w` is real if and only if the embedding of `w` into the complex numbers is real. In other words, an infinite place of a number field is considered real if its associated complex embedding is fixed by complex conjugation.
More concisely: An infinite place `w` of a field `K` is real if and only if its complex embedding into the complex numbers is self-conjugate.
|
NumberField.InfinitePlace.not_isReal_iff_isComplex
theorem NumberField.InfinitePlace.not_isReal_iff_isComplex :
∀ {K : Type u_2} [inst : Field K] {w : NumberField.InfinitePlace K}, ¬w.IsReal ↔ w.IsComplex
This theorem states that for any number field `K` and any infinite place `w` of `K`, `w` is not a real place if and only if `w` is a complex place. In other words, an infinite place of a number field cannot be both real and complex at the same time. If it's not real, it's definitely complex and vice versa.
More concisely: For any number field K and its infinite place w, w is neither real nor complex if and only if it is complex.
|
NumberField.InfinitePlace.isReal_mk_iff
theorem NumberField.InfinitePlace.isReal_mk_iff :
∀ {K : Type u_2} [inst : Field K] {φ : K →+* ℂ},
(NumberField.InfinitePlace.mk φ).IsReal ↔ NumberField.ComplexEmbedding.IsReal φ
This theorem asserts that for any field `K` and any complex embedding `φ` from `K` to the complex numbers `ℂ`, the infinite place generated by `φ` is real (as defined by `NumberField.InfinitePlace.IsReal`) if and only if the complex embedding `φ` is real (as defined by `NumberField.ComplexEmbedding.IsReal`). In other words, an infinite place in a number field is real if and only if it is defined by an embedding into the complex numbers that is fixed by complex conjugation.
More concisely: For any field `K` and complex embedding `φ:` `K` → `ℂ,` the infinite place generated by `φ` is real if and only if `φ` is a real embedding.
|
NumberField.Embeddings.range_eval_eq_rootSet_minpoly
theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly :
∀ (K : Type u_1) (A : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : Field A] [inst_3 : Algebra ℚ A]
[inst_4 : IsAlgClosed A] (x : K), (Set.range fun φ => φ x) = (minpoly ℚ x).rootSet A
The theorem states that for any algebraically closed field `A` and any number `x` from a number field `K`, the set of values that `x` can take when mapped by all possible embeddings of `K` in `A` is precisely the set of roots in `A` of the minimal polynomial of `x` over the rationals `ℚ`. In other words, each embedding of `K` into `A` sends `x` to a distinct root of its minimal polynomial in `A`.
More concisely: For any algebraically closed field `A` and number `x` from a number field `K`, the set of values obtained by applying all embeddings of `K` into `A` to `x` equals the set of roots in `A` of the minimal polynomial of `x` over the rationals.
|
NumberField.InfinitePlace.mk_embedding
theorem NumberField.InfinitePlace.mk_embedding :
∀ {K : Type u_2} [inst : Field K] (w : NumberField.InfinitePlace K), NumberField.InfinitePlace.mk w.embedding = w
This theorem states that for any given number field `K` and an infinite place `w` of `K`, the infinite place constructed using the complex embedding associated with `w` (by the function `NumberField.InfinitePlace.mk`) is exactly `w` itself. In other words, the process of obtaining a complex embedding from an infinite place and then constructing an infinite place from that embedding is an identity operation on the set of infinite places of the number field.
More concisely: For any number field `K` and its infinite place `w`, the complex embedding and subsequent construction of an infinite place from `w` yield the same result. In other words, `NumberField.InfinitePlace.mk (NumberField.complexEmbedding w) = w`.
|
NumberField.ComplexEmbedding.isReal_iff
theorem NumberField.ComplexEmbedding.isReal_iff :
∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
NumberField.ComplexEmbedding.IsReal φ ↔ NumberField.ComplexEmbedding.conjugate φ = φ
This theorem establishes an equivalence for a field `K` and a map `φ` from `K` to the complex numbers `ℂ`. It states that a complex embedding `φ` is real if and only if the conjugate of this embedding `φ` is equal to `φ` itself. In other words, an embedding into the complex numbers is characterized as real if it remains unchanged under the operation of complex conjugation.
More concisely: A complex embedding from a field into the complex numbers is real if and only if its conjugate equals the embedding itself.
|
NumberField.InfinitePlace.comap_mk
theorem NumberField.InfinitePlace.comap_mk :
∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (φ : K →+* ℂ) (f : k →+* K),
(NumberField.InfinitePlace.mk φ).comap f = NumberField.InfinitePlace.mk (φ.comp f)
The theorem `NumberField.InfinitePlace.comap_mk` states that for any two fields `k` and `K` and any ring homomorphisms `φ` from `K` to the complex numbers `ℂ` and `f` from `k` to `K`, the restriction of the infinite place (`NumberField.InfinitePlace.comap`) defined by the complex embedding `φ` along the embedding `f` is equal to the infinite place defined by the composition of the ring homomorphisms `φ` and `f` (`RingHom.comp φ f`). In other words, it's saying that the process of restricting an infinite place and then defining a new infinite place is the same as first composing the two ring homomorphisms and then defining the infinite place.
More concisely: The theorem asserts that the restriction of the infinite place of a complex embedding of a field to an embedding of another field is equal to the infinite place obtained by composing the two embeddings.
|
NumberField.InfinitePlace.mk_eq_iff
theorem NumberField.InfinitePlace.mk_eq_iff :
∀ {K : Type u_2} [inst : Field K] {φ ψ : K →+* ℂ},
NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔
φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ
The theorem `NumberField.InfinitePlace.mk_eq_iff` states that for any field `K` and any two complex embeddings `φ` and `ψ` from `K` into the complex numbers, the infinite place defined by `φ` equals the infinite place defined by `ψ` if and only if `φ` equals `ψ` or the complex conjugate of the embedding `φ` equals `ψ`.
More concisely: The infinite places of a field `K` under complex embeddings `φ` and `ψ` are equal if and only if `φ` is equal to `ψ` or the complex conjugate of `φ`.
|
NumberField.Embeddings.card
theorem NumberField.Embeddings.card :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (A : Type u_2) [inst_2 : Field A] [inst_3 : CharZero A]
[inst_4 : IsAlgClosed A], Fintype.card (K →+* A) = FiniteDimensional.finrank ℚ K
The theorem states that the number of embeddings of a number field is equal to its rank. More specifically, for any type `K` with a field structure and a number field structure, and any type `A` with a field structure, a characteristic zero structure, and an algebraically closed structure, the number of ring homomorphisms from `K` to `A` (represented by `K →+* A`) is equal to the rank of `K` as a vector space over the rationals `ℚ` (represented by `FiniteDimensional.finrank ℚ K`). In essence, this theorem links the algebraic structure of a number field with its geometric or vector space structure.
More concisely: The number of embeddings of a number field into an algebraically closed field of characteristic zero equals the finite dimensionality of the field as a vector space over the rationals.
|
NumberField.InfinitePlace.card_complex_embeddings
theorem NumberField.InfinitePlace.card_complex_embeddings :
∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K],
Fintype.card { φ // ¬NumberField.ComplexEmbedding.IsReal φ } = 2 * NumberField.InfinitePlace.NrComplexPlaces K
This theorem states that for any number field `K`, the number of complex embeddings that are not real, i.e., they are not fixed by complex conjugation, is twice the number of infinite complex places of the number field `K`. Here, an infinite place of a number field is complex if its residue field is the complex numbers. In mathematical terms, given a number field `K`, the cardinality of the set of complex embeddings not fixed by complex conjugation equals twice the number of infinite complex places of `K`.
More concisely: The number of complex embeddings of a number field `K` not fixed by complex conjugation equals twice the number of its infinite complex places.
|
NumberField.InfinitePlace.not_isUnramified_iff
theorem NumberField.InfinitePlace.not_isUnramified_iff :
∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
{w : NumberField.InfinitePlace K},
¬NumberField.InfinitePlace.IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
The theorem `NumberField.InfinitePlace.not_isUnramified_iff` states that for any field `k`, field extension `K` of `k`, and an infinite place `w` of `K`, the infinite place `w` is not unramified if and only if `w` is a complex place and the restriction of `w` to `k` via the algebra structure is a real place. Here, an infinite place being unramified means that when restricted to the field `k`, the place has the same multiplicity. An infinite place is defined as complex if it's defined by a complex embedding, and as real if it's defined by a real embedding.
More concisely: For a field extension K of k and an infinite place w of K, w is not unramified if and only if w is a complex place with a real restriction when regarded as an algebra homomorphism from the algebraic closure of k into the completion of K at w.
|
NumberField.Embeddings.pow_eq_one_of_norm_eq_one
theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (A : Type u_2) [inst_2 : NormedField A]
[inst_3 : IsAlgClosed A] [inst_4 : NormedAlgebra ℚ A] {x : K},
IsIntegral ℤ x → (∀ (φ : K →+* A), ‖φ x‖ = 1) → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
This theorem states that for any algebraic integer `x` in a number field `K` that is also a normed field `A`, if `x` is integral and the norm of every embedding `φ` of `x` is one, then `x` is a root of unity. In other words, there exists a positive integer `n` such that `x` to the power of `n` is equal to one. This theorem shows that algebraic integers with a norm of one have a special property, specifically that they are roots of unity.
More concisely: If `x` is an algebraic integer in a number field `K` that is also a normed field `A`, with `x` integral and having norm one for every embedding `φ`, then `x` is a root of unity.
|
NumberField.InfinitePlace.card_real_embeddings
theorem NumberField.InfinitePlace.card_real_embeddings :
∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K],
Fintype.card { φ // NumberField.ComplexEmbedding.IsReal φ } = NumberField.InfinitePlace.NrRealPlaces K
This theorem states that for any number field `K`, the number of complex embeddings of `K` into `ℂ` that are real (i.e., they are fixed by complex conjugation) is equal to the number of infinite real places of `K`. The number of such embeddings is calculated using the `Fintype.card` function which provides the number of elements in a finite type. The infinite real places of a number field are a notion from algebraic number theory, giving a count of the "real parts" of the number field.
More concisely: The number of real complex embeddings of a number field `K` equals the number of its infinite real places.
|
NumberField.InfinitePlace.comap_surjective
theorem NumberField.InfinitePlace.comap_surjective :
∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K],
Algebra.IsAlgebraic k K → Function.Surjective fun x => x.comap (algebraMap k K)
This theorem states that for any two types `k` and `K`, which are fields, where an algebra structure exists from `k` to `K` and `K` is an algebraic over `k`, the function that takes an infinite place of `K` and maps it to an infinite place of `k` is surjective. In other words, for every infinite place in `k`, there exists an infinite place in `K` such that when the infinite place of `K` is restricted along the algebraic embedding from `k` to `K`, we get the original infinite place of `k`.
More concisely: For any field extension K of a field k with a given algebra structure, every infinite place of k has an infinite place in K mapping to it under restriction along the algebraic embedding.
|
NumberField.Embeddings.finite_of_norm_le
theorem NumberField.Embeddings.finite_of_norm_le :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (A : Type u_2) [inst_2 : NormedField A]
[inst_3 : IsAlgClosed A] [inst_4 : NormedAlgebra ℚ A] (B : ℝ),
{x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite
The theorem states that for any number field `K`, any normed field `A`, and any real number `B`, the set of all algebraic integers in `K` such that all of their conjugates have a norm less than or equal to `B` is finite. Here, an algebraic integer is said to be integral if it is a root of some monic polynomial `p` over the integers. And a conjugate of an element of a number field is the image of that element under an embedding of the field into the complex numbers.
More concisely: For any number field `K`, the set of algebraic integers in `K` with norm of all conjugates less than or equal to a real number `B` forms a finite set.
|
NumberField.InfinitePlace.even_card_aut_of_not_isUnramified
theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified :
∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
{w : NumberField.InfinitePlace K} [inst_3 : IsGalois k K] [inst_4 : FiniteDimensional k K],
¬NumberField.InfinitePlace.IsUnramified k w → Even (Fintype.card (K ≃ₐ[k] K))
This theorem states that for any number field `K` over a field `k` with a given infinite place `w`, if `K` is a Galois extension of `k` and `K` is of finite dimension over `k`, then if the infinite place `w` is not unramified in the field extension from `k` to `K`, the number of field automorphisms of `K` that fix `k` (denoted as `(K ≃ₐ[k] K)`) is an even number. In other words, if a certain form of complexity (ramification) at the infinite place happens when extending from `k` to `K`, the group of automorphisms of `K` preserving `k` must have even order.
More concisely: If `K` is a finite-dimensional Galois extension of number field `k` such that `w` is an infinite place of `K` that is ramified in the extension, then the order of the group of `k`-automorphisms of `K` is even.
|
NumberField.InfinitePlace.mult_comap_le
theorem NumberField.InfinitePlace.mult_comap_le :
∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k →+* K) (w : NumberField.InfinitePlace K),
(w.comap f).mult ≤ w.mult
The theorem `NumberField.InfinitePlace.mult_comap_le` asserts that for any field `k`, any field `K`, any ring homomorphism `f` from `k` to `K`, and any infinite place `w` of `K`, the multiplicity of the infinite place obtained by the restriction of `w` along the embedding `f` (using `comap`) is less than or equal to the multiplicity of the original infinite place `w` in `K`. Here, the multiplicity of an infinite place refers to the number of distinct complex embeddings that define it.
More concisely: For any field homomorphism `f` and infinite place `w` of a field `K`, the multiplicity of the image of `w` under the restriction of `w` along `f` is less than or equal to the multiplicity of `w` in `K`.
|
NumberField.InfinitePlace.prod_eq_abs_norm
theorem NumberField.InfinitePlace.prod_eq_abs_norm :
∀ {K : Type u_2} [inst : Field K] [inst_1 : NumberField K] (x : K),
(Finset.univ.prod fun w => w x ^ w.mult) = ↑|(Algebra.norm ℚ) x|
This theorem, named `NumberField.InfinitePlace.prod_eq_abs_norm`, states that for any number field `K` and any element `x` from `K`, the infinite part of the product formula holds. More specifically, it means that the product of the normalized absolute values of `x` for all places `w` (which we denote by `‖x‖_w`) equals the absolute value of the norm of `x` (denoted by `|norm(x)|`). In mathematical notation, we represent this as `Π_w ‖x‖_w = |norm(x)|`. Here, the norm of an element `s` of an `R`-algebra is defined as the determinant of the multiplication operation `(*) s`.
More concisely: For any number field `K` and its element `x`, the infinite product of the normalized absolute values of `x` at all places equals the absolute value of `x`'s norm. That is, `∏_w ‖x‖_w = |norm(x)|`.
|
NumberField.ComplexEmbedding.IsConj.eq
theorem NumberField.ComplexEmbedding.IsConj.eq :
∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ}
{σ : K ≃ₐ[k] K}, NumberField.ComplexEmbedding.IsConj φ σ → ∀ (x : K), φ (σ x) = star (φ x)
The theorem `NumberField.ComplexEmbedding.IsConj.eq` states that for any field `K` with a field `k` as its scalar field, given an embedding `φ` from `K` into the complex numbers `ℂ`, and a `k`-algebra isomorphism `σ` of `K` with itself, if `σ` is a conjugation under `φ`, then for any element `x` of `K`, the image of `σ(x)` under `φ` is the complex conjugate of the image of `x` under `φ`. In other words, applying the isomorphism and then the embedding is the same as applying the embedding and then taking the complex conjugate.
More concisely: For any field extension `K/k` with complex embedding `φ` and `k`-algebra isomorphism `σ` of `K` as a conjugation under `φ`, `φ(σ(x)) = overline{φ(x)}` for all `x` in `K`.
|
NumberField.ComplexEmbedding.IsReal.isConjGal_one
theorem NumberField.ComplexEmbedding.IsReal.isConjGal_one :
∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ},
NumberField.ComplexEmbedding.IsReal φ → NumberField.ComplexEmbedding.IsConj φ 1
This theorem, referred to as an alias of the reverse direction of `NumberField.ComplexEmbedding.isConj_one_iff`, establishes that for any field `K` with the algebra structure over another field `k`, and any ring homomorphism `φ` from `K` to the complex numbers `ℂ`, if `φ` is a real embedding (i.e., it is fixed by complex conjugation), then `φ` is a conjugation under the identity automorphism of `K`. That is, the complex conjugate of `φ` is the composition of `φ` with the identity automorphism on `K`.
More concisely: If `φ: K -> ℂ` is a real embedding of the field `K` as an algebra over another field `k`, then the complex conjugate of `φ` is equal to `φ` composed with the identity automorphism on `K`.
|