English
Composition of generator-homs is compatible with extension: toExtensionHom(f ∘ g) = (toExtensionHom f) ∘ (toExtensionHom g).
Русский
Сведение отображений между порождающими к отображениям между расширенными объектами сохраняет композицию: toExtensionHom(f ∘ g) = toExtensionHom(f) ∘ toExtensionHom(g).
LaTeX
$$$\\text{toExtensionHom}(f\\circ g) = \\text{toExtensionHom}(f)\\circ \\text{toExtensionHom}(g)$$$
Lean4
@[simp]
theorem toExtensionHom_comp [Algebra R S'] [IsScalarTower R S S'] [Algebra R R''] [Algebra R S'']
[IsScalarTower R R'' S''] [IsScalarTower R S S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S'']
[IsScalarTower S S' S''] [IsScalarTower R R' R''] [IsScalarTower R R' S'] (f : P'.Hom P'') (g : P.Hom P') :
toExtensionHom (f.comp g) = f.toExtensionHom.comp g.toExtensionHom := by ext; simp
