coe_smul_primesOver_mk_eq_map_galRestrict

English

There is a natural action of AlgEquiv K L L on the set (p.primesOver B).Elem, defined by σ • Q = primesOver.mk p (map (galRestrict A K L B) σ Q.1, i.e., the action is compatible with the map induced by galRestrict.

Русский

Существует естественное действие AlgEquiv K L L на множество (p.primesOver B).Elem, определяемое σ • Q = primesOver.mk p (map (galRestrict A K L B) σ) Q.1.

LaTeX

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

Lean4

theorem coe_smul_primesOver_mk_eq_map_galRestrict (σ : L ≃ₐ[K] L) (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
    (σ • primesOver.mk p P).1 = map (galRestrict A K L B σ) P :=
  rfl

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