R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
⊢ toOpen R ⊤ ≫ germ (structureSheaf R).val ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑⊤) }) x) = toStalk R ↑x
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
⊢ toOpen R U ≫ germ (Sheaf.presheaf (structureSheaf R)) x = toStalk R ↑x
rw [← toOpen_res R ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]
no goals
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
⊢ toOpen R ⊤ ≫ germ (structureSheaf R).val ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑⊤) }) x) = toStalk R ↑x
rfl