Stream: new members

Topic: problem trying to prove instance comm_group

Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:20):

I am a total Lean newbie, so maybe I am trying something too advanced, but anyway: I was trying to prove that a normal subgroup of a group is a commutative group. I am running into some problem with coercions (or my understanding of type classes is wrong, I can't quite tell). What I tried is this:

import group_theory.subgroup

variables (G : Type*) [group G]

instance normal_subgroup_is_comm_group (s: set G) [normal_subgroup s] : comm_group s := {
mul_comm := begin
-- here * is not expanded
rintros ⟨a, ha⟩ ⟨b, hb⟩,
simp, -- can't simplify the definition of *, for some reason?!
sorry,
end,
mul_assoc := begin -- part of ..subtype.group, but I include it to show the difference to mul_comm
-- here the definition of * from subtype.monoid (via subtype.group) is used
rintros ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩,
simp, -- simplifies the definition of * just fine
exact mul_assoc a b c,
end,
..subtype.group
}


Kevin Buzzard (Jun 12 2020 at 18:23):

One issue here is the fact that it's not true that an arbitrary normal subgroup of an arbitrary group is always commutative.

Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:23):

that would be a problem ;-)

Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:24):

but I still don't understand why the first simp doesn't manage to expand *

Kevin Buzzard (Jun 12 2020 at 18:24):

In fact I think this might be the only issue, you seem to have proved associativity just fine

Kevin Buzzard (Jun 12 2020 at 18:25):

I get unknown identifier 'normal_subgroup'. I'm using today's mathlib. -- Aah, I need to add import deprecated.subgroup

Kevin Buzzard (Jun 12 2020 at 18:28):

So your goal is ⊢ ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨b, hb⟩ * ⟨a, ha⟩ and simp doesn't do anything -- I don't understand the question. You want to change it to a * b = b * a? This works:

        rintros ⟨a, ha⟩ ⟨b, hb⟩,
change (⟨a * b, _⟩ : s) = ⟨b * a, _⟩,
simp,


Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:29):

I don't understand why the second simp does something, and the first doesn't

Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:36):

But anyway, change helped me already, thanks

Johan Commelin (Jun 12 2020 at 18:43):

@Carl Friedrich Bolz-Tereick Are you thinking of "a subgroup of a commutative group is always normal"?

Carl Friedrich Bolz-Tereick (Jun 12 2020 at 18:47):

no, I arrived at this mathematically wrong example above while trying to reduce more and more what I actually tried to prove, which is that the center of a division_ring is a comm_ring. with kevin's hint I now managed to do that. I don't completely understand how the change tactic he proposed works, though

Kevin Buzzard (Jun 12 2020 at 18:50):

The second simp doesn't do anything useful. * is notation for has_mul.mul which simp has changed to the definitionally equal group.mul.

Kevin Buzzard (Jun 12 2020 at 18:51):

If the goal is X then change Y will successfully change the goal to Y if and only if X and Y are definitionally equal.

thanks

Bryan Gin-ge Chen (Jun 12 2020 at 18:59):

Here's the tactic doc: tactic#change

Carl Friedrich Bolz-Tereick (Jun 13 2020 at 06:48):

and I managed to show that the center of a division_ring is a field, which is what I originally wanted to try :-). the proof is pretty hairy though, need to simplify it

Last updated: May 10 2021 at 19:16 UTC