# Commit 2021-06-16 06:02 690ab173

View on Github →refactor(algebra/algebra/basic): replace `algebra.comap`

with `restrict_scalars`

(#7949)
The constructions `algebra.comap`

and `restrict_scalars`

are essentially the same thing -- a type synonym to allow one to switch to a smaller scalar field. Previously `restrict_scalars`

was for modules and `algebra.comap`

for algebras; I am unifying them so that `restrict_scalars`

works for both.
Declaration changes:

`algebra.comap`

,`algebra.comap.inhabited`

,`is_scalar_tower.comap`

Use the pre-existing (for modules)`restrict_scalars`

,`restrict_scalars.inhabited`

,`restrict_scalars.is_scalar_tower`

`algebra.comap.X`

for`X`

in`semiring`

,`ring`

,`comm_semiring`

,`comm_ring`

,`algebra`

Replaced with`restrict_scalars.X`

`algebra.comap.algebra'`

Replaced with`restrict_scalars.algebra_orig`

(to be consistent with`restrict_scalars.module_orig`

)`algebra.comap.to_comap`

and`algebra.comap.of_comap`

Combined into an`alg_equiv`

and renamed`restrict_scalars.alg_equiv`

(to be consistent with`restrict_scalars.linear_equiv`

)`subalgebra.comap`

Replaced with a generalized version,`subalgebra.restrict_scalars`

, which (to be consistent with`submodule.restrict_scalars`

) applies to an`is_scalar_tower`

, not just to the type synonym Deleted altogether:`algebra.to_comap`

,`algebra.to_comap_apply`

This construction is now`(algebra.of_id S (restrict_scalars R S A)).restrict_scalars R`

It was only used once in mathlib, where I have replaced it by its definition`alg_hom.comap`

,`alg_equiv.comap`

These are not currently used in mathlib but if needed one can instead use`alg_hom.restrict_scalars`

and`alg_equiv.restrict_scalars`

`is_scalar_tower.algebra_comap_eq`

The proof is now`rfl`

and it was never used in mathlib. It would then be possible, in a follow-up PR, to rename`subalgebra.comap'`

to`subalgebra.comap`

, although I have no immediate plans to do this.