English
If X is irreducible and germ-injective at x, two X-partial maps f,g whose stalks agree are equivalent.
Русский
Если X неразложимо и гема инъективна в x, то две частичные карты f,g совпадающие на стоках эквивалентны.
LaTeX
$$$ \\text{equiv\_of\_fromSpecStalkOfMem\_eq} [IrreducibleSpace X] \\ x, f, g, h := \\; f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg \\Rightarrow f.equiv g$$
Lean4
theorem equiv_of_fromSpecStalkOfMem_eq [IrreducibleSpace X] {x : X} [X.IsGermInjectiveAt x] (f g : X.PartialMap Y)
(hxf : x ∈ f.domain) (hxg : x ∈ g.domain) (H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg) : f.equiv g :=
by
have hdense : Dense ((f.domain ⊓ g.domain) : Set X) := f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2
have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι) (x := ⟨x, hxf, hxg⟩)).mp ‹_›
have :=
spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme) (X.homOfLE inf_le_left ≫ f.hom)
(X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
· obtain ⟨U, hxU, e⟩ := this
refine
⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense ⟨_, ⟨_, hxU, rfl⟩⟩,
((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]
simp only [restrict_hom, ← Category.assoc] at e ⊢
convert e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp
· rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩, ←
g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H
simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv, restrict_hom,
Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H
