NumberField.mixedEmbedding.disjoint_span_commMap_ker
theorem NumberField.mixedEmbedding.disjoint_span_commMap_ker :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
Disjoint (Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K)))
(LinearMap.ker (NumberField.mixedEmbedding.commMap K))
This theorem, `NumberField.mixedEmbedding.disjoint_span_commMap_ker`, states that for any number field `K`, the vector space spanned (over real numbers `ℝ`) by the image of the `ℂ`-basis of `ℂ^n` defined via `canonicalEmbedding.latticeBasis` is disjoint from the kernel of the linear map `commMap` defined in `NumberField.mixedEmbedding`. Here, two vector spaces are considered disjoint if their intersection is the zero vector space. This is a technical condition required to show that the image of the `ℂ`-basis is a `ℝ`-basis of `ℝ^r₁ × ℂ^r₂` in the context of `mixedEmbedding.latticeBasis`.
More concisely: The image of the complex basis of a number field under the `commMap` map in the mixed embedding is disjoint from its kernel with respect to the real vector space structure.
|
NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul
theorem NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (K →+* ℂ) → ℂ),
(∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)) →
∀ (c : NumberField.mixedEmbedding.index K),
↑(((NumberField.mixedEmbedding.stdBasis K).repr ((NumberField.mixedEmbedding.commMap K) x)) c) =
(NumberField.mixedEmbedding.matrixToStdBasis K).mulVec (x ∘ ⇑(NumberField.mixedEmbedding.indexEquiv K)) c
The theorem `NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul` states that for a field `K` which is a number field, if we have a function `x` from the set of complex embeddings of `K` into complex numbers `ℂ` such that each `x_φ` is the complex conjugate of `x_(conj φ)` for every complex embedding `φ : K →+* ℂ`, then the representation of `commMap K x` on the standard basis (`stdBasis`) is (up to reindexing) given by the product of `matrixToStdBasis` and `x`. In other words, the linear map `commMap` which makes `canonicalEmbedding` and `mixedEmbedding` commute interacts with the standard basis in a specific way defined by the matrix multiplication with `x`. Here, `NumberField.ComplexEmbedding.conjugate φ` denotes the complex conjugate of a complex embedding, and `starRingEnd ℂ` is the complex conjugate operation in the field of complex numbers.
More concisely: For a number field `K` and a complex embedding function `x : Set (ComplexEmbedding K) -> ℂ` such that `x_φ = (x (conj φ))*` for all `φ : ComplexEmbedding K`, the representation of `commMap K x` on the standard basis is equal to the product of `matrixToStdBasis` and `x`.
|
NumberField.canonicalEmbedding.conj_apply
theorem NumberField.canonicalEmbedding.conj_apply :
∀ {K : Type u_1} [inst : Field K] {x : (K →+* ℂ) → ℂ} (φ : K →+* ℂ),
x ∈ Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding K)) →
(starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)
This theorem states that for any field `K` and any function `x` from the set of ring homomorphisms from `K` to the complex numbers `ℂ` to `ℂ`, if `x` lies in the real `ℝ`-submodule spanned by the image of the canonical embedding of `K`, then the complex conjugate of `x` evaluated at any ring homomorphism `φ` from `K` to `ℂ` is equal to `x` evaluated at the complex conjugate of `φ`. In other words, the image of the canonical embedding of a number field `K` lives in the `ℝ`-submodule of `x` such that the complex conjugate of `x` applied to `φ` is equal to `x` applied to the complex conjugate of `φ` for all ring homomorphisms `φ` from `K` to `ℂ`.
More concisely: For any field `K` and ring homomorphism `x` from `K` to the complex numbers `ℂ` with image in `K`'s real submodule, `x` and its complex conjugate satisfy `x(φ) = old φ.conj(). x` for all ring homomorphisms `φ` from `K` to `ℂ`.
|