[Merged by Bors] - feat(data/equiv): define ring_equiv_class
#11977
Conversation
Vierkantor
added
awaiting-review
| ext, | ||
| exact congr_fun w a, | ||
| end | ||
| fun_like.coe_injective | ||
|
|
||
| instance has_coe_to_ring_equiv : has_coe (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂) := ⟨alg_equiv.to_ring_equiv⟩ |
There was a problem hiding this comment.
You can get rid of this one by adding the has_coe_t F (A₁ ≃+* A₂) instance from ring_equiv_class.
There was a problem hiding this comment.
I'd prefer to do so in a separate PR, since reviewing/debugging coercions is quite a bit harder than reviewing the new class.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
| @@ -382,7 +382,7 @@ begin | |||
| (mv_polynomial.map_surjective f.to_ring_hom hf_surj).comp (alg_equiv.surjective _), | |||
| ideal.fg_ker_comp _ _ _ _ (alg_equiv.surjective _)⟩, | |||
| { convert submodule.fg_bot, | |||
| exact ring_hom.ker_coe_equiv _, }, | |||
| exact ring_hom.ker_coe_equiv (mv_polynomial.sum_alg_equiv R ι ι').to_ring_equiv }, | |||
There was a problem hiding this comment.
The unifier had issues here because the goal contained (coe : alg_hom → ring_hom) sum_alg_equiv.to_alg_hom which had to be unified with (coe : ring_equiv → ring_hom) sum_alg_equiv.to_ring_equiv. Apparently the new generic coercion to ring_hom deriving from ring_equiv.ring_hom_class makes this unification slightly too hard without this hint.
In any case, we should be able to fix the requirement for unification entirely by generalizing ker to a ring_hom_class.
github-actions
bot
removed
the
awaiting-CI
|
Thanks! |
github-actions
bot
added
ready-to-merge
This PR applies the morphism class pattern to `ring_equiv`, producing a new `ring_equiv_class` extending `mul_equiv_class` and `add_equiv_class`. It also provides a `ring_equiv_class` instance for `alg_equiv`s. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
ring_equiv_classring_equiv_class
This PR applies the morphism class pattern to
ring_equiv, producing a newring_equiv_classextendingmul_equiv_classandadd_equiv_class. It also provides aring_equiv_classinstance foralg_equivs.