map_baseChange — Mathlib

English

Compatibility of map with base change: applying map after baseChange equals baseChange after map with the appropriate extensions.

Русский

Совместимость отображения с базовым изменением: применение map после baseChange равно baseChange после map в соответствующих расширениях.

LaTeX

$$$\mathrm{map}\_{W'} f (\mathrm{baseChange}\_F K P) = \mathrm{baseChange}\_F L (\mathrm{map}\_{W'} f P)$$$

Lean4

theorem map_baseChange [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalarTower R F L] (f : K →ₐ[F] L)
    (P : W'⟮F⟯) : map f (baseChange F K P) = baseChange F L P :=
  by
  have : Subsingleton (F →ₐ[F] L) := inferInstance
  convert map_map (Algebra.ofId F K) f P

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