lift_unique — Mathlib

English

Let hg be injective on A → L, and f any hom K → L that agrees with g on algebraMap A K. Then the lift is equal to f.

Русский

Пусть hg инъективно продолжает g через A в L, и f — любой гомоморфизм K → L, который совпадает с g на algebraMap A K. Тогда этот лифт равен f.

LaTeX

$$$ (\forall x : A, f(\operatorname{algebraMap} A K x) = g x) \Rightarrow \mathrm{IsFractionRing.lift}(hg) = f $$$

Lean4

theorem lift_unique (hg : Function.Injective g) {f : K →+* L} (hf1 : ∀ x, f (algebraMap A K x) = g x) :
    IsFractionRing.lift hg = f :=
  IsLocalization.lift_unique _ hf1

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