ext' — Mathlib

English

Two scheme morphisms f,g:X→Y are equal if their associated LRSHom data agree; equivalence of LRSHom components implies equality of morphisms.

Русский

Два морфизма схем равны, если их соответствующие данные LRSHom совпадают; равенство LRSHom-частей влечет равенство морфизмов.

LaTeX

$$f = g := (f.toLRSHom = g.toLRSHom) → f = g$$

Lean4

/-- An alternative ext lemma for scheme morphisms. -/
protected theorem ext' {f g : X ⟶ Y} (h : f.toLRSHom = g.toLRSHom) : f = g := by cases f; cases g; congr 1

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