relation_mem_ker — Mathlib

English

The map of ker is surjective and identifies the composed kernel with the image of the original kernel under the ofComp map.

Русский

Карта ядра сюръективна и идентифицирует составное ядро с образом исходного ядра под отображением ofComp.

LaTeX

$$$\\ker( Q\\!\\ofComp\\!P ) = \\text{image of }\\ker(Q)\\text{ under }(Q.toComp P)$$$

Lean4

theorem relation_mem_ker (i) : P.relation i ∈ P.ker :=
  by
  rw [← P.span_range_relation_eq_ker]
  apply Ideal.subset_span
  use i

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