English
Given a map b: κ → B, the matrix whose (i,σ) entry is σ(b(i)) collects all A-embeddings σ: B →ₐ[A] C evaluated at the basis elements b(i).
Русский
При заданной карте b: κ → B матрица, чьи элементы на позиции (i,σ) равны σ(b(i)) для вложения σ: B →ₐ[A] C, собирает значения вложений на базисных элементах b(i).
LaTeX
$$$\\mathrm{embeddingsMatrix}(b)_{i,\\sigma} = \\sigma(b_i) \\quad (\\sigma : B \\toₐ[A] C)$$$
Lean4
/-- `embeddingsMatrix A C b : Matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is
`σ (b i)`. It is mostly useful for fields when `Fintype.card κ = finrank A B` and `C` is
algebraically closed. -/
def embeddingsMatrix (b : κ → B) : Matrix κ (B →ₐ[A] C) C :=
of fun i (σ : B →ₐ[A] C) =>
σ
(b i)
-- TODO: set as an equation lemma for `embeddingsMatrix`, see https://github.com/leanprover-community/mathlib4/pull/3024
