Reindexed basis

This file introduces an equivalence between the set of embeddings of K into ℂ and the index set of the chosen basis of the ring of integers of K.

Tags

house, number field, algebraic number

@[reducible, inline]

noncomputable abbrev NumberField.equivReindex (K : Type u_1) [Field K] [NumberField K] : (K →+* ℂ) ≃ Module.Free.ChooseBasisIndex ℤ (RingOfIntegers K)

An equivalence between the set of embeddings of K into ℂ and the index set of the chosen basis of the ring of integers of K.

@[reducible, inline]

noncomputable abbrev NumberField.basisMatrix (K : Type u_1) [Field K] [NumberField K] : Matrix (K →+* ℂ) (K →+* ℂ) ℂ

The basis matrix for the embeddings of K into ℂ. This matrix is formed by taking the lattice basis vectors of K and reindexing them according to the equivalence equivReindex, then transposing the resulting matrix.

theorem NumberField.basisMatrix_eq_embeddingsMatrixReindex (K : Type u_1) [Field K] [NumberField K] : basisMatrix K = Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) RingHom.equivRatAlgHom

theorem NumberField.conj_basisMatrix (K : Type u_1) [Field K] [NumberField K] : (basisMatrix K).map ⇑(starRingEnd ℂ) = (Matrix.reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) (basisMatrix K)

theorem NumberField.det_of_basisMatrix_non_zero (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] : (basisMatrix K).det ≠ 0

@[implicit_reducible]

noncomputable instance NumberField.instInvertibleMatrixRingHomComplexBasisMatrix (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] : Invertible (basisMatrix K)

theorem NumberField.canonicalEmbedding_eq_basisMatrix_mulVec {K : Type u_1} [Field K] [NumberField K] (α : K) : (canonicalEmbedding K) α = (basisMatrix K).transpose.mulVec fun (i : K →+* ℂ) => ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)

theorem NumberField.inverse_basisMatrix_mulVec_eq_repr {K : Type u_1} [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] (α : RingOfIntegers K) (i : K →+* ℂ) : (basisMatrix K).transpose⁻¹.mulVec (fun (j : K →+* ℂ) => (canonicalEmbedding K) ((algebraMap (RingOfIntegers K) K) α) j) i = ↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)