English
If f is a unit in every stalk on a cover, then f is a unit on the entire space.
Русский
Если f является единицей во всех ростках на покрытии, то f единица на всём пространстве.
LaTeX
$$$\exists \{V_i\}, \big( \forall i, IsUnit (germ_{V_i}(f))\big) \Rightarrow IsUnit(f\text{ on X})$$$
Lean4
/-- If a section `f` is a unit in each stalk, `f` must be a unit. -/
theorem isUnit_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U))
(h : ∀ (x) (hx : x ∈ U), IsUnit (X.presheaf.germ U x hx f)) : IsUnit f := by
-- We pick a cover of `U` by open sets `V x`, such that `f` is a unit on each `V x`.
choose V iVU m h_unit using fun x : U => X.isUnit_res_of_isUnit_germ U f x x.2 (h x.1 x.2)
have hcover : U ≤ iSup V := by
intro x hxU
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe, Subtype.exists]
tauto
-- Let `g x` denote the inverse of `f` in `U x`.
choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)
have ic : IsCompatible (sheaf X).val V g := by
intro x y
apply section_ext X.sheaf (V x ⊓ V y)
rintro z ⟨hzVx, hzVy⟩
rw [germ_res_apply, germ_res_apply]
apply (h z ((iVU x).le hzVx)).mul_right_inj.mp
rw [← germ_res_apply X.presheaf (iVU x) z hzVx f]
-- Porting note: change was not necessary in Lean3
change
X.presheaf.germ _ z hzVx _ * (X.presheaf.germ _ z hzVx _) =
X.presheaf.germ _ z hzVx _ * X.presheaf.germ _ z hzVy (g y)
rw [← RingHom.map_mul, hg x, germ_res_apply X.presheaf _ _ _ f, ← germ_res_apply X.presheaf (iVU y) z hzVy f, ←
RingHom.map_mul, (hg y), RingHom.map_one, RingHom.map_one]
-- We claim that these local inverses glue together to a global inverse of `f`.
obtain ⟨gl, gl_spec, -⟩ :
-- We need to rephrase the result from `HasForget` to `CommRingCat`.
∃ gl : X.presheaf.obj (op U), (∀ i, ((sheaf X).val.map (iVU i).op) gl = g i) ∧ _ :=
X.sheaf.existsUnique_gluing' V U iVU hcover g ic
apply isUnit_of_mul_eq_one f gl
apply X.sheaf.eq_of_locally_eq' V U iVU hcover
intro i
change ((sheaf X).val.map (iVU i).op).hom (f * gl) = ((sheaf X).val.map (iVU i).op) 1
rw [RingHom.map_one, RingHom.map_mul, gl_spec]
exact hg i
