English
If f, g: X → Y agree on the germ and coincide on stalks, they agree on an open neighborhood of x when X is germ-injective.
Русский
Если f и g согласуются на гера и совпадают на стоке, то они совпадут на открытом окрестности x, когда X germ-injective.
LaTeX
$$$\exists U \; x \in U \land U.ι \circ f = U.ι \circ g$$$
Lean4
/-- Let `x : X` and `f g : X ⟶ Y` be two morphisms such that `f x = g x`.
If `f` and `g` agree on the stalk of `x`, then they agree on an open neighborhood of `x`,
provided `X` is "germ-injective" at `x` (e.g. when it's integral or locally Noetherian).
TODO: The condition on `X` is unnecessary when `Y` is locally of finite type.
-/
@[stacks 0BX6]
theorem spread_out_unique_of_isGermInjective {x : X} [X.IsGermInjectiveAt x] (f g : X ⟶ Y) (e : f.base x = g.base x)
(H : f.stalkMap x = Y.presheaf.stalkSpecializes (Inseparable.of_eq e.symm).specializes ≫ g.stalkMap x) :
∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g :=
by
obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hxV, -⟩ :=
(isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ
have hxV' : g.base x ∈ V := e ▸ hxV
obtain ⟨U, hxU, _, hUV, HU⟩ := X.exists_le_and_germ_injective x (f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V) ⟨hxV, hxV'⟩
refine ⟨U, hxU, ?_⟩
rw [← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_left), ← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)]
congr 1
have : IsAffine V := hV
suffices
∀ (U₀ V₀) (eU : U = U₀) (eV : V = V₀),
f.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_left) = g.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_right)
by
rw [← cancel_mono V.toScheme.isoSpec.hom]
simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality, Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
congr 2
apply this <;> simp
rintro U V rfl rfl
have := ConcreteCategory.mono_of_injective _ HU
rw [← cancel_mono (X.presheaf.germ U x hxU)]
simp only [Scheme.Hom.appLE, Category.assoc, X.presheaf.germ_res', ← Scheme.stalkMap_germ, H]
simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.stalkMap_germ]
