isCoatom_ker_of_surjective — Mathlib

English

If f: M → N is surjective and N is simple, then ker f is a coatom in the lattice of submodules.

Русский

Если f: M → N сюръективно и N прост, то ker f — коатом в решетке подмодулей.

LaTeX

$$[IsSimpleModule R N] (f: M → N) ∧ Surjective f ⇒ IsCoatom (ker f).$$

Lean4

theorem isCoatom_ker_of_surjective [IsSimpleModule R N] {f : M →ₗ[R] N} (hf : Function.Surjective f) :
    IsCoatom (LinearMap.ker f) := by
  rw [← isSimpleModule_iff_isCoatom]
  exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)

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