Difficulty with `exists`

Stream: new members

[Hanting Zhang]

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 $A' \trianglelefteq A$ and $B' \trianglelefteq B$ as subgroups of $\alpha$. The first step is to construct a map $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 $ax \in A' (A \sqcap B)$ for $a \in A'$ and $x \in A \sqcap B$. Map $ax$ to $xD$, where $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' (A \sqcap B')$. The inclusion $A' (A \sqcap B') \subseteq \ker f$ is supposed to be obvious: $ax$ is mapped to $xD = D$, since $x$ is annihilated.

Now the problem: To invoke the factorization of $ax$ from a generic term of $A'(A \sqcap B)$, I have to use mem_mul . However, this only gives me $x \in A \sqcap B$ and loses the information that $x \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

[Hanting Zhang]

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

[Mario Carneiro]

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

[Mario Carneiro]

How is Zassenhaus_aux proven?

[Hanting Zhang]

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

[Mario Carneiro]

And normal_subgroup_mul?

[Mario Carneiro]

I'm wondering where the existential came from

[Hanting Zhang]

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

[Hanting Zhang]

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

[Mario Carneiro]

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 }

[Mario Carneiro]

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

[Mario Carneiro]

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

[Hanting Zhang]

Pushed here: branch#acxxa/composition-series

[Mario Carneiro]

Your "no abel/ring" in normal_sup_normal is simp

[Hanting Zhang]

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 $ax \in A' (A \sqcap B)$", immediately unwrapping the data while adding the assumptions that $a \in A'$ and $x \in A \sqcap B$. But it seems I can't convince lean to do it for me with rcases.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Hanting Zhang]

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

[Hanting Zhang]

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

[Yakov Pechersky]

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

[Hanting Zhang]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Hanting Zhang]

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

[Hanting Zhang]

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.