galRestrict_symm_algebraMap_apply

English

Let σ be a K-algebra automorphism of L and x ∈ B. Then applying galRestrict with the inverse automorphism and then algebraMap yields the same as applying algebraMap to x and then σ.

Русский

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

LaTeX

$$$\\forall (σ : L \\simeq_{\\text{Alg},K} L)\\ (x : B),\\; (galRestrict A K L B).symm σ\\bigl(\\mathrm{algebraMap}_{B,L}(x)\\bigr) = \\mathrm{algebraMap}_{B,L}(σ\\,x)$$$

Lean4

theorem galRestrict_symm_algebraMap_apply (σ : B ≃ₐ[A] B) (x : B) :
    (galRestrict A K L B).symm σ (algebraMap B L x) = algebraMap B L (σ x) :=
  galRestrictHom_symm_algebraMap_apply A K L B σ x

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