algebraMap_galRestrict_apply — Mathlib

English

Let σ be a K-algebra automorphism of L, and let x be an element of B. Then the embedding of B into L, followed by restricting through galRestrict, commutes with applying σ to the embedding of B into L.

Русский

Пусть σ — автоморфизм K-алгебр поля L, а x ∈ B. Тогда отображение B → L далее через galRestrict, совместимо с применением σ к отображению B → L.

LaTeX

$$$\\text{For every }(\\sigma : L \\simeq_{\\text{alg},K} L)\\,(x \\in B),\\quad \\mathrm{algebraMap}_{B,L}(\\,galRestrict\\,A K L B \\ σ\\ x) = σ\\bigl(\\mathrm{algebraMap}_{B,L}(x)\\bigr) $$$

Lean4

theorem algebraMap_galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) :
    algebraMap B L (galRestrict A K L B σ x) = σ (algebraMap B L x) :=
  algebraMap_galRestrictHom_apply A K L B σ.toAlgHom x

Похожие утверждения