[Merged by Bors] - feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 #16450
Conversation
Paul-Lez
added
the
awaiting-CI
Paul-Lez
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
Paul-Lez
added
WIP
Paul-Lez
added
awaiting-review
|
✌️ Paul-Lez can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
| @@ -999,7 +999,8 @@ symm_bijective.injective $ ext $ λ x, rfl | |||
|
|
|||
| @[simp] theorem refl_symm : (alg_equiv.refl : A₁ ≃ₐ[R] A₁).symm = alg_equiv.refl := rfl | |||
|
|
|||
| @[simp] lemma to_ring_equiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm := rfl | |||
| --this should be a simp lemma but causes a lint timeout | |||
There was a problem hiding this comment.
Have you considered using the new alg_equiv_class?
There was a problem hiding this comment.
Good point, I'll have a look at that!
There was a problem hiding this comment.
@riccardobrasca I had a go at it, would this be the correct statement?
lemma to_ring_equiv_symm {F : Type*} [alg_equiv_class F R A₁ A₂] (f : F) : ((f : A₁ ≃ₐ[R] A₂) : A₁ ≃+* A₁).symm = (f : A₁ ≃ₐ[R] A₂).symm := rfl
There was a problem hiding this comment.
The statement doesn't compile so I'm not sure it's correct, although I think some coercions might be missing since Lean threw me an error when I wrote (f : A₁ ≃ₐ[R] A₂).
There was a problem hiding this comment.
I think the idea of alg_equiv_class is to make this kind of lemmas useless, but I am indeed not sure it can be used here. @Vierkantor what do you think (maybe you also know why simp is causing a timeout)?
There was a problem hiding this comment.
Would it be reasonable to merge this PR so we can then merge #15000 and then fix the lemma in a subsequent PR, or would it be better to do the fix now?
There was a problem hiding this comment.
Yes, I don't see any problem in this.
bors merge
github-actions
bot
removed
the
awaiting-CI
…16450) This PR contains some lemmas that were originally in #15000. The main result that is proven here is `quotient_equiv_quotient_minpoly_map`, which says that if `α` has minimal polynomial `f` over `R` and `I` is an ideal of `R`, then rings `R[α] / I[α]` and `(R/I)[X] / (f mod I)` are isomorphic as R-algebras. Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…16450) This PR contains some lemmas that were originally in #15000. The main result that is proven here is `quotient_equiv_quotient_minpoly_map`, which says that if `α` has minimal polynomial `f` over `R` and `I` is an ideal of `R`, then rings `R[α] / I[α]` and `(R/I)[X] / (f mod I)` are isomorphic as R-algebras. Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>
This PR contains some lemmas that were originally in #15000.
The main result that is proven here is
quotient_equiv_quotient_minpoly_map, which says that ifαhas minimal polynomialfoverRandIis an ideal ofR, then ringsR[α] / I[α]and(R/I)[X] / (f mod I)are isomorphic as R-algebras.Co-authored-by: Anne Baanen vierkantor@vierkantor.com