map_baseChange — Mathlib

English

The base change construction is compatible with maps: for ψ, the map of the base-changed objects equals the base change of the map.

Русский

Базовая смена совместима с отображениями: для ψ отображение базовой смены равно базовой смене отображения.

LaTeX

$$$$ (C.baseChange\, A).map(\psi) = C.baseChange(B) $$$$

Lean4

@[simp]
theorem map_baseChange {S : Type s} [CommRing S] [Algebra R S] {A : Type v} [CommRing A] [Algebra R A] [Algebra S A]
    [IsScalarTower R S A] {B : Type w} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (ψ : A →ₐ[S] B) :
    (C.baseChange A).map ψ = C.baseChange B :=
  congr_arg C.map <| ψ.comp_algebraMap_of_tower R

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