eq_of_fromFunctionField_eq — Mathlib

English

If two rational maps have the same fromFunctionField, then the two maps are equal.

Русский

Если два рациональных отображения имеют одинаковый fromFunctionField, то они равны.

LaTeX

$$$f.fromFunctionField = g.fromFunctionField \Rightarrow f = g$$$

Lean4

theorem eq_of_fromFunctionField_eq [IsIntegral X] (f g : X.RationalMap Y)
    (H : f.fromFunctionField = g.fromFunctionField) : f = g :=
  by
  obtain ⟨f, rfl⟩ := f.exists_rep
  obtain ⟨g, rfl⟩ := g.exists_rep
  refine PartialMap.toRationalMap_eq_iff.mpr ?_
  exact PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H

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