English
If U ⊆ V are opens, the comap along the identity equals the restriction map.
Русский
Для вложения открытых множества жеал комап по тождественному отображению равен ограничению.
LaTeX
$$$(comap (RingHom.id R) U V) = ((structureSheaf R).1.map (i\\!\\! V).op) $$$
Lean4
/-- For an inclusion `i : V ⟶ U` between open sets of the prime spectrum of `R`, the comap of the
identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.
This is a generalization of the fact that, for fixed `U`, the comap of the identity from OO_X(U)
to OO_X(U) is the identity.
-/
theorem comap_id_eq_map (U V : Opens (PrimeSpectrum.Top R)) (iVU : V ⟶ U) :
(comap (RingHom.id R) U V fun _ hpV => leOfHom iVU <| hpV) = ((structureSheaf R).1.map iVU.op).hom :=
RingHom.ext fun s =>
Subtype.eq <|
funext fun p =>
by
rw [comap_apply]
-- Unfortunately, we cannot use `Localization.localRingHom_id` here, because
-- `PrimeSpectrum.comap (RingHom.id R) p` is not *definitionally* equal to `p`. Instead, we use
-- that we can write `s` as a fraction `a/b` in a small neighborhood around `p`. Since
-- `PrimeSpectrum.comap (RingHom.id R) p` equals `p`, it is also contained in the same
-- neighborhood, hence `s` equals `a/b` there too.
obtain ⟨W, hpW, iWU, h⟩ := s.2 (iVU p)
obtain ⟨a, b, h'⟩ := h.eq_mk'
obtain ⟨hb₁, s_eq₁⟩ := h' ⟨p, hpW⟩
obtain ⟨hb₂, s_eq₂⟩ := h' ⟨PrimeSpectrum.comap (RingHom.id _) p.1, hpW⟩
dsimp only at s_eq₁ s_eq₂
erw [s_eq₂, Localization.localRingHom_mk', ← s_eq₁, ← res_apply _ _ _ iVU]
