mem_range_comap_iff — Mathlib

English

A reformulation: p ∈ range f.specComap iff an appropriate equivalence holds with comaps and maps.

Русский

Переформулировка: p ∈ диапазона f.specComap эквивалентно определенному соответствию с comap и map.

LaTeX

$$$p \\in \\operatorname{range} f.{\\rm specComap} \\iff (p.asIdeal.map f).comap f = p.asIdeal$$$

Lean4

/-- `p` is in the image of `Spec S → Spec R` if and only if `p` extended to `S` and
restricted back to `R` is `p`. -/
theorem mem_range_comap_iff {p : PrimeSpectrum R} : p ∈ Set.range f.specComap ↔ (p.asIdeal.map f).comap f = p.asIdeal :=
  by
  refine ⟨fun ⟨q, hq⟩ ↦ by simp [← hq], ?_⟩
  rw [Ideal.comap_map_eq_self_iff_of_isPrime]
  rintro ⟨q, _, hq⟩
  exact ⟨⟨q, inferInstance⟩, PrimeSpectrum.ext hq⟩

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