toExtensionHom — Mathlib

English

There is a construction that turns a map between generators f: P→P' into a map between their extensions, giving a morphism P.toExtension.Hom P'.toExtension.

Русский

Существует конструкция, превращающая отображение между порождающими f: P→P' в отображение между их расширениями, образующая морфизм P.toExtension.Hom P'.toExtension.

LaTeX

$$$\\text{toExtensionHom}:\\ (P.Hom\,P')\\to (P.toExtension.Hom\,P'.toExtension)$$$

Lean4

/-- Reinterpret a hom between generators as a hom between extensions. -/
@[simps]
noncomputable def toExtensionHom [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') :
    P.toExtension.Hom P'.toExtension where
  toRingHom := f.toAlgHom.toRingHom
  toRingHom_algebraMap x := by simp
  algebraMap_toRingHom x := by simp

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