AKS E and field hom injective

[metakunt]

Show that both field homomorphisms and the AKS subset definition of E is injective.

[tirix]

This is a very good candidate for being moved to main, so let's look closely at the wording and the label !

There is a discussion in #3054 about how to name and describe injections. It seems we reserve "monomorphism" in set.mm to monomorphisms of categories. I think here we would rather say "injective homomorphism", and use the f1 label suffix. @benjub @jkingdon What's your opinion?

[metakunt]

I've changed the label to be consistent with other labels. fld for field hm for homomorphism and f1 for injective function. What do you think about it?

Also the reason that I'm proving this is I need the Frobenius automorphism. You have proved that it is a ring hom.

[tirix]

Yes, the new label fldhmf1 looks good to me! Let's see what others think.

[jkingdon]

Seems like a good label.

In the comment I would change that sends 1 to 1 to that sends the multiplicative identity to the multiplicative identity assuming that is what 1 is supposed to mean here. Or if it is supposed to be a reference to -1-1-> that would call for a different rewording.

[benjub]

I don't know for the label. I would write the second sentence: "This comes from the fact that a ring morphism is unital." (The name of the property you're looking for is "unital".)

But... a ring morphism is unital and need not be injective ! So, why single out that property as the cause of injectivity ?

Note that you only need that the codomain be a nonzero ring. That is a worthy addition, from which you can then deduce the field morphism result.

[metakunt]

Back in linear algebra we had 3 different characterisations of field homomorphisms.
Definition was a field homomorphism f: K->L that satisfies one of the equivalent formulations
1: Sends 1 to 1,
2: f(K) not equal to {0}
3. f injective.

I think for algebraic closures I'll define them by choosing all by the map

$$AlgCl = ( k \in Fld \mapsto \{ w \in Fld | \forall p \in w[X] (deg(p)\in \mathbb{N} => \exists r\in w: p(r)=0)\land \exists f: k\to w, f RingHom, f \text{injective}\} )$$

I don't know yet the definition of algebraic closures, but I want to build on the api. I'll postulate as an axiom that the algebraic closure exists so that I can eliminate the hypotheses since the construction is out of reach for now.

Also I need the Frobenius automorphism on the algebraic closure of $$\mathbb{F}_p$$, @tirix has already proven that it is a ring hom, I've proven injectivity, surjectivity will follow by the property in AlgCl.

[icecream17]

I think the new label is good, and I agree with it being a candidate for main

[metakunt]

Ah @tirix I think I need https://us.metamath.org/mpeuni/ply1fermltl.html over any field of characteristic p. How would I modify/apply your theorem?

[tirix]

For any field (actually, a commutative ring is enough) of prime characteristic, the theorem needs to be rewritten in the more general context. I've done that in #4548.