lift — Mathlib

English

The lift composed with the canonical map algebraMap k K equals φ.

Русский

Дополнение lift после algebraMap k K даёт то же отображение φ.

LaTeX

$$(lift K φ) ∘ algebraMap k K = φ$$

Lean4

/-- A (random) lift of the complex embedding `φ : k →+* ℂ` to an extension `K` of `k`.
-/
noncomputable def lift [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) : K →+* ℂ :=
  by
  letI := φ.toAlgebra
  exact (IsAlgClosed.lift (R := k)).toRingHom

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