English
There is a canonical equality expressing that the germ composed with the tilde-open localization equals the stalk-identified element; this mirrors the universal property of germs with respect to opens and stalks.
Русский
Существует каноническое равенство, выражающее, что Germ, составленный с open-локализацией tilde, равен элементу, идентифицированному через стэк; это отражает универсальность гема относительно открытий и стэков.
LaTeX
$$$\text{germ}_{U}^{x} \circ (\text{toOpen } M\,U) = (\text{toStalk } M\,x)$$$
Lean4
@[simp]
theorem const_apply (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R))
(hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) (x : U) :
(const M m r U hu).1 x = LocalizedModule.mk m ⟨r, hu x x.2⟩ :=
rfl
