restrictScalarsId'App_hom_naturality

English

The inverse component is natural with respect to φ: restrictScalarsId'App f hf).inv maps compatibly with (restrictScalars f).map φ.

Русский

Обратная компонента естественна по отношению к φ: inv ограничений совместима с отображением φ.

LaTeX

$$$ (\restrictScalarsId'App f hf).inv.naturality(\varphi). $$$

Lean4

@[reassoc]
theorem restrictScalarsId'App_hom_naturality {M N : ModuleCat R} (φ : M ⟶ N) :
    (restrictScalars f).map φ ≫ (restrictScalarsId'App f hf N).hom = (restrictScalarsId'App f hf M).hom ≫ φ :=
  (restrictScalarsId' f hf).hom.naturality φ

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