substAlgHom_comp_substAlgHom — Mathlib

English

The composition of two substAlgHoms, restricted to scalars, equals the substAlgHom of the composed substitution.

Русский

Сведение подстановок AlgHom через ограничения скаляров эквивалентно подстановке, соответствующей композиции подстановок.

LaTeX

$$$((\operatorname{substAlgHom} hb).\mathrm{restrictScalars}\, R)\circ (\operatorname{substAlgHom} ha) = \operatorname{substAlgHom}(ha.comp hb)$$$

Lean4

theorem substAlgHom_comp_substAlgHom (ha : HasSubst a) (hb : HasSubst b) :
    ((substAlgHom hb).restrictScalars R).comp (substAlgHom ha) = substAlgHom (ha.comp hb) :=
  by
  letI : UniformSpace R := ⊥
  letI : UniformSpace S := ⊥
  letI : UniformSpace T := ⊥
  apply comp_aeval (R := R) (ε := (substAlgHom hb).restrictScalars R) ha.hasEval
  simpa [AlgHom.coe_restrictScalars'] using continuous_subst (R := S) hb

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