isLocallyFraction_pred — Mathlib

English

Alternate formulation of germ-stalk compatibility through Spec and fromSpecStalk constructions.

Русский

Альтернативная формулировка совместимости germ-stalk через конструирования Spec и fromSpecStalk.

LaTeX

$$$\\text{germ}(\\cdot) = \\text{stalkCongr}(\\cdot).hom$$$

Lean4

@[simp]
theorem isLocallyFraction_pred {U : Opens (PrimeSpectrum.Top R)} (f : ∀ x : U, Localizations R x) :
    (isLocallyFraction R).pred f =
      ∀ x : U,
        ∃ (V : _) (_ : x.1 ∈ V) (i : V ⟶ U),
          ∃ r s : R, ∀ y : V, s ∉ y.1.asIdeal ∧ f (i y : U) * algebraMap _ _ s = algebraMap _ _ r :=
  rfl

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