coe_smul_primesOver_mk — Mathlib

English

Let p be an ideal of A and P a prime ideal of B lying over p. For every σ in G, the prime of B lying over p obtained by applying σ to the canonical prime over p, corresponds to the prime P acted on by σ; i.e., the underlying component is preserved by this action: (σ • primesOver.mk p P).1 = σ • P.

Русский

Пусть p – идеал A, P – простый идеал B, лежащий над p. Для любого σ из G соответствующий элемент primesOver под действием σ соответствует образу P под σ; т. е. основание модуля сохраняется под действием действия: (σ • primesOver.mk p P).1 = σ • P.

LaTeX

$$$(\\sigma \\cdot \\text{primesOver.mk } p\\; P).1 = \\sigma \\cdot P$$$

Lean4

@[simp]
theorem coe_smul_primesOver_mk (σ : G) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : (σ • primesOver.mk p P).1 = σ • P :=
  rfl

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