Random intermediate_field.adjoin question

Stream: Berkeley Lean Seminar

[Patrick Lutz]

Do we know that an $F$-algebra homomorphism on $F(S)$ is determined by its action on $S$? For example do we have a lemma saying that if $E/F$ is a field extension with $F(S) = \top$ and if $f$ is an $F$-algebra automorphism of $E$ then $f$ is the identity if and only if it's the identity on $S$? For some reason I feel like we should have something like this but I don't see it

[Thomas Browning]

I've needed this too. I don't think that we have it.

[Thomas Browning]

A while ago I defined an equalizer subalgebra which allows you to do this for subalgebras

[Thomas Browning]

Could we define an equalizer intermediate field?

[Thomas Browning]

I guess, if E/F is a field extension and if you have two F-algebra homomorphisms E->A, then the equalizer is an intermediate field?

[Patrick Lutz]

yeah, I guess that's true

[Patrick Lutz]

actually I think I might really want it for subalgebras not intermediate fields. Since I guess most of the stuff in splitting_field.lean is about algebra adjoin not intermediate field adjoin

[Patrick Lutz]

is there a lemma saying exactly what I said above for subalgebras? (I realize it's pretty easy to prove using the equalizer but if it's already there I don't want to redo it)

[Thomas Browning]

I would guess that it's not stated explicitly for subalgebra adjoin

[Thomas Browning]

It would be a good lemma

[Thomas Browning]

It doesn't seem like it's in ring_theory/adjoin, which would be the natural place

[Patrick Lutz]

Actually, do you know why the gc and gi instances on algebra.adjoin are protected?

[Thomas Browning]

no, although there is api at the top of ring_theory/adjoin

[Thomas Browning]

adjoin_le_iff, for example

[Patrick Lutz]

actually, here's a possibly stupid question: does mathlib know that two algebra isomorphisms are equal if and only if they are equal as algebra homomorphisms?

[Thomas Browning]

not sure. it's a one-liner using the ext-lemmas though

[Patrick Lutz]

Thomas Browning said:

not sure. it's a one-liner using the ext-lemmas though

hmm, for me it's a very slow one-liner using simp and a faster two-linear using simp only with a bunch of little lemmas thrown in

[Patrick Lutz]

maybe "very" is an exaggeration

[Thomas Browning]

example {R A B : Type*} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
  (f g : A ≃ₐ[R] B) : f = g ↔ f.to_alg_hom = g.to_alg_hom :=
⟨λ h, by rw h, λ h, alg_equiv.ext $ λ x, alg_hom.ext_iff.mp h x⟩