[Merged by Bors] - feat(ring_theory/algebraic): alg_hom from an algebraic extension to itself is bijective

[alreadydone]

• Generalizes alg_hom.bijective and alg_equiv_equiv_alg_hom and move them so that they can be derived from the generalized versions. Upgrade alg_equiv_equiv_alg_hom to a mul_equiv by introducing the monoid instance alg_hom.End on self-alg_homs.

• Show that algebraicity of an algebra is preserved under alg_equiv (alg_equiv.is_algebraic_iff).

Zulip

---

[linesthatinterlace]

Suggested change

	λ x hx, begin
	rw [mem_root_set_iff' hp, ← f.comp_algebra_map, ← map_map, eval_map],
	erw [eval₂_hom, (mem_root_set_iff' (λ h, _) x).1 hx],
	{ apply _root_.map_zero },
	rw [← f.comp_algebra_map, ← map_map, h] at hp,
	exact hp (polynomial.map_zero f),
	end
	λ x, begin
	have H : map (algebra_map T S) p ≠ 0,
	{ contrapose! hp,
	rw [← f.comp_algebra_map, ← map_map, hp, polynomial.map_zero] },
	simp_rw [mem_root_set_iff' hp, mem_root_set_iff' H, eval_map, ← alg_hom_eval₂_algebra_map],
	exact λ hx, hx.symm ▸ f.map_zero
	end

It's possible that the have here should be a lemma? If we don't already have it (it seems simple!)

[tb65536]

Does polynomial.map_ne_zero help?

[alreadydone]

I golfed the proof further down to three lines. polynomial.map_ne_zero is for maps out of a division ring to a nontrivial target, where we have injectivity, so it doesn't help here (we doesn't even assume T is a domain).

Here we derives p.map (algebra_map T S) ≠ 0 from p.map (algebra_map T S') ≠ 0 from the existence of an alg_hom f, which is sort of "comap_ne_zero f`. I think this is the lemma @linesthatinterlace suggest that we extract, but it seems no other theorems in the same file can benefit from this, so I'd rather not.

[riccardobrasca]

Suggested change

	def alg_equiv_equiv_alg_hom (ha : algebra.is_algebraic K L) : (L ≃ₐ[K] L) ≃ (L →ₐ[K] L) :=
	@[simps] def alg_equiv_equiv_alg_hom (ha : algebra.is_algebraic K L) : (L ≃ₐ[K] L) ≃ (L →ₐ[K] L) :=

Also, can you prove that this equiv respects composition (it is a monoid equiv, but L →ₐ[K] L doesn't seem to be a monoid)?

[alreadydone]

I've introduced alg_hom.End by copying alg_equiv.aut and showed this is a mul_equiv. Moreover I moved the finite_dimensional case to this file but kept the original names. Let's see if CI passes!

[alreadydone]

Alright CI passed. @riccardobrasca Can you check if you're happy with the new changes? Due to the upgrade from equiv to mul_equiv I have to insert .to_equiv at two occasions in galois.lean. Moreover one proof in an apparently unrelated file broke and I'm not sure why ...

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests