English
For any open U, comap along the identity on U equals the identity map.
Русский
Для любого открытого множества U комап по тождественному отображению внутри U равен тождественному отображению.
LaTeX
$$$(comap (RingHom.id R) U U (\\dots)) = \\text{RingHom.id}$$$
Lean4
/-- The comap of the identity is the identity. In this variant of the lemma, two open subsets `U` and
`V` are given as arguments, together with a proof that `U = V`. This is useful when `U` and `V`
are not definitionally equal.
-/
theorem comap_id {U V : Opens (PrimeSpectrum.Top R)} (hUV : U = V) :
(comap (RingHom.id R) U V fun p hpV => by rwa [hUV, PrimeSpectrum.comap_id]) =
(eqToHom (show (structureSheaf R).1.obj (op U) = _ by rw [hUV])).hom :=
by rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]
