R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ (p : ↑(PrimeSpectrum.Top S)), p ∈ V → ↑(PrimeSpectrum.comap f) p ∈ U
hVW : ∀ (p : ↑(PrimeSpectrum.Top P)), p ∈ W → ↑(PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj U.op)
p : { x // x ∈ W.op.unop }
⊢ ↑(Localization.localRingHom (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal (↑p).asIdeal (RingHom.comp g f)
          (_ :
            (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal =
              (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal))
      (↑s
        { val := ↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p,
          property := (_ : ↑(PrimeSpectrum.comap f) (↑(PrimeSpectrum.comap g) ↑p) ∈ U) }) =
    ↑(↑(RingHom.comp (comap g V W hVW) (comap f U V hUV)) s) p
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ (p : ↑(PrimeSpectrum.Top S)), p ∈ V → ↑(PrimeSpectrum.comap f) p ∈ U
hVW : ∀ (p : ↑(PrimeSpectrum.Top P)), p ∈ W → ↑(PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj U.op)
p : { x // x ∈ W.op.unop }
⊢ ↑(↑(comap (RingHom.comp g f) U W
              (_ :
                ∀ (p : ↑(PrimeSpectrum.Top P)),
                  p ∈ W.carrier → ↑(PrimeSpectrum.comap f) (↑(PrimeSpectrum.comap g) p) ∈ U))
          s)
      p =
    ↑(↑(RingHom.comp (comap g V W hVW) (comap f U V hUV)) s) p
rw [comap_apply]
no goals
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ (p : ↑(PrimeSpectrum.Top S)), p ∈ V → ↑(PrimeSpectrum.comap f) p ∈ U
hVW : ∀ (p : ↑(PrimeSpectrum.Top P)), p ∈ W → ↑(PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj U.op)
p : { x // x ∈ W.op.unop }
⊢ ↑(Localization.localRingHom (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal (↑p).asIdeal (RingHom.comp g f)
          (_ :
            (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal =
              (↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p).asIdeal))
      (↑s
        { val := ↑(PrimeSpectrum.comap (RingHom.comp g f)) ↑p,
          property := (_ : ↑(PrimeSpectrum.comap f) (↑(PrimeSpectrum.comap g) ↑p) ∈ U) }) =
    ↑(↑(RingHom.comp (comap g V W hVW) (comap f U V hUV)) s) p
erw [Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal] <;>
rfl