[Merged by Bors] - feat(field_theory/minimal_polynomial): add algebra_map_inj #5062
Conversation
riccardobrasca
added
the
awaiting-review
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
| /--A minimal polynomial is not a unit.-/ | ||
| /-- If `L/K` is a ring extension, and `x` is an element of `L` in the image of `K`, | ||
| then the minimal polynomial of `x` is `X - C x`. -/ | ||
| lemma algebra_map_inj [nontrivial α] (a : α) (hf : function.injective (algebra_map α β)) |
There was a problem hiding this comment.
This naming surprises me a bit - I'd expect this to be a proof of function.injective (algebra_map α β), not one that takes that as an assumption.
There was a problem hiding this comment.
Perhaps eq_if_algebra_map_inj?
There was a problem hiding this comment.
Ah, I see this matches algebra_map and algebra_map' below.
There was a problem hiding this comment.
I still have some problem with the name convention, so it is probably just my fault...
There was a problem hiding this comment.
I'm inclined to say that we should fix the other names instead. But I don't have a very good suggestion atm.
There was a problem hiding this comment.
It seems Kevin's comment about is_integral α (algebra_map α β a) applies to minimal_polynomial.algebra_map too - it has no need for that condition, right?
There was a problem hiding this comment.
Yes, that's why there is algebra_map'. It is exactly algebra_map without that assumption. We can remove one of them I think.
There was a problem hiding this comment.
Just to clarify: I added inj in the name to distinguish it fromalgebra_map, but the injectivity, although necessary, does not need to appear in the name. Indeed I don't see any concrete situation where one want to speak about a minimal polynomial without the injectivity condition (for example the minimal polynomial is not even unique in that case... something quite weird)
There was a problem hiding this comment.
Perhaps these should be:
minimal_polynomial.eq_X_sub_C_if_algebra_map_inj(currentlyminimal_polynomial.algebra_map_inj)minimal_polynomial.eq_X_sub_C(currentlyminimal_polynomial.algebra_map')- Remove
minimal_polynomial.algebra_mapas the hypothesis is always true
There was a problem hiding this comment.
I think I like that (with _if_ changed to _of_).
jcommelin
added
awaiting-author
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
…thlib into min_poly_alg_map
riccardobrasca
added
awaiting-review
|
I'm still unhappy about those names. But otherwise this looks fine. What do you think of Eric's suggestions? |
|
Now they are |
Vierkantor
added
awaiting-author
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
riccardobrasca
added
awaiting-review
github-actions
bot
added
ready-to-merge
I have added `algebra_map_inj` that computes the minimal polynomial of an element of the base ring. It generalizes `algebra_map` that assumes the base ring to be a field. I left `algebra_map` since I think it is reasonable to have a lemma that works without proving explicitly that the algebra map is injective.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
I have added
algebra_map_injthat computes the minimal polynomial of an element of the base ring. It generalizesalgebra_mapthat assumes the base ring to be a field. I leftalgebra_mapsince I think it is reasonable to have a lemma that works without proving explicitly that the algebra map is injective.