restrictScalars_extendScalarsOfIsLocalization

English

Extending scalars then restricting back recovers the original map, i.e., (f.extendScalars...).restrictScalars = f.

Русский

Расширение скаляров, а затем ограничение обратно восстанавливают исходное отображение, то есть (f.extendScalars...).restrictScalars = f.

LaTeX

$$$\\operatorname{restrictScalars}_R\\big(\\operatorname{extendScalarsOfIsLocalization}(f)\\big)=f$$$

Lean4

@[simp]
theorem restrictScalars_extendScalarsOfIsLocalization (f : M →ₗ[R] N) :
    (f.extendScalarsOfIsLocalization S A).restrictScalars R = f :=
  rfl

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