English
A practical condition for equality of two local-ring-based representations of a morphism X: equality holds iff there exists a coordinate-algebraic relation connecting the two representations via a base change that respects stalk congruence.
Русский
Условия равенства двух представлений морфизма с локальным кольцом: равенство эквивалентно существованию связи между двумя представлениями через базовую смену, сохраняющую конгруэнцию стежки.
LaTeX
$$$f_1 = f_2 \\iff \\exists h_1: f_1.1 = f_2.1,\\; f_1.2.1 = (X.presheaf.stalkCongr (by rw [h_1]; rfl)).hom \\;$$
Lean4
/-- useful lemma for applications of `SpecToEquivOfLocalRing` -/
theorem SpecToEquivOfLocalRing_eq_iff {f₁ f₂ : Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalHom f.hom }} :
f₁ = f₂ ↔ ∃ h₁ : f₁.1 = f₂.1, f₁.2.1 = (X.presheaf.stalkCongr (by rw [h₁]; rfl)).hom ≫ f₂.2.1 :=
by
constructor
· rintro rfl; simp
· obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁
obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂
rintro ⟨rfl : x₁ = x₂, e : f₁ = _⟩
simp [e]
