map_baseChange — Mathlib

English

If g is a map of algebras A → B over a base S, then the map induced by g commutes with base change: (W.baseChange A).map g = W.baseChange B.

Русский

Если g — отображение алгебр A → B над основанием S, то отображение, индуцированное g, commute с базовой сменой: (W.baseChange A).map g = W.baseChange B.

LaTeX

$$$ (W.baseChange A).map g = W.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] (g : A →ₐ[S] B) :
    (W.baseChange A).map g = W.baseChange B :=
  congr_arg W.map <| g.comp_algebraMap_of_tower R

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