toAlgHom_ofComp_rename — Mathlib

English

A refinement showing that the equality above persists in a base-changed setting with isScalarTower relations.

Русский

Уточнение, сохраняющее равенство в условии базового изменения с учётом отношений IsScalarTower.

LaTeX

$$$ (Q.ofComp P).toAlgHom ((rename Sum.inr) p) = C (algebraMap _ _ p)$$$

Lean4

@[simp]
theorem toAlgHom_ofComp_rename (Q : Generators S T ι') (P : Generators R S ι) (p : P.Ring) :
    (Q.ofComp P).toAlgHom ((rename Sum.inr) p) = C (algebraMap _ _ p) :=
  have :
    (Q.ofComp P).toAlgHom.comp (rename Sum.inr) =
      (IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S) :=
    by ext; simp
  DFunLike.congr_fun this p

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