lift_comp_algebraMap — Mathlib

English

The lift is a ring homomorphism from K to ℂ extending φ.

Русский

Поднятие является кольцевым гомоморфизмом K →+* ℂ, расширяющим φ.

LaTeX

$$lift K φ : K →+* ℂ extends φ$$

Lean4

@[simp]
theorem lift_comp_algebraMap [Algebra k K] [Algebra.IsAlgebraic k K] (φ : k →+* ℂ) :
    (lift K φ).comp (algebraMap k K) = φ := by
  unfold lift
  letI := φ.toAlgebra
  rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, RingHom.algebraMap_toAlgebra']

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