[Merged by Bors] - refactor(algebra/algebra/basic): replace algebra.comap with restrict_scalars
#7949
Conversation
hrmacbeth
added
the
awaiting-review
src/algebra/algebra/basic.lean
Outdated
| /-- Identity homomorphism `A →ₐ[S] restrict_scalars R S A`. -/ | ||
| def restrict_scalars.to_restrict_scalars : A →ₐ[S] restrict_scalars R S A := alg_hom.id S A | ||
| /-- Identity homomorphism `restrict_scalars R S A →ₐ[S] A`. -/ | ||
| def restrict_scalars.of_restrict_scalars : restrict_scalars R S A →ₐ[S] A := alg_hom.id S A |
There was a problem hiding this comment.
What's the linear map version of these functions called? It's not clear to me that the alg_hom versions are deserving of the shorter name.
There was a problem hiding this comment.
AFAICT, there was no linear map version, only algebra.comap.to_comap and algebra.to_comap which did different things annoyingly enough.
There was a problem hiding this comment.
I renamed to alg_equiv.self_to_restrict_scalars, feel free to rename.
There was a problem hiding this comment.
@eric-wieser @Vierkantor I noticed that in #7807, the linear equiv version is introduced. It's named restrict_scalars.linear_equiv and goes in the opposite direction, A →ₐ[S] restrict_scalars R S A. So I have changed up the algebra equiv version again to mimick it.
There was a problem hiding this comment.
Thanks! Your choices for what to modify or delete look good to me, though some of the older stuff might be worth polishing as we update it.
Beware that there is a merge conflict with #7807, since both PRs touch the docstrings.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
github-actions
bot
removed
the
merge-conflict
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
…ct_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.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
algebra.comap with restrict_scalarsalgebra.comap with restrict_scalars
The constructions
algebra.comapandrestrict_scalarsare essentially the same thing -- a type synonym to allow one to switch to a smaller scalar field. Previouslyrestrict_scalarswas for modules andalgebra.comapfor algebras; I am unifying them so thatrestrict_scalarsworks for both.Declaration changes:
algebra.comap,algebra.comap.inhabited,is_scalar_tower.comapUse the pre-existing (for modules)
restrict_scalars,restrict_scalars.inhabited,restrict_scalars.is_scalar_toweralgebra.comap.XforXinsemiring,ring,comm_semiring,comm_ring,algebraReplaced with
restrict_scalars.Xalgebra.comap.algebra'Replaced with
restrict_scalars.algebra_orig(to be consistent withrestrict_scalars.module_orig)algebra.comap.to_comapandalgebra.comap.of_comapCombined into an
alg_equivand renamedrestrict_scalars.alg_equiv(to be consistent withrestrict_scalars.linear_equiv)subalgebra.comapReplaced with a generalized version,
subalgebra.restrict_scalars, which (to be consistent withsubmodule.restrict_scalars) applies to anis_scalar_tower, not just to the type synonymDeleted altogether:
algebra.to_comap,algebra.to_comap_applyThis construction is now
(algebra.of_id S (restrict_scalars R S A)).restrict_scalars RIt was only used once in mathlib, where I have replaced it by its definition
alg_hom.comap,alg_equiv.comapThese are not currently used in mathlib but if needed one can instead use
alg_hom.restrict_scalarsandalg_equiv.restrict_scalarsis_scalar_tower.algebra_comap_eqThe proof is now
rfland it was never used in mathlib.It would then be possible, in a follow-up PR, to rename
subalgebra.comap'tosubalgebra.comap, although I have no immediate plans to do this.Zulip