English
The basic open associated to a section f is the set of points where the germ of f is a unit.
Русский
Базовое открытое, связанное с секцией f, состоит из точек, где росток f является единицей.
LaTeX
$$$\text{basicOpen}(f) = \{ x \\mid IsUnit( germ_x(f) ) \}$$$
Lean4
/-- The basic open of a section `f` is the set of all points `x`, such that the germ of `f` at
`x` is a unit.
-/
def basicOpen {U : Opens X} (f : X.presheaf.obj (op U)) : Opens X
where
carrier := {x : X | ∃ (hx : x ∈ U), IsUnit (X.presheaf.germ U x hx f)}
is_open' := by
rw [isOpen_iff_forall_mem_open]
rintro x ⟨hxU, hx⟩
obtain ⟨V, i, hxV, hf⟩ := X.isUnit_res_of_isUnit_germ U f x hxU hx
use V.1
refine ⟨?_, V.2, hxV⟩
intro y hy
use i.le hy
convert RingHom.isUnit_map (X.presheaf.germ _ y hy).hom hf
exact (X.presheaf.germ_res_apply i y hy f).symm
