comap_surjective — Mathlib

English

The number of infinite places cannot decrease under restriction along a field extension with algebraic embeddings.

Русский

Число бесконечных мест не может уменьшаться при ограничении вдоль расширения поля с алгебраическими вложениями.

LaTeX

$$$ \operatorname{card}(\mathrm{InfinitePlace}(k)) \leq \operatorname{card}(\mathrm{InfinitePlace}(K)) $$$

Lean4

theorem comap_surjective [Algebra k K] [Algebra.IsAlgebraic k K] : Function.Surjective (comap · (algebraMap k K)) :=
  fun w ↦ ⟨(mk (ComplexEmbedding.lift K w.embedding)), by simp⟩

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