Quotients of equivalent things are equivalent

Stream: new members

[Hanting Zhang]

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]

#mwe? What imports / namespace?

[Hanting Zhang]

Argggghh sorry

[Hanting Zhang]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Hanting Zhang]

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]

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]

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]

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

[Hanting Zhang]

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

[Mario Carneiro]

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]

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

[Hanting Zhang]

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]

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]

Can you write something with a complete type?

[Mario Carneiro]

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

[Hanting Zhang]

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]

What's the quotient relation?

[Mario Carneiro]

er I guess that's always left_rel

[Hanting Zhang]

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

[Mario Carneiro]

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]

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

[Hanting Zhang]

: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]

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

[Hanting Zhang]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

"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]

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]

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

[Hanting Zhang]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Hanting Zhang]

I tried using mul_equiv.of_bijective but that went terribly.

[Hanting Zhang]

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.