hom_ext_of_forall — Mathlib

English

Two morphisms f,g:X→Y are equal if for every x in X there exists an open cover revealing equality of restrictions.

Русский

Две морфизмы f,g: X → Y равны, если для каждого точки x существует открытое покрытие, где их ограничения совпадают.

LaTeX

$$$$ \forall x \in X, \exists U \subseteq X, x \in U, U.ι \;\Rightarrow\; U.ι \circ f = U.ι \circ g \implies f=g. $$$$

Lean4

theorem hom_ext_of_forall {X Y : Scheme} (f g : X ⟶ Y) (H : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ U.ι ≫ f = U.ι ≫ g) :
    f = g := by
  choose U hxU hU using H
  let 𝒰 : X.OpenCover :=
    { I₀ := X, X i := (U i), f i := (U i).ι,
      mem₀ := by
        rw [presieve₀_mem_precoverage_iff]
        refine ⟨fun x ↦ ⟨x, by simpa using hxU x⟩, inferInstance⟩ }
  exact 𝒰.hom_ext _ _ hU

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