Commit 2021-06-16 06:02 690ab173

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.