English
If the germ of a section is a unit in every stalk on a cover, then the section is a unit globally.
Русский
Если каждый росток секции является единицей в касательном пространстве на покрытии, то секция является единицей глобально.
LaTeX
$$$\forall x,\; IsUnit( germ_x(f) ) \Rightarrow IsUnit(f)$$
Lean4
/-- If the germ of a section `f` is a unit in the stalk at `x`, then `f` must be a unit on some small
neighborhood around `x`.
-/
theorem isUnit_res_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U)) (x : X) (hx : x ∈ U)
(h : IsUnit (X.presheaf.germ U x hx f)) : ∃ (V : Opens X) (i : V ⟶ U) (_ : x ∈ V), IsUnit (X.presheaf.map i.op f) :=
by
obtain ⟨g', heq⟩ := h.exists_right_inv
obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.germ_exist x g'
let W := U ⊓ V
have hxW : x ∈ W := ⟨hx, hxV⟩
replace heq :
(X.presheaf.germ _ x hxW) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) =
(X.presheaf.germ _ x hxW) 1 :=
by
rwa [map_mul, map_one, X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,
X.presheaf.germ_res_apply (Opens.infLERight U V) x hxW g]
obtain ⟨W', hxW', i₁, i₂, heq'⟩ := X.presheaf.germ_eq x hxW hxW _ _ heq
use W', i₁ ≫ Opens.infLELeft U V, hxW'
simp only [map_mul, map_one] at heq'
simpa using isUnit_of_mul_eq_one _ _ heq'
