## Stream: new members

### Topic: Difficulty with exists

#### 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 $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 (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  #### 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 #### Mario Carneiro (Apr 16 2021 at 06:50): How is Zassenhaus_aux proven? #### 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  #### Mario Carneiro (Apr 16 2021 at 07:00): And normal_subgroup_mul? #### Mario Carneiro (Apr 16 2021 at 07:00): I'm wondering where the existential came from #### 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  #### Hanting Zhang (Apr 16 2021 at 07:01): Hold on, I should probably commit my branch to git. #### 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 }  #### 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 #### Mario Carneiro (Apr 16 2021 at 07:04): The set.snd function is nonsense if it's not #### Hanting Zhang (Apr 16 2021 at 07:18): Pushed here: branch#acxxa/composition-series #### Mario Carneiro (Apr 16 2021 at 07:35): Your "no abel/ring" in normal_sup_normal is simp #### 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 $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 (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 #### 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 #### 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 #### 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  #### Mario Carneiro (Apr 16 2021 at 08:00): Using this function, you can make the proof of  Zassenhaus_fun a lot shorter #### 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 #### Hanting Zhang (Apr 16 2021 at 19:40): Thanks, I was able to finish much more of the proof with this! #### 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


#### 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

#### 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.

#### 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)

#### 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

#### Hanting Zhang (Apr 16 2021 at 19:57):

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

#### 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