eq_mk' — Mathlib

English

A restatement of germ-stalk compatibility when passing through Spec.map φ and fromSpecStalk, under locality hypotheses.

Русский

Повторное утверждение совместимости germ-stalk при прохождении через Spec.map φ и fromSpecStalk под локальности.

LaTeX

$$$\\text{germ-stalk-compatibility} : \\; \\cdots$$$

Lean4

theorem eq_mk' {U : Opens (PrimeSpectrum.Top R)} {f : ∀ x : U, Localizations R x} (hf : IsFraction f) :
    ∃ r s : R,
      ∀ x : U,
        ∃ hs : s ∉ x.1.asIdeal,
          f x =
            IsLocalization.mk' (Localization.AtPrime _) r (⟨s, hs⟩ : (x : PrimeSpectrum.Top R).asIdeal.primeCompl) :=
  by
  rcases hf with ⟨r, s, h⟩
  refine ⟨r, s, fun x => ⟨(h x).1, (IsLocalization.mk'_eq_iff_eq_mul.mpr ?_).symm⟩⟩
  exact (h x).2.symm

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