English
Reindexing the embeddings matrix by a bijection e from κ to the set of embeddings corresponds to permuting its columns according to e.
Русский
Переиндексация матрицы вложений по биекциям e из κ в множество вложений соответствует перестановке её столбцов согласно e.
LaTeX
$$$\\mathrm{embeddingsMatrixReindex}(b,e)_{i,j} = (e(j))(b_i)$$$
Lean4
/-- `embeddingsMatrixReindex A C b e : Matrix κ κ C` is the matrix whose `(i, j)` coefficient
is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ` given by a
bijection `e : κ ≃ (B →ₐ[A] C)`. It is mostly useful for fields and `C` is algebraically closed.
In this case, in presence of `h : Fintype.card κ = finrank A B`, one can take
`e := equivOfCardEq ((AlgHom.card A B C).trans h.symm)`. -/
def embeddingsMatrixReindex (b : κ → B) (e : κ ≃ (B →ₐ[A] C)) :=
reindex (Equiv.refl κ) e.symm (embeddingsMatrix A C b)
