[WIP] subgroups and homomorphisms#94
[WIP] subgroups and homomorphisms#94kim-em wants to merge 19 commits intoleanprover-community:masterfrom kim-em:group_theory
Conversation
|
|
||
| theorem inv (a : α) : (f a)⁻¹ = f a⁻¹ := | ||
| inv_eq_of_mul_eq_one $ by simp [(H a a⁻¹).symm, one H] | ||
| @[simp] theorem inv (a : α) : f a⁻¹ = (f a)⁻¹ := |
There was a problem hiding this comment.
We thought the inv theorem was better stated in this direction, as it is telling you how to compute f on the inverse of something, rather than telling you how to compute the inverse of f of something. (That is, it's about the homomorphism, not the group structure.)
|
|
||
| instance comp : is_group_hom (g ∘ f) := { | ||
| hom_mul := λ x y, calc | ||
| g (f (x * y)) = g (f x * f y) : by rw mul f -- Why doesn't `simp` work here? |
There was a problem hiding this comment.
If someone could explain why simp doesn't work here, that would be great.
There was a problem hiding this comment.
As I mention above, the hom theorems can't be simp lemmas because they have nothing to key on - the head of the expression is a variable. You can write simp [mul f, one f] etc though.
| infix * := lcoset | ||
| infix * := rcoset | ||
|
|
||
| end coset_notation |
There was a problem hiding this comment.
This doesn't work. You can't namespace notations in lean 3, and this will ruin multiplication everywhere else. You must use local notation, but then they can't be the same symbol. Try *l and *r or something.
| include w | ||
|
|
||
| theorem mul : ∀ a b : α, f (a * b) = f a * f b := H | ||
| @[simp] theorem mul : ∀ a b : α, f (a * b) = f a * f b := w.hom_mul |
There was a problem hiding this comment.
These can't be simp lemmas, they don't work since f is a variable.
There was a problem hiding this comment.
I wish I understood simp better. I thought that simp was fine with "(precondition) -> X = Y", isn't that what is going on here? forall f, H (saying f is a group hom), a and b, blah?
There was a problem hiding this comment.
The reason why mul won't work (well[1]) as a simp lemma is not because there is a precondition, but because the function symbol f is not a constant (it is a variable here).
The simplifier indexes the available lemmas by the head function symbol of the left-hand side, for example foo 0 = 1 would be indexed by the name foo. If the simplifier then sees a subterm of the form foo (a*b), it will only look for simp lemmas for the name foo and will not find the mul lemma.
[1] I believe that you can use mul as a simp lemma if the homomorphism that you want to rewrite is a local constant, but I haven't tested it.
| def is_group_hom (f : α → β) : Prop := | ||
| ∀ a b : α, f (a * b) = f a * f b | ||
| class is_group_hom (f : α → β) := | ||
| (hom_mul : ∀ a b : α, f (a * b) = f a * f b) |
There was a problem hiding this comment.
Why did you make this a Type? We really want is_* things to be Props
There was a problem hiding this comment.
Turned is_group_hom back into a Prop in ca77526, although this caused two typeclass inference problems I don't understand: see #94 (review).
Style issues hopefully all fixed in 91693ec.
|
|
||
| theorem inv (a : α) : (f a)⁻¹ = f a⁻¹ := | ||
| inv_eq_of_mul_eq_one $ by simp [(H a a⁻¹).symm, one H] | ||
| @[simp] theorem inv (a : α) : f a⁻¹ = (f a)⁻¹ := |
|
|
||
| instance comp : is_group_hom (g ∘ f) := { | ||
| hom_mul := λ x y, calc | ||
| g (f (x * y)) = g (f x * f y) : by rw mul f -- Why doesn't `simp` work here? |
There was a problem hiding this comment.
As I mention above, the hom theorems can't be simp lemmas because they have nothing to key on - the head of the expression is a variable. You can write simp [mul f, one f] etc though.
| exact mul_mem this h, | ||
| simp | ||
| } | ||
| end |
There was a problem hiding this comment.
style: 2 indent spaces, braces on same line
| attribute [simp] subgroup.one_mem | ||
| subgroup.inv_mem | ||
| subgroup.mul_mem | ||
| normal_subgroup.normal |
There was a problem hiding this comment.
I don't think these should be simp lemmas, simp isn't really designed for this sort of thing. If it helps here, use local attribute [simp] instead.
There was a problem hiding this comment.
I've made this local for now, but could just inline them into the simps that use them if that's preferred.
| one_mul := λ ⟨x, hx⟩, subtype.eq $ one_mul x, | ||
| mul_one := λ ⟨x, hx⟩, subtype.eq $ mul_one x, | ||
| inv := λ ⟨x, hx⟩, ⟨x⁻¹, inv_mem hx⟩, | ||
| mul_left_inv := λ ⟨x, hx⟩, subtype.eq $ mul_left_inv x } |
| def trivial (G : Type u) [group G] : set G := {1} | ||
|
|
||
| instance trivial_in : normal_subgroup (trivial G) := | ||
| by refine {..}; simp {contextual := tt} |
There was a problem hiding this comment.
I've given all the instances better names (to me at least; I know people think I name things verbosely) in 808e1a0. (Sorry, that should have been two separate commits.)
| end | ||
|
|
||
| lemma inj_iff_trivial_kernel {f : G → H} [is_group_hom f] : function.injective f ↔ kernel f = trivial G := | ||
| ⟨trivial_kernel_of_inj, inj_of_trivial_kernel⟩ |
There was a problem hiding this comment.
Inline the last two lemmas into this one
| ⟨inv_ker_one, one_ker_inv⟩ | ||
|
|
||
| lemma inv_iff_ker (f : G → H) [w : is_group_hom f] (a b : G) : f a = f b ↔ a * b⁻¹ ∈ kernel f := | ||
| ⟨@inv_ker _ _ _ _ f w _ _, @ker_inv _ _ _ _ f w _ _⟩ -- TODO: I don't understand why I can't just write ⟨inv_ker, ker_inv⟩ here. (This gives typeclass errors; it can't find `w`.) |
There was a problem hiding this comment.
I don't understand why typeclass inference is failing here (after I turned is_group_hom back into a Prop). Help appreciated!
There was a problem hiding this comment.
I think f needs to be explicit in the previous several lemmas. Also none of them should be [simp], for the same reasons as the is_group_hom lemmas: it only works as a simp lemma if the LHS starts with a constant, not f.
There was a problem hiding this comment.
Okay, I've removed all the [simp]s, and made all the fs explicit.
|
|
||
| -- Examples of subgroups | ||
| @[simp] | ||
| def trivial (G : Type u) [group G] : set G := {1} |
There was a problem hiding this comment.
I don't think you want this definition to be [simp], if you intend on using it at all. This will just make it unfold everywhere, making things like trivial_normal useless.
| variables [group G] [group H] | ||
|
|
||
| @[simp] | ||
| def kernel (f : G → H) [is_group_hom f] : set G := preimage f (trivial H) |
| one_mem := ⟨1, one_mem S, one f⟩, | ||
| inv_mem := assume a ⟨b, hb, eq⟩, | ||
| ⟨b⁻¹, inv_mem hb, by rw inv f; simp *⟩ | ||
| } |
There was a problem hiding this comment.
style: braces on same line, before and after. Also leave off the subgroup . if it can be inferred (which should always be the case, assuming you have stated the target type of the theorem).
| end | ||
|
|
||
| lemma inj_iff_trivial_kernel {f : G → H} [w : is_group_hom f] : function.injective f ↔ kernel f = trivial G := | ||
| ⟨@trivial_kernel_of_inj _ _ _ _ f w, @inj_of_trivial_kernel _ _ _ _ f w⟩ -- TODO again, why can't it find w by itself? |
There was a problem hiding this comment.
Make f explicit in this and the last two lemmas, and that should fix your typeclass problem. You may be getting a sense for why I thought making is_group_hom a typeclass doesn't gain you that much, except possibly chains like is_group_hom.comp.
There was a problem hiding this comment.
Unfortunately it doesn't fix it. Commit coming in a moment.
| universes u v | ||
| variables {G : Type u} {H : Type v} | ||
|
|
||
| class subgroup [group G] (S : set G) : Prop := |
There was a problem hiding this comment.
There was a problem hiding this comment.
Thanks Kenny for pointing this out: @johoelzl did this after Mitchell had finished for the summer, and neither of us had seen it in the meantime.
Rather than immediately update this PR so that it uses this code, I'll send an intermediate commit that modifies the existing subgroup.lean so that it uses is_subgroup as a typeclass. After everyone's had a chance to comment on that, I'll "rebase" Mitchell's work onto Johannes's.
…an to use typeclasses
|
I submitted my changes to |
|
|
||
| end add_comm_group | ||
|
|
||
| variables [group α] {β : Type*} [group β] |
There was a problem hiding this comment.
Is there a reason why you want to have it in this order?
Usually the order is: types, type classes instances, values, proofs. This does not always work due to dependencies. But in this case it should be no difference.
There was a problem hiding this comment.
I was just to keep related things together. I have no real sense that this is valuable enough to break the usual ordering you indicated, so I will change it back.
There was a problem hiding this comment.
I think it is a good heuristic to keep types first, as this is often the problem when something can not be inferred.
| def left_coset [has_mul G] (a : G) (S : set G) : set G := image (λ x, a * x) S | ||
| def right_coset [has_mul G] (S : set G) (a : G) : set G := image (λ x, x * a) S | ||
|
|
||
| infix ` *l `:70 := left_coset |
There was a problem hiding this comment.
we have a lot of *x notation nowadays, do we really want to fix this to left and right coset? how about changing this to local infix notation?
There was a problem hiding this comment.
I'll change this to local. (I think Mario earlier suggested the same, sorry for missing it.)
|
|
||
| instance center_normal : normal_subgroup (center G) := { | ||
| one_mem := by simp [center], | ||
| mul_mem := begin |
There was a problem hiding this comment.
begin should be at the next line, and the list of tactic calls inside indented by 2.
And everywhere further down too.
|
Hi Scott, I have a couple of stylistic fixes. If you want I can merge this pull request and do the changes myself. |
|
@johoelzl, that would be great! I will read your fixes afterwards. |
|
Closed with fa86d34. I squashed your commits into one. |
This is some basic material on finite group theory, done by my student Mitchell Rowett in January.
There's also some further material on quotient groups, and the first isomorphism theorem, which can follow in a later PR.