Zulip Chat Archive

Stream: new members

Topic: Quotients of equivalent things are equivalent


Hanting Zhang (Apr 16 2021 at 22:59):

How could I go about proving something like this?

noncomputable def equiv_quotient_of_eq
  {A : Type u} [group A] {B : Type v} [group B] {A' : subgroup A} {B' : subgroup B}
  [hAN : A'.normal] [hBN : B'.normal] (h' : A' ≃* B') (h : A ≃* B) :
  quotient A' ≃* quotient B' := sorry

I'm having trouble figuring out how to write out the definition of to_fun in mathlib quotient language.

Eric Wieser (Apr 16 2021 at 23:01):

#mwe? What imports / namespace?

Hanting Zhang (Apr 16 2021 at 23:02):

Argggghh sorry

Hanting Zhang (Apr 16 2021 at 23:03):

import group_theory.subgroup
import group_theory.quotient_group
import data.setoid.basic

universes u v
namespace subgroup
open quotient_group

noncomputable def equiv_quotient_of_eq
  {A : Type u} [group A] {B : Type v} [group B] {A' : subgroup A} {B' : subgroup B}
  [hAN : A'.normal] [hBN : B'.normal] (e' : A' ≃* B') (e : A ≃* B) :
  quotient A' ≃* quotient B' :=
{ to_fun := _,
  inv_fun := _,
  left_inv := _,
  right_inv := _,
  map_mul' := _ }

end subgroup

Hanting Zhang (Apr 16 2021 at 23:14):

Wait... maybe this isn't even true.

Eric Wieser (Apr 16 2021 at 23:14):

To channel Kevin Buzzard, "whats the maths proof?"

Eric Wieser (Apr 16 2021 at 23:15):

monoid_hom.to_mul_equiv
  (quotient_group.lift A' _ _)
  (quotient_group.lift B' _ _)
  _
  _

might at least get you over the initial quotient hurdle, but it won't help you with it being false

Hanting Zhang (Apr 16 2021 at 23:16):

It isn't true :hurt:
Taking quotients of Z4×Z2\mathbb Z_4 \times \mathbb Z_2 can yield groups isomorphic to Z4\mathbb Z_4 and Z2×Z2\mathbb Z_2 \times \mathbb Z_2.

Hanting Zhang (Apr 16 2021 at 23:18):

What I really want to do is show that quotient $ ((A' ⊓ B) ⊔ (A ⊓ B')).of (A ⊓ B) is isomorphic to quotient $ ((B' ⊓ A) ⊔ (B ⊓ A')).of (B ⊓ A).

Kevin Buzzard (Apr 17 2021 at 00:08):

You seem to be using different notation to the above. A and B were different groups in the aboveb question but now you're intersecting them

Hanting Zhang (Apr 17 2021 at 03:28):

Ok, my bad.

I was kind of led astray by the two (bad) examples above, but I've reduced my problem to something which looks _very_ true. I just need to be able to define it:

import group_theory.subgroup

def of_eq {G H : Type*} [group G] [group H] (h : G = H) : G ≃* H :=
{ to_fun := λ x, h  x, -- fails :(
  inv_fun := _,
  left_inv := _,
  right_inv := _,
  map_mul' := _ }

What does "eliminator" elaborator failed to compute the motive mean?

As for why I need to do this, the proof for the Zassenhaus lemma uses a symmetry argument which proves that quotient ((A' ⊔ A ⊓ B').of (A' ⊔ A ⊓ B)) and quotient ((B' ⊔ B ⊓ A').of (B' ⊔ B ⊓ A)) are both isomorphic to quotient ((A' ⊓ B ⊔ A ⊓ B').of (A ⊓ B)). With my proofs, the swap between A and B means I also have to prove quotient ((A' ⊓ B ⊔ A ⊓ B').of (A ⊓ B)) = quotient ((B' ⊓ A ⊔ B ⊓ A').of (B ⊓ A). However, this doesn't work because when I try to use this rewrite in my final proof, Lean raises an error that "the type motive is not correct." So instead of rewriting, I want to just use trans with an equiv. Hence where I am now.

Adam Topaz (Apr 17 2021 at 03:47):

(this of_eq is false. Do you see why?)

Hanting Zhang (Apr 17 2021 at 03:52):

Ah, the group structure need not be the same. Well this isn't very exciting.

Mario Carneiro (Apr 17 2021 at 03:59):

It should be the case that group.quotient H ≃* group.quotient H' if H = H' are equal subgroups of the same group. Does this help?

Mario Carneiro (Apr 17 2021 at 04:01):

This also generalizes to something like group.quotient H ->* group.quotient H' if H <= H'

Hanting Zhang (Apr 17 2021 at 04:07):

No, the problem is that I have 4 subgroups of G: H', H, K', K, where H' = K' and H = K. I'm taking quotients of H' in H and K' in K, which means quotient H' and quotient K' are not of the same group. One is of ↥H and another of ↥K. I also can't seem to rewrite these types, as Lean keeps giving me "the type motive is not correct" errors

Hanting Zhang (Apr 17 2021 at 04:08):

Your suggestion is what I tried at first, but I think Lean wants to be convinced that ↥H and ↥K are defeq, which I guess they are not?

Mario Carneiro (Apr 17 2021 at 04:56):

Can you write something with a complete type?

Mario Carneiro (Apr 17 2021 at 04:57):

I'm not sure what "I'm taking quotients of H' in H" means if H' is a subgroup of G

Hanting Zhang (Apr 17 2021 at 05:05):

It looks like this

import group_theory.subgroup
import group_theory.quotient_group
import data.setoid.basic

universes u v
namespace subgroup
variables {α : Type u} [group α]

open quotient_group

def of (H : subgroup α) (K : subgroup α) : subgroup K := H.comap K.subtype

noncomputable def equiv_quotient_of_eq {A' A B' B: subgroup α}
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (h' : A' = B') (h : A = B) :
  quotient (A'.of A) ≃* quotient (B'.of B) := sorry

end subgroup

Mario Carneiro (Apr 17 2021 at 05:08):

What's the quotient relation?

Mario Carneiro (Apr 17 2021 at 05:08):

er I guess that's always left_rel

Hanting Zhang (Apr 17 2021 at 05:11):

Ah sorry, you also need to add (h' : A' = B') and (h : A = B)

Mario Carneiro (Apr 17 2021 at 05:13):

Note that it's always easy to prove theorems like this by "brute force", you just

noncomputable def equiv_quotient_of_eq {A' A B' B: subgroup α}
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal]
  (h' : A' = B') (h : A = B) :
  quotient (A'.of A) ≃* quotient (B'.of B) :=
by unfreezingI { cases h'; cases h; refl }

The trouble is that this definition doesn't compute very well, when you want to know what the isomorphism actually is

Mario Carneiro (Apr 17 2021 at 05:13):

so it's better to use the quotient API to build it instead

Hanting Zhang (Apr 17 2021 at 05:20):

:open_mouth: My goodness. If it's possible, could you explain what is going on in your proof? All my attempts to prove this were met with failure.

What does "brute force" mean here? And what exactly is cases h' breaking down into?

Hanting Zhang (Apr 17 2021 at 05:22):

Trying to build it from the quotient API just makes a horrid mess for me.

Hanting Zhang (Apr 17 2021 at 05:22):

But I don't really know what I'm doing

Mario Carneiro (Apr 17 2021 at 05:29):

The basic principle here is that if x = y then f x = f y, for any f

Mario Carneiro (Apr 17 2021 at 05:30):

In this case f is complicated and dependent, but the theorem is still true. In fact we can prove that the two quotients are =, not just isomorphic

Mario Carneiro (Apr 17 2021 at 05:31):

"brute force" is talking about the fact that this proof doesn't really have anything to do with group theory, it's just using basic logic

Mario Carneiro (Apr 17 2021 at 05:31):

this has some downsides because it is skipping the whole quotient API which means it is tricky to work out what the isomorphism does

Mario Carneiro (Apr 17 2021 at 05:32):

It is still possible to work with this, and it works in a pinch

Hanting Zhang (Apr 17 2021 at 05:36):

I see. Also why does rw h not work, as opposed to cases h? The former produces rewrite tactic failed, motive is not type correct. How is cases h taking the place (?) of rw here?

Hanting Zhang (Apr 17 2021 at 05:39):

My guess is that rw cannot look through the dependent part of f, so it fails. Is this somewhat correct?

Mario Carneiro (Apr 17 2021 at 05:43):

Here's a definition that uses the quotient API (and as a result generalizes to the one-directional version)

def quotient_map_of_le {A' A B' B: subgroup α}
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal]
  (h' : A'  B') (h : A  B) :
  quotient (A'.of A) →* quotient (B'.of B) :=
quotient_group.map _ _ (inclusion h) $
by simp [of, comap_comap]; exact comap_mono h'

def quotient_equiv_of_eq {A' A B' B: subgroup α}
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal]
  (h' : A' = B') (h : A = B) :
  quotient (A'.of A) ≃* quotient (B'.of B) :=
by apply monoid_hom.to_mul_equiv
    (quotient_map_of_le h'.le h.le) (quotient_map_of_le h'.ge h.ge);
  { ext x⟩,
    simp [quotient_map_of_le, quotient_group.map, quotient_group.lift, mk', inclusion],
    refl }

Mario Carneiro (Apr 17 2021 at 05:43):

Yes, the problem with rw is that it gets tripped up by the dependencies. cases h or subst h will make A and A' the same everywhere, so there aren't any type correctness issues

Mario Carneiro (Apr 17 2021 at 05:45):

This fails for your earlier example because even after the cases you will still have inst_1 inst_2 : group A in the context, and the identity function is not a group hom between these (arbitrary) group structures

Hanting Zhang (Apr 17 2021 at 06:02):

Thanks! I am honestly shocked by the conciseness of your proofs. You make it seem so easy...

Hanting Zhang (Apr 17 2021 at 06:02):

I tried using mul_equiv.of_bijective but that went terribly.

Hanting Zhang (Apr 17 2021 at 06:23):

And hooray! I finally have a sorry free proof of the Zassenhaus lemma. It only took 600 lines of code and 5 days. Thank you immensely to @Mario Carneiro for helping me with the tricky parts.


Last updated: Dec 20 2023 at 11:08 UTC