range_asIdeal — Mathlib

English

Let R be a commutative semiring. The image of the maximal-spectrum map asIdeal equals the set of maximal ideals of R.

Русский

Пусть R — коммутативное полукольцо. Образ отображения asIdeal из максимального спектра в множество идеалов совпадает с множеством максимальных идеалов в R.

LaTeX

$$$\operatorname{range}(\mathrm{asIdeal}) = \{ J \in \mathrm{Ideal}(R) \;|\; J \text{ maximal} \}$$$

Lean4

theorem range_asIdeal : Set.range MaximalSpectrum.asIdeal = {J : Ideal R | J.IsMaximal} :=
  Set.ext fun J ↦
    ⟨fun hJ ↦
      let ⟨j, hj⟩ := Set.mem_range.mp hJ;
      Set.mem_setOf.mpr <| hj ▸ j.isMaximal,
      fun hJ ↦ Set.mem_range.mpr ⟨⟨J, Set.mem_setOf.mp hJ⟩, rfl⟩⟩

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