annihilator_map_mkQ_eq_colon — Mathlib

English

For submodules N ⊆ M, the annihilator of the quotient M/N equals N.colon ⊤, i.e., the set of scalars r that kill the quotient is precisely the set of r for which the action sends M into N.

Русский

Аннигилятороция модуля: аннигилятор фактор-модуля M/N равен N.colon ⊤.

LaTeX

$$$\\operatorname{Ann}_R(M/N) = N : \\top$$$

Lean4

@[simp]
theorem annihilator_map_mkQ_eq_colon : annihilator (P.map N.mkQ) = N.colon P :=
  by
  ext
  rw [mem_annihilator, mem_colon]
  exact
    ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)), fun H _ ⟨p, hp, hpm⟩ ↦
      hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

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