EtaleCohomology.exists_zariski_neighborhood_sections_eq_of_etale_map_eq
Equality after restriction to an étale neighborhood gives equality on an actual open neighborhood of each point in its image.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory TopologicalSpace Opposite
namespace EtaleCohomologyLean source · statement
theorem exists_zariski_neighborhood_sections_eq_of_etale_map_eq
{X : Scheme.{u}} (F : Sheaf X.smallEtaleTopology (Type u))
(U : X.Opens) (a b : F.obj.obj (op ((zariskiToEtale X).obj U)))
(V : X.Etale) (g : V ⟶ (zariskiToEtale X).obj U)
(hab : F.obj.map g.op a = F.obj.map g.op b) (v : V.left) :
∃ (W : X.Opens) (hWU : W ≤ U), V.hom v ∈ W ∧
F.obj.map ((zariskiToEtale X).map (homOfLE hWU)).op a =
F.obj.map ((zariskiToEtale X).map (homOfLE hWU)).op b