Algebra: subring which is a field. How to use mathlib4?

Stream: new members

[Michał Staromiejski]

Hi everyone, I'm new here.
So far I was learning Lean 4 by going through tutorials, then decided to try to code some proofs from my publications.
It was going quite well until I got stuck with the following problem (I reduced it to MWE).
I need to show that if a ring homomorphism from a subring that is a field to a field maps an element a to 0 then a = 0. There is map_eq_zero for GroupWithZero that is used to also prove that any ring homomorphism from a field to a non-trivial ring is injective so I tried to use it:

import Mathlib.Algebra.Field.Basic
import Mathlib.Algebra.Ring.Subring.Basic
import Mathlib.Algebra.GroupWithZero.Units.Lemmas -- map_eq_zero

-- this works:
theorem t1 {F K : Type u} [Field F] [Field K]
    {f : F →+* K} {a : F} (ha : f a = 0) : a = 0 :=
  (map_eq_zero f.toMonoidWithZeroHom).mp ha

-- this does not work
-- error: failed to synthesize MonoidWithZeroHomClass (↥S →*₀ K) (↥S) K
theorem t2 {R K : Type u} [CommRing R] [Field K] {S : Subring R} [Field S]
    {f : S →+* K} {a : S} (ha : f a = 0) : a = 0 :=
  (map_eq_zero f.toMonoidWithZeroHom).mp ha

Any help would be very much appreciated.

[Daniel Weber]

What do you mean by "subring which is a field"? Isn't that just a subfield? Note that if you have both S : Subring R and Field S then you have a diamond, as there are two instances of addition and multiplication on the type S - the instances from the Field instances, and the instances from the CommRing instance of R, and there is no relation between them

[Kevin Buzzard]

Field S means "choose an arbitrary field structure on S, unrelated to the ring structure coming from R", and this is what gives you the incomprehensible error message. Change Field S to IsField S and you should be OK (you'll need to import Algebra.Field.IsField).

[Michał Staromiejski]

@Daniel Weber Somehow for me, when one says "subfield", it means a subfield of a field. What I mean is that I have a ring R and a subring S of R that I can show is a field.
@Kevin Buzzard Thanks a lot! In the MWE it works, will try it in the main code.

Thanks for clarification!

[Michał Staromiejski]

@Kevin Buzzard I think I was too fast, didn't see another error. Is this what you mean by using IsField:

import Mathlib.Algebra.Field.Basic
import Mathlib.Algebra.Field.IsField
import Mathlib.Algebra.Ring.Subring.Basic
import Mathlib.Algebra.GroupWithZero.Units.Lemmas

theorem t2 {R K : Type u} [CommRing R] [Field K] {S : Subring R} (hS : IsField S)
    {f : S →+* K} {a : S} (ha : f a = 0) : a = 0 :=
  (map_eq_zero f.toMonoidWithZeroHom).mp ha

It still says failed to synthesize MonoidWithZeroHomClass (↥S →*₀ K) (↥S) K and failed to synthesize GroupWithZero ↥S...

[Eric Wieser]

This works:

theorem t2 {R K : Type u} [CommRing R] [Field K] {S : Subring R} (hS : IsField S)
    {f : S →+* K} {a : S} (ha : f a = 0) : a = 0 :=
  letI := hS.toField
  (map_eq_zero f.toMonoidWithZeroHom).mp ha

[Michał Staromiejski]

Indeed! Thanks a lot @Eric Wieser, works also in my code. I think the lesson for me is to be careful with have and let, I used have _ : Field S := (<proof of IsField S>).toField, after switching to let _ : Field S := ... it works.

[Eric Wieser]

Right: IsField.toField constructs a field that is compatible with the ring structure, but if you use have then Lean isn't allowed to know that.

[Eric Wieser]

(let vs letI doesn't really matter here, that was just me being lazy)