mathlib

690ab173 - refactor(algebra/algebra/basic): replace `algebra.comap` with `restrict_scalars` (#7949)

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.