coe_smul_primesOver_eq_map_galRestrict

English

For σ in Aut_K(L) and P a prime over p in B, the image of P under σ corresponds to the map galRestrict A K L B applied to P; i.e., (σ • primesOver mk p P).1 = map (galRestrict A K L B σ) P.

Русский

Для σ ∈ Aut_K(L) и P – простой над p в B, образ P во всей системе соответствует отображению galRestrict A K L B σ: (σ • primesOver.mk p P).1 = map (galRestrict A K L B σ) P.

LaTeX

$$$(\\sigma \\cdot (\\text{primesOver.mk } p\\; P)).1 = \\mathrm{map}(\\mathrm{galRestrict}\\ A\\ K\\ L\\ B\\ \\sigma)\\; P$$

Lean4

theorem coe_smul_primesOver_eq_map_galRestrict (σ : L ≃ₐ[K] L) (P : primesOver p B) :
    (σ • P).1 = map (galRestrict A K L B σ) P :=
  rfl

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