Proving something is a subfield

Stream: new members

[Abhimanyu Pallavi Sudhir]

I'm trying to prove that the intersection of two subfields is a subfield -- the problem with using subfield.mk, or just using {...} directly, is that subfield is defined using extends, so I need to prove that it's a subring -- and by extension that it is an additive subgroup and a submonoid. What's the notation for this?

[Abhimanyu Pallavi Sudhir]

This is what I have:

[Abhimanyu Pallavi Sudhir]

import algebra.field
import field_theory.subfield
theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) :=
{   --do I need to put something here?
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

[Abhimanyu Pallavi Sudhir]

Got it, it's to_is_subring.

[Abhimanyu Pallavi Sudhir]

Ok, I suppose one could do without that, too.

[Abhimanyu Pallavi Sudhir]

theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) := {
    zero_mem := and.intro h1.zero_mem h2.zero_mem,
    one_mem := and.intro h1.one_mem h2.one_mem,
    add_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro
        (by {have k := h1.add_mem, exact @k a b ha1 hb1})
        (by {have k := h2.add_mem, exact @k a b ha2 hb2}),
    mul_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro
        (by {have k := h1.mul_mem, exact @k a b ha1 hb1})
        (by {have k := h2.mul_mem, exact @k a b ha2 hb2}),
    neg_mem := λ a ⟨ha1, ha2⟩, and.intro
        (by {have k := h1.neg_mem, exact @k a ha1})
        (by {have k := h2.neg_mem, exact @k a ha2}),
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

[Abhimanyu Pallavi Sudhir]

I got confused because Lean doesn't point out which fields are to be provided when something extends something.

[Abhimanyu Pallavi Sudhir]

On a related note, why doesn't this work?

theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) := {
    zero_mem := and.intro h1.zero_mem h2.zero_mem,
    one_mem := and.intro h1.one_mem h2.one_mem,
    add_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro (h1.add_mem ha1 hb1) (h2.add_mem ha2 hb2),
    mul_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro (h1.mul_mem ha1 hb1) (h2.mul_mem ha2 hb2),
    neg_mem := λ a ⟨ha1, ha2⟩, and.intro (h1.neg_mem ha1) (h2.neg_mem ha2),
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

Or even this:

theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) := {
    zero_mem := and.intro h1.zero_mem h2.zero_mem,
    one_mem := and.intro h1.one_mem h2.one_mem,
    add_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro (@h1.add_mem a b ha1 hb1) (@h2.add_mem a b ha2 hb2),
    mul_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro (@h1.mul_mem ha1 hb1) (@h2.mul_mem a b ha2 hb2),
    neg_mem := λ a ⟨ha1, ha2⟩, and.intro (@h1.neg_mem a ha1) (@h2.neg_mem a ha2),
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

One has to do a have statement and then construct the statement with the local instance of neg_mem, etc. Why?

[Reid Barton]

What exactly did you write the first time? with to_is_subring

[Abhimanyu Pallavi Sudhir]

Oh, I just nested them all in:

theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) := {
    to_is_subring := {
        to_is_add_subgroup := {
            to_is_add_submonoid := {
                zero_mem := and.intro h1.zero_mem h2.zero_mem,
                add_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro
                    (by {have k := h1.add_mem, exact @k a b ha1 hb1})
                    (by {have k := h2.add_mem, exact @k a b ha2 hb2}),
            },
            neg_mem := λ a ⟨ha1, ha2⟩, and.intro
                (by {have k := h1.neg_mem, exact @k a ha1})
                (by {have k := h2.neg_mem, exact @k a ha2}),
            },
        to_is_submonoid := {
            one_mem := and.intro h1.one_mem h2.one_mem,
            mul_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro
                (by {have k := h1.mul_mem, exact @k a b ha1 hb1})
                (by {have k := h2.mul_mem, exact @k a b ha2 hb2}),
        },
    },
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

[Mario Carneiro]

@h1.neg_mem doesn't work because you can't mix field notation and @ notation

[Mario Carneiro]

you have to write @neg_mem h1

[Mario Carneiro]

also you shouldn't project out of a typeclass argument, because it's implicit

[Abhimanyu Pallavi Sudhir]

Re:(@,.) -- I thought so, but I tried that and it doesn't work either -- it just doesn't find is_subfield.neg_mem

[Abhimanyu Pallavi Sudhir]

also you shouldn't project out of a typeclass argument, because it's implicit

What do you mean?

[Mario Carneiro]

what do you get when you try it?

[Abhimanyu Pallavi Sudhir]

unknown identifier 'is_subfield.add_mem'

[Mario Carneiro]

that means it's not called that

[Mario Carneiro]

what is the def of is_subfield?

[Abhimanyu Pallavi Sudhir]

I tried with is_add_submonoid too.

[Abhimanyu Pallavi Sudhir]

type mismatch at application
  is_add_submonoid.add_mem
term
  h1
has type
  is_subfield F1 : Type
but is expected to have type
  Type ? : Type (?+1)

[Mario Carneiro]

you don't pass in h1 at all

[Abhimanyu Pallavi Sudhir]

I did.

[Abhimanyu Pallavi Sudhir]

This is what I'm trying:

theorem field_intersect (F1 F2 : set K) [h1 : is_subfield F1] [h2 : is_subfield F2] : is_subfield (F1 ∩ F2) := {
    zero_mem := and.intro h1.zero_mem h2.zero_mem,
    one_mem := and.intro h1.one_mem h2.one_mem,
    add_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro ((@is_add_submonoid.add_mem h1) a b ha1 hb1) (@h2.add_mem a b ha2 hb2),
    mul_mem := λ a b ⟨ha1, ha2⟩ ⟨hb1, hb2⟩, and.intro (@h1.mul_mem ha1 hb1) (@h2.mul_mem a b ha2 hb2),
    neg_mem := λ a ⟨ha1, ha2⟩, and.intro (@h1.neg_mem a ha1) (@h2.neg_mem a ha2),
    inv_mem := (λ x ⟨hx1, hx2⟩, and.intro (is_subfield.inv_mem hx1) (is_subfield.inv_mem hx2))
}

[Mario Carneiro]

i know, stop

[Mario Carneiro]

just call it without passing in h1

[Abhimanyu Pallavi Sudhir]

Ah.

[Mario Carneiro]

like is_add_submonoid.add_mem ha1 hb1

[Abhimanyu Pallavi Sudhir]

I see, yes this works.

[Abhimanyu Pallavi Sudhir]

But why? What's wrong with trying to feed Lean the class?

[Mario Carneiro]

the class is implicit, you aren't supposed to give it, lean finds it by typeclass inference

[Mario Carneiro]

you can give it if you use @

[Abhimanyu Pallavi Sudhir]

Yes, why wasn't that working?

[Abhimanyu Pallavi Sudhir]

Using @ and feeding the class?

[Mario Carneiro]

that should work, you just need a few more arguments that way, like the types

[Mario Carneiro]

I guess it looks something like @is_add_submonoid.add_mem F1 h1 a b ha1 hb1

[Mario Carneiro]

oh wait, no it should be something more complicated than just h1 there

[Mario Carneiro]

because h1 is a is_subfield and it needs a is_add_monoid, it does some typeclass inference to fill the gap

[Abhimanyu Pallavi Sudhir]

Oh ok. I think I see why it's best to leave things to Lean's class inference.

[Abhimanyu Pallavi Sudhir]

I'm proving a similar theorem and having the same problem again, except this time just leaving Lean to do its type class inference doesn't work (only zero_mem and one_mem work):

variables {K L : Type} [discrete_field K] [discrete_field L] (f : K → L)
theorem field_intersect' (PL : set (set L)) [H : ∀ J ∈ PL, is_subfield J] : is_subfield (set.sInter PL) :=
{   zero_mem := by { simp, exact λ J HJ, (H J HJ).zero_mem },
    one_mem := by { simp, exact λ J HJ, (H J HJ).one_mem },
    add_mem := by { simp, exact λ a b ha hb J HJ, is_add_submonoid.add_mem (ha J HJ) (hb J HJ) },
    mul_mem := by { simp, exact λ a b ha hb J HJ, is_submonoid.mul_mem (ha J HJ) (hb J HJ) },
    neg_mem := by { simp, exact λ a h J HJ, is_add_subgroup.neg_mem (h J HJ) },
    inv_mem := by { simp, exact λ a h J HJ, is_subfield.inv_mem (h J HJ) } }

It worked with set.Inter:

theorem field_intersect (Fi : ι → set K) [hi : ∀ i, is_subfield (Fi i)] : is_subfield (set.Inter Fi) :=
{   zero_mem := by { simp, exact λ i, (hi i).zero_mem },
    one_mem := by { simp, exact λ i, (hi i).one_mem },
    add_mem := by { simp, exact λ a b ha hb i, is_add_submonoid.add_mem (ha i) (hb i) },
    mul_mem := by { simp, exact λ a b ha hb i, is_submonoid.mul_mem (ha i) (hb i) },
    neg_mem := by { simp, exact λ a h i, is_add_subgroup.neg_mem (h i) },
    inv_mem := by { simp, exact λ a h i, is_subfield.inv_mem (h i) } }

[Kevin Buzzard]

Can you post working code so I can cut and paste?

[Kevin Buzzard]

PS this "simp, ..." style is discouraged. There are always ways around it.

[Abhimanyu Pallavi Sudhir]

import algebra.field
import field_theory.subfield
import data.polynomial
variables {K L : Type} [discrete_field K] [discrete_field L] (f : K → L)
theorem field_intersect' (PL : set (set L)) [H : ∀ J ∈ PL, is_subfield J] : is_subfield (set.sInter PL) :=
{   zero_mem := by { simp, exact λ J HJ, (H J HJ).zero_mem },
    one_mem := by { simp, exact λ J HJ, (H J HJ).one_mem },
    add_mem := by { simp, exact λ a b ha hb J HJ, is_add_submonoid.add_mem (ha J HJ) (hb J HJ) },
    mul_mem := by { simp, exact λ a b ha hb J HJ, is_submonoid.mul_mem (ha J HJ) (hb J HJ) },
    neg_mem := by { simp, exact λ a h J HJ, is_add_subgroup.neg_mem (h J HJ) },
    inv_mem := by { simp, exact λ a h J HJ, is_subfield.inv_mem (h J HJ) } }

[Abhimanyu Pallavi Sudhir]

Doesn't that work (for copy-pasting, I mean)?

[Kevin Buzzard]

import field_theory.subfield

variables {K L : Type} [discrete_field K] [discrete_field L] (f : K → L)
theorem field_intersect' (PL : set (set L)) [H : ∀ J ∈ PL, is_subfield J] : is_subfield (set.sInter PL) :=
{   zero_mem := λ J HJ, (H J HJ).zero_mem,
    one_mem := λ J HJ, (H J HJ).one_mem,
    add_mem := λ a b ha hb J HJ, let X := (H J HJ).add_mem in X (ha J HJ) (hb J HJ),
    mul_mem := sorry,
    neg_mem := sorry,
    inv_mem := sorry,
}

You don't need simp for stuff like this, you can just spell it out. Although I struggled with add_mem and I don't know why, it's something to do with classes that I don't understand properly.

[Abhimanyu Pallavi Sudhir]

Yeah, the simp was a legacy from my code for field_intersect with indexed subsets.

[Abhimanyu Pallavi Sudhir]

Interesting that the let ... in thing works, though -- I did notice that going have the add_mem statement (without feeding it any parameters) in tactic mode worked.

[Patrick Massot]

This is pretty weird. A more understandable solution would be λ a b ha hb J HJ, by haveI := H J HJ ; exact is_add_submonoid.add_mem (ha J HJ) (hb J HJ),

[Patrick Massot]

Of course you can also use the ugly direct term @is_add_submonoid.add_mem _ _ _ (H J HJ).to_is_add_submonoid _ _ (ha J HJ) (hb J HJ)