Zulip Chat Archive

Stream: new members

Topic: Difficulty with `exists`


view this post on Zulip Hanting Zhang (Apr 16 2021 at 06:28):

Hi,

This is a long #mwe; I've shorten as much of it as possible while trying to keep all the important things, although please ask if something seems to be missing. I'm trying to prove the Zassenhaus butterfly lemma, and I've run into some problems while trying to work with the construction of the isomorphisms. Here we have AAA' \trianglelefteq A and BBB' \trianglelefteq B as subgroups of α\alpha. The first step is to construct a map A(AB)(AB)/(AB)(AB)A' (A \sqcap B) \to (A \sqcap B) / (A' \sqcap B)(A \sqcap B'). This is Zassenhaus_fun . Normally the definition goes something like: "Let axA(AB)ax \in A' (A \sqcap B) for aAa \in A' and xABx \in A \sqcap B. Map axax to xDxD, where D=(AB)(AB)D = (A' \sqcap B)(A \sqcap B'). This is well-defined because blah blah..."

This is done as λ x, quotient.mk' ⟨_, ((mem_mul (Zassenhaus_aux B hA)).mp x.2).some_spec.some_spec.2.1⟩. (This is very ugly and I would be happy to know if there was a better way to do it.) But I settled on it and tried to move on with the next part of the proof, which is showing that the kernel of the map is A(AB)A' (A \sqcap B'). The inclusion A(AB)kerfA' (A \sqcap B') \subseteq \ker f is supposed to be obvious: axax is mapped to xD=DxD = D, since xx is annihilated.

Now the problem: To invoke the factorization of axax from a generic term of A(AB)A'(A \sqcap B), I have to use mem_mul . However, this only gives me xABx \in A \sqcap B and loses the information that xABx \in A \sqcap B'. In my code, this happens exactly as I define X : ↥(A ⊓ B). How should I retain the membership information? I want to use the h hypothesis, but it turns out that doing so yields an error where the type of my proofs don't match, and I can't convert my goal. (I can also post the code for my other attempts.)

Also, I'm wondering if this is an #xy problem. Is my entire way of approaching this wrong? How should I think to proceed?

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

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

/- View `H` as a subgroup of `K`. -/
def of (H : subgroup α) (K : subgroup α) : subgroup K := H.comap K.subtype

lemma mem_of (H : subgroup α) (K : subgroup α) (h : K) : h  H.of K  K.subtype h  H  K := sorry

lemma mem_of_subset {x : α} {H K : subgroup α} (hK : H  K) (h : x  H) : x  K := sorry

lemma mem_mul {G : Type u} [group G] {H K : subgroup G} {g : G} (h : (H  K) = (H : set G) * K) :
  g  H  K   x y, x  H  y  K  x * y = g := sorry

lemma Zassenhaus_subgroup {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  : ((A'  B)  (A  B')  A  B) :=
sup_le (inf_le_inf hA (le_refl _)) (inf_le_inf (le_refl _) hB)

instance Zassenhaus1 {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] : (((A'  B)  (A  B')).of (A  B)).normal :=
sorry

def Zassenhaus_quot {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :=
quotient_group.quotient $ ((A'  B)  (A  B')).of (A  B)

instance Zassenhaus_group {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] : group (Zassenhaus_quot hA hB) :=
by { dsimp [Zassenhaus_quot], haveI := subgroup.Zassenhaus1 hA hB, apply_instance }

lemma Zassenhaus_aux {A' A : subgroup α} (B : subgroup α) (hA : A'  A) [hAN : (A'.of A).normal] :
  (A'  A  B) = (A' : set α) * (A  B : subgroup α) := sorry

noncomputable def Zassenhaus_fun {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] : (A'  A  B) →* (Zassenhaus_quot hA hB) :=
{ to_fun := λ x, quotient.mk' _, ((mem_mul (Zassenhaus_aux B hA)).mp x.2).some_spec.some_spec.2.1⟩,
  map_one' := sorry,
  map_mul' := sorry }

lemma Zassenhaus_fun_ker (A' A B' B : subgroup α) (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  (Zassenhaus_fun hA hB).ker = (A'  A  B').of (A'  A  B) :=
begin
  ext ax,
  refine λ h, _, λ h, _⟩,
  { sorry },
  rw monoid_hom.mem_ker,
  dsimp [Zassenhaus_fun],
  refine quot.sound _,
  simp [mem_of] at h,
  have split_ax := ((mem_mul (Zassenhaus_aux B hA)).mp ax.2),
  let X : (A  B) := split_ax.some_spec.some, split_ax.some_spec.some_spec.2.1⟩,
  suffices hm : X⁻¹ * 1  ((A'  B  A  B').of (A  B)),
  exact hm,
  sorry
end

end subgroup

view this post on Zulip Hanting Zhang (Apr 16 2021 at 06:38):

Here is the version where I do use h, for more context.

lemma Zassenhaus_fun_ker (A' A B' B : subgroup α) (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  (Zassenhaus_fun hA hB).ker = (A'  A  B').of (A'  A  B) :=
begin
  ext ax,
  refine λ h, _, λ h, _⟩,
  { sorry },
  rw monoid_hom.mem_ker,
  dsimp [Zassenhaus_fun],
  refine quot.sound _,
  simp [mem_of] at h,
  rcases ((mem_mul (Zassenhaus_aux B' hA)).mp h) with a, x, ha, hx, hax⟩,
  -- Here `hx` is the correct membership proof that `x ∈ A ⊓ B'`.
  have hx' := mem_of_subset (inf_le_inf (le_refl A) hB) hx, -- I can upgrade it to `x ∈ A ⊓ B`,
  have X : (A  B) := x, hx'⟩, -- And use it to construct `X`,
  suffices h : X⁻¹ * 1  ((A'  B  A  B').of (A  B)), -- But now it fails :(
  exact h,
  sorry
end

view this post on Zulip Mario Carneiro (Apr 16 2021 at 06:47):

Given your definitions, one thing that might be useful to prove is H.of K = (H ⊓ K).of K. Then, given x \in H.of K, you can manufacture a bit of extra information about it before the quotient

view this post on Zulip Mario Carneiro (Apr 16 2021 at 06:50):

How is Zassenhaus_aux proven?

view this post on Zulip Hanting Zhang (Apr 16 2021 at 06:58):

Like this:

lemma Zassenhaus_aux {A' A : subgroup α} (B : subgroup α) (hA : A'  A) [hAN : (A'.of A).normal] :
  (A'  A  B) = (A' : set α) * (A  B : subgroup α) :=
normal_subgroup_mul A' A (A  B) hA (inf_le_left_of_le (le_refl A))

The statement of normal_subgroup_mul is:

lemma normal_subgroup_mul (A' A B : subgroup α) (hA : A'  A) [hN : (A'.of A).normal] (hB : B  A) :
  ((A'  B : subgroup α) : set α) = A' * B := sorry

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:00):

And normal_subgroup_mul?

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:00):

I'm wondering where the existential came from

view this post on Zulip Hanting Zhang (Apr 16 2021 at 07:01):

Sorry, like this:

lemma normal_subgroup_mul (A' A B : subgroup α) (hA : A'  A) [hN : (A'.of A).normal] (hB : B  A) :
  ((A'  B : subgroup α) : set α) = A' * B :=
begin
  suffices h : ((A'  B).of A : set A) = A'.of A * B.of A,
  simp only [of, coe_comap, coe_subtype] at h,
  apply_fun set.image (coe : A  α) at h,
  nth_rewrite 3  coe_subtype at h,
  nth_rewrite 3  coe_subtype at h,
  rw  preimage_mul_of_injective at h,
  simp only [subtype.image_preimage_coe, set_like.mem_coe, coe_subtype] at h,
  change ((A'  B : subgroup α) : set α)  A = A' * B  A at h,
  rw set.inter_eq_self_of_subset_left at h,
  rwa set.inter_eq_self_of_subset_left at h,
  rw  set.le_eq_subset,
  have : A' * B  A * A := set.mul_subset_mul hA hB,
  rw coe_mul_self_eq at this,
  exact this,
  exact sup_le hA hB,
  exact subtype_injective A,
  simp only [ monoid_hom.coe_range, subtype_range],
  exact hA,
  simp only [ monoid_hom.coe_range, subtype_range],
  exact hB,
  simp [sup_of A' B A hA hB, normal_mul],
end

view this post on Zulip Hanting Zhang (Apr 16 2021 at 07:01):

Hold on, I should probably commit my branch to git.

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:02):

BTW you can make the Zassenhaus function a bit less obtuse with an auxiliary definition:

noncomputable def set.snd {A B : set α} : (A * B : set α)  B :=
λ x, _, (x.2).some_spec.some_spec.2.1

noncomputable def Zassenhaus_fun {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] : (A'  A  B) →* (Zassenhaus_quot hA hB) :=
{ to_fun := λ x, quotient.mk' (set.snd _, (mem_mul (Zassenhaus_aux B hA)).mp x.2⟩),
  map_one' := sorry,
  map_mul' := sorry }

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:04):

Looking at that proof, it seems like this is not just any set product, it's one you know is injective, so perhaps you should retain that information somehow

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:04):

The set.snd function is nonsense if it's not

view this post on Zulip Hanting Zhang (Apr 16 2021 at 07:18):

Pushed here: branch#acxxa/composition-series

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:35):

Your "no abel/ring" in normal_sup_normal is simp

view this post on Zulip Hanting Zhang (Apr 16 2021 at 07:44):

One thing I'm wondering is what exactly is the difference between rcases and exists.some/spec? It seems rcases forgets the data, which is forcing me to constantly use some/some_spec in the Zassenhaus_fun proof. It's feels a bit strange that the proofs are so bulky. IRL one would say "let axA(AB)ax \in A' (A \sqcap B)", immediately unwrapping the data while adding the assumptions that aAa \in A' and xABx \in A \sqcap B. But it seems I can't convince lean to do it for me with rcases.

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:47):

You can't use cases/rcases to destruct an existential if you are constructing a function. You need AC for that, which is why classical.some gets involved

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:48):

You can use the choose tactic to construct a function from a forall exists statement, but that's only helpful if you have some limited scope within which you need the construction, i.e. it's not good for constructing defs like Zassenhaus_fun

view this post on Zulip Mario Carneiro (Apr 16 2021 at 07:49):

But when you do use some directly in a definition, you are encouraged to immediately state the corresponding some_spec lemma and henceforth forget about the actual definition

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:00):

I think this is the lemma you are missing:

noncomputable def Zassenhaus_fun_aux {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (x : A'  A  B) : Zassenhaus_quot hA hB :=
quotient.mk' _, ((mem_mul (Zassenhaus_aux B hA)).mp x.2).some_spec.some_spec.2.1

-- "This is well-defined because blah blah..."
theorem Zassenhaus_fun_aux_app {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (a : A') (x : A  B) (h) :
  Zassenhaus_fun_aux hA hB a * x, h = quotient.mk' x :=
sorry

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:00):

Using this function, you can make the proof of Zassenhaus_fun a lot shorter

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:29):

Indeed, this vastly shrinks the size of Zassenhaus_fun

lemma mem_mul' {G : Type u} [group G] {H K : subgroup G} {g : G} (h : (H  K) = (H : set G) * K) :
  g  H  K   (x:H) (y:K), (x * y : G) = g :=
(mem_mul h).trans 
  λ a, b, ha, hb, h⟩, ⟨⟨a, ha⟩, b, hb⟩, h⟩,
  λ ⟨⟨a, ha⟩, b, hb⟩, h⟩, a, b, ha, hb, h⟩⟩

noncomputable def Zassenhaus_fun_aux {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (x : A'  A  B) : Zassenhaus_quot hA hB :=
quotient.mk' _, ((mem_mul (Zassenhaus_aux B hA)).mp x.2).some_spec.some_spec.2.1

theorem Zassenhaus_fun_aux_app {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (a : A') (x : A  B) (h) :
  Zassenhaus_fun_aux hA hB a * x, h = quotient.mk' x :=
begin
  apply quotient.sound',
  have H := (mem_mul (Zassenhaus_aux B hA)).mp h,
  let u := H.some, let v := H.some_spec.some,
  cases a with a ha, cases x with x hx,
  obtain h1 : u  A', h2 : v  A  B, h3 : u * v = a * x := H.some_spec.some_spec,
  refine (mem_of _ _ _).2 (_ : v⁻¹ * x  (A'  B  A  B')  (A  B)),
  rw inf_eq_left.2 (sup_le (inf_le_inf_right _ hA) (inf_le_inf_left _ hB)),
  sorry -- your turn
end

theorem Zassenhaus_fun_aux_app' {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] (a : A') (x : A  B) (b : A'  A  B)
  (e : (a * x : α) = b.1) :
  Zassenhaus_fun_aux hA hB b = quotient.mk' x :=
begin
  have h : (a * x : α)  A'  A  B, {rw e, exact b.2},
  convert  Zassenhaus_fun_aux_app _ _ _ _ h, ext, exact e
end

noncomputable def Zassenhaus_fun {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  (A'  A  B) →* Zassenhaus_quot hA hB :=
{ to_fun := Zassenhaus_fun_aux _ _,
  map_one' := Zassenhaus_fun_aux_app' _ _ 1 _ _ (by simp; refl),
  map_mul' := λ a, ha b, hb⟩,
  begin
    clear_,
    obtain a₁, a₂, rfl := (mem_mul' (Zassenhaus_aux B hA)).1 ha,
    obtain b₁, b₂, rfl := (mem_mul' (Zassenhaus_aux B hA)).1 hb,
    simp only [Zassenhaus_fun_aux_app],
    refine Zassenhaus_fun_aux_app' _ _ a₁ * (a₂ * b₁ * a₂⁻¹), _ _ _ _,
    { sorry },
    simp [mul_assoc],
  end }

The sorry is something about normal subgroups that I'm sure you already have

view this post on Zulip Hanting Zhang (Apr 16 2021 at 19:40):

Thanks, I was able to finish much more of the proof with this!

view this post on Zulip Hanting Zhang (Apr 16 2021 at 19:43):

I've run into another problem though. In the final lemma, it seems like Lean is unable to infer the fact that the quotients have a group structure. I've tried to force it by explicitly writing out the instances with Zassenhaus_normal and finally, but Lean is doesn't know how to use them.

lemma Zassenhaus_fun_ker {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  (Zassenhaus_fun hA hB).ker = (A'  A  B').of (A'  A  B) := sorry

open quotient_group

instance Zassenhaus_normal {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  ((A'  A  B').of (A'  A  B)).normal :=
by { rw  Zassenhaus_fun_ker hA hB, exact monoid_hom.normal_ker _, }

@[instance] lemma finally {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  group $ quotient_group.quotient ((A'  A  B').of (A'  A  B)) :=
begin
  haveI := subgroup.Zassenhaus_normal hA hB,
  apply_instance,
end

lemma Zassenhaus_fun_surjective {A' A B' B : subgroup α} (hA : A'  A) (hB : B'  B)
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  function.surjective (Zassenhaus_fun hA hB) := λ x, x.induction_on' $
begin
  rintro y, (hy : y  (A  B))⟩,
  have hy' := (mem_mul' (Zassenhaus_aux B hA)).mpr 1, y, hy⟩, one_mul _⟩,
  use y, hy'⟩,
  rw subtype.coe_mk at hy',
  rw  one_mul y at hy',
  rw  subtype.coe_mk y hy at hy',
  conv_lhs { find y { rw  one_mul y, rw  subtype.coe_mk y hy, } },
  simp only [Zassenhaus_fun, monoid_hom.coe_mk],
  exact Zassenhaus_fun_aux_app hA hB 1 y, hy hy',
end

lemma butterfly {A' A B' B : subgroup α} {hA : A'  A} {hB : B'  B}
  [hAN : (A'.of A).normal] [hBN : (B'.of B).normal] :
  quotient ((A'  A  B').of (A'  A  B)) ≃* quotient ((B'  B  A').of (B'  B  A)) :=
begin
  sorry
end

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 19:45):

A mul_equiv isn't a lemma, it's a def because you have to supply not just the proof that the multiplication is respected, but also the data of the function that is bijective

view this post on Zulip Hanting Zhang (Apr 16 2021 at 19:49):

Ah, my bad. That's one mistake fixed, but it seems changing to def still doesn't help Lean infer the group instance.

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 19:55):

It can't automatically infer it because it hasn't been supplied the (hA : A' ≤ A) (hB : B' ≤ B)

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 19:56):

It can't find from the instance cache, it's not automatically available to the TC search, if I understand correctly

view this post on Zulip Hanting Zhang (Apr 16 2021 at 19:57):

Hmm, should I be using [hA : A' ≤ A] then? Or maybe [fact (A' ≤ A)]?

view this post on Zulip Hanting Zhang (Apr 16 2021 at 20:00):

Making them implicit arguments isn't working either, which is weird because Lean is able to infer {A' A B' B : subgroup \a} on its own.


Last updated: May 06 2021 at 22:13 UTC