comap — Mathlib

English

Restriction of an infinite place along an embedding defines a corresponding infinite place on the base field.

Русский

Ограничение бесконечного места вдоль вложения задаёт бесконечное место базового поля.

LaTeX

$$$\mathrm{comap}(w,f) = \text{theInfinitePlace on } k \text{ defined by } (f^{-1})^*(w)$$$

Lean4

/-- The restriction of an infinite place along an embedding. -/
def comap (w : InfinitePlace K) (f : k →+* K) : InfinitePlace k :=
  ⟨w.1.comp f.injective, w.embedding.comp f, by { ext x; change _ = w.1 (f x); rw [← w.2.choose_spec]; rfl
  }⟩

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