English
If the germ map on an affine open is injective, then the germ on any basic open inside it is also injective.
Русский
Если гомоморфизм гера на аффинном открытом множество инъективен, то на любом базовом открытом внутри него тоже инъективен.
LaTeX
$$$\text{If } H : X.presheaf.germ(U,x) \text{ is injective, then } X.presheaf.germ(basicOpen(f),x,...) \text{ is injective.}$$$
Lean4
theorem injective_germ_basicOpen (U : X.Opens) (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) (f : Γ(X, U))
(hf : x ∈ X.basicOpen f) (H : Function.Injective (X.presheaf.germ U x hx)) :
Function.Injective (X.presheaf.germ (X.basicOpen f) x hf) :=
by
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at H ⊢
intro t ht
have := hU.isLocalization_basicOpen f
obtain ⟨t, s, rfl⟩ := IsLocalization.mk'_surjective (.powers f) t
rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem, RingHom.mem_ker,
RingHom.algebraMap_toAlgebra, TopCat.Presheaf.germ_res_apply] at ht
swap; · exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)
rw [H _ ht, IsLocalization.mk'_zero]
