spread_out_unique_of_isGermInjective'

English

A variant: equality of scheme morphisms on stalks implies equality on an open neighborhood.

Русский

Вариант: равенство отображений по стокам влечет за собой равенство на открытом окрестности.

LaTeX

$$$\exists U \; x \in U \land U.ι \circ f = U.ι \circ g$$$

Lean4

/-- A variant of `spread_out_unique_of_isGermInjective`
whose condition is an equality of scheme morphisms instead of ring homomorphisms.
-/
theorem spread_out_unique_of_isGermInjective' {x : X} [X.IsGermInjectiveAt x] (f g : X ⟶ Y)
    (e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g) : ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g :=
  by
  fapply spread_out_unique_of_isGermInjective
  · simpa using congr(($e).base (IsLocalRing.closedPoint _))
  · apply Spec.map_injective
    rw [← cancel_mono (Y.fromSpecStalk _)]
    simpa [Scheme.Spec_map_stalkSpecializes_fromSpecStalk]

Похожие утверждения