no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ ↑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier
rwa [hUV, PrimeSpectrum.comap_id]
no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ (structureSheaf R).val.obj U.op = (structureSheaf R).val.obj V.op
rw [hUV]
no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ comap (RingHom.id R) U V
      (_ : ∀ (p : ↑(PrimeSpectrum.Top R)), p ∈ V.carrier → p ∈ ↑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier) =
    eqToHom (_ : (structureSheaf R).val.obj U.op = (structureSheaf R).val.obj V.op)
erw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]