coeff_zero_of_isScalarTower — Mathlib

English

Under an IsScalarTower of algebras, the constant term maps coherently with the composed maps: algebraMap(B,C)(algebraMap(A,B)(p.coeff 0)) = (mapAlg A C p).coeff 0.

Русский

При IsScalarTower константное слагаемое согласуется через композицию отображений: algebraMap(B,C)(algebraMap(A,B)(p.coeff 0)) = (mapAlg A C p).coeff 0.

LaTeX

$$$$ (\mathrm{algebraMap}\ B C)((\mathrm{algebraMap}\ A B)(p.\coeff 0)) = (\mathrm{mapAlg}\ A C\ p).\coeff 0.$$$$

Lean4

theorem coeff_zero_of_isScalarTower (p : A[X]) :
    (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = (mapAlg A C p).coeff 0 :=
  by
  have h : algebraMap A C = (algebraMap B C).comp (algebraMap A B) :=
    by
    ext a
    simp [Algebra.algebraMap_eq_smul_one, RingHom.coe_comp, Function.comp_apply]
  rw [mapAlg_eq_map, coeff_map, h, RingHom.comp_apply]

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