## Stream: new members

### Topic: Proving something is a subfield

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 21:21):

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 (Jan 10 2019 at 21:21):

This is what I have:

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 21:21):

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 (Jan 10 2019 at 21:37):

Got it, it's to_is_subring.

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:10):

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

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:10):

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 (Jan 10 2019 at 22:11):

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

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:14):

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,
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 (Jan 10 2019 at 22:15):

What exactly did you write the first time? with to_is_subring

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:15):

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 := {
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 (Jan 10 2019 at 22:22):

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

#### Mario Carneiro (Jan 10 2019 at 22:22):

you have to write @neg_mem h1

#### Mario Carneiro (Jan 10 2019 at 22:24):

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

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:24):

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 (Jan 10 2019 at 22:25):

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

What do you mean?

#### Mario Carneiro (Jan 10 2019 at 22:25):

what do you get when you try it?

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:26):

unknown identifier 'is_subfield.add_mem'

#### Mario Carneiro (Jan 10 2019 at 22:26):

that means it's not called that

#### Mario Carneiro (Jan 10 2019 at 22:27):

what is the def of is_subfield?

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:27):

I tried with is_add_submonoid too.

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:27):

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


#### Mario Carneiro (Jan 10 2019 at 22:27):

you don't pass in h1 at all

I did.

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:28):

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,
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))
}


i know, stop

#### Mario Carneiro (Jan 10 2019 at 22:28):

just call it without passing in h1

Ah.

#### Mario Carneiro (Jan 10 2019 at 22:29):

like is_add_submonoid.add_mem ha1 hb1

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:30):

I see, yes this works.

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:30):

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

#### Mario Carneiro (Jan 10 2019 at 22:31):

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

#### Mario Carneiro (Jan 10 2019 at 22:31):

you can give it if you use @

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:32):

Yes, why wasn't that working?

#### Abhimanyu Pallavi Sudhir (Jan 10 2019 at 22:32):

Using @ and feeding the class?

#### Mario Carneiro (Jan 10 2019 at 22:32):

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

#### Mario Carneiro (Jan 10 2019 at 22:33):

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

#### Mario Carneiro (Jan 10 2019 at 22:34):

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

#### Mario Carneiro (Jan 10 2019 at 22:35):

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 (Jan 10 2019 at 22:36):

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

#### Abhimanyu Pallavi Sudhir (Jan 16 2019 at 19:28):

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 (Jan 16 2019 at 19:46):

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

#### Kevin Buzzard (Jan 16 2019 at 19:46):

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

#### Abhimanyu Pallavi Sudhir (Jan 16 2019 at 19:53):

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 (Jan 16 2019 at 19:53):

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

#### Kevin Buzzard (Jan 16 2019 at 20:04):

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 (Jan 16 2019 at 20:07):

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

#### Abhimanyu Pallavi Sudhir (Jan 16 2019 at 20:07):

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 (Jan 16 2019 at 20:30):

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 (Jan 16 2019 at 20:33):

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)

Last updated: May 10 2021 at 23:11 UTC