Zulip Chat Archive

Stream: new members

Topic: Frustration with finset


Marc Masdeu (Jul 02 2020 at 14:14):

Hi all,

Noob question: I am trying to prove some elementary results in number theory to get more practice with Lean proof writing. I feel that some generic tactic should kill this MWE, but I can't seem to find it:

import group_theory.subgroup
import tactic

open_locale classical big_operators

lemma blah {G : Type*} [comm_group G] [fintype G]:
( g : G, g) = ( g in {g : G | true}.to_finset, g) :=
begin
  sorry,
end

Thanks in advance for any help...

Mario Carneiro (Jul 02 2020 at 14:26):

congr, ext, simp

Johan Commelin (Jul 02 2020 at 14:27):

@Marc Masdeu Hi, welcome back. (Have you seen https://leanprover-community.github.io/lftcm2020/)
Ooh, Mario is faster with answering the actual question :oops:

Marc Masdeu (Jul 02 2020 at 14:33):

Marc Masdeu Hi, welcome back. (Have you seen https://leanprover-community.github.io/lftcm2020/)

Thanks @Johan Commelin, I've been following everything Lean, just not posting to here... I know about the workshop, but sadly I'll be "away" next week...

Johan Commelin (Jul 02 2020 at 14:34):

Ok, no worries!

Marc Masdeu (Jul 02 2020 at 14:50):

OK, turns out that the MWE I constructed was too M (but thanks @Mario Carneiro ! I did learn about congr!). Here's an updated one, hopefully it is enough now:

def some_subgroup (G : Type*)[comm_group G] : subgroup G := sorry

lemma blah2 {G : Type*} [comm_group G] [fintype G]:
( (x : G) in {x : G | x  some_subgroup G}.to_finset, x) =
     (g : (some_subgroup G)), g :=
begin
    sorry,
end

Johan Commelin (Jul 02 2020 at 14:53):

apply finset.prod_congr --?

Marc Masdeu (Jul 02 2020 at 14:57):

It complains with

invalid apply tactic, failed to unify
   (x : G) in {x : G | x  some_subgroup G}.to_finset, x =  (g : (some_subgroup G)), g
with
  ?m_4.prod ?m_5 = ?m_6.prod ?m_7

Johan Commelin (Jul 02 2020 at 14:57):

Aah, of course

Johan Commelin (Jul 02 2020 at 14:58):

The rhs is over some subgroup.

Johan Commelin (Jul 02 2020 at 14:58):

rw finset.prod_subtype?

Johan Commelin (Jul 02 2020 at 14:58):

If all else fails, there is finset.prod_bij but I would try to avoid that.

Marc Masdeu (Jul 02 2020 at 15:00):

finset.prod_subtype does not seem to exists...

Johan Commelin (Jul 02 2020 at 15:00):

import data.fintype.card? I think

Marc Masdeu (Jul 02 2020 at 15:04):

This has worked:

    rw finset.prod_subtype,
    tauto,
    finish,

Leaving me with no idea of what's going on, of course...

Mario Carneiro (Jul 02 2020 at 15:05):

prod_subtype is missing

Mario Carneiro (Jul 02 2020 at 15:11):

oops, misread Johan's suggestion. This proof might be a little clearer:

lemma blah2 {G : Type*} [comm_group G] [fintype G]:
( (x : G) in {x : G | x  some_subgroup G}.to_finset, x) =
     (g : (some_subgroup G)), g :=
begin
  apply finset.prod_subtype,
  simp, exact λ _, iff.rfl
end

Mario Carneiro (Jul 02 2020 at 15:13):

Unfortunately the unification problem leaves has_coe_t_aux.coe in the term, and simp doesn't know how to simplify it, so we have to finish with iff.rfl instead

Marc Masdeu (Jul 02 2020 at 17:25):

Here is what I have managed to prove: given a finite commutative group G, the product of all its elements equals the product of its elements of order 2. This could be seen as some sort of generalization of Wilson's theorem on the factorial of p-1 modulo p.

Now I know that this is terrible coding style, especially the proof of prod_all_eq_prod_two_torsion. I would appreciate a constructive critique of it. I am not looking for anything mathlib-ready at all, and in fact I'm happy with expensive tactics (to prove mathematically obvious statements) as long as it stays somewhat readable...

Thanks!

import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic

open_locale classical big_operators

lemma prod_finset_distinct_inv {α : Type*} [comm_group α] {s : finset α} :
  ( x  s, x⁻¹  s)  ( x  s, x⁻¹  x)  ( x in s, x) = 1 :=
begin
apply finset.case_strong_induction_on s, by tauto,
intros a s a_notin_s H h1 h2,
specialize H (finset.erase s a⁻¹) (finset.erase_subset (a⁻¹) s),
have r : ( x in (finset.erase s a⁻¹), x) = 1,
{
  apply H,
  {
    intros x h,
    suffices : ¬x = a  x⁻¹  s, by simpa,
    split,
    clarify,
    suffices : x⁻¹  a, by finish,
    have x_not_ainv := finset.ne_of_mem_erase h,
    by_contradiction hh,
    push_neg at hh,
    induction hh,
    finish,
  },
  {
    intros x h,
    apply h2,
    exact finset.mem_insert_of_mem (finset.mem_of_mem_erase h)
  }
},
{
  rw finset.prod_insert a_notin_s,
  suffices hkey : ( x in s, x) = a⁻¹,
  exact mul_eq_one_iff_inv_eq.mpr (eq.symm hkey),
  have ainv_notin_s1 : a⁻¹  finset.erase s a⁻¹ := finset.not_mem_erase a⁻¹ s,
  have ainv_in_s : a⁻¹  s,
  {
    have ainv_in_s1 : a⁻¹  insert a s := h1 a (finset.mem_insert_self a s),
    suffices : a⁻¹  a, by exact finset.mem_of_mem_insert_of_ne ainv_in_s1 this,
    exact h2 a (finset.mem_insert_self a s)
  },
  {
    rw [finset.insert_erase ainv_in_s,finset.prod_insert ainv_notin_s1,r],
    exact mul_one a⁻¹
  },
},
end

def two_torsion_subgroup (G : Type*)[comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
  one_mem' := by simp,
  mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
  begin
    tidy,
    rw [mul_mul_mul_comm a b a b, ha, hb],
    refine mul_one 1,
  end,
  inv_mem' := λ a (ha : a * a = 1), by {tidy, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha}
}

lemma prod_all_eq_prod_two_torsion {G : Type*} [comm_group G] [fintype G]:
( g : G, g) = ( g : two_torsion_subgroup G, g) :=
begin
    have hdisj : disjoint {x : G | x  two_torsion_subgroup G} {x : G | x  x⁻¹ },
    {
        intros x hx,
        cases hx with h1 h2,
        norm_num,
        have hA : x * x = 1, by assumption,
        suffices hB : x * x  1, by exact h2 (false.rec (x = x⁻¹) (hB hA)),
        clear hA h1,
        simp [ mul_eq_one_iff_eq_inv] at h2,
        assumption,
    },
    have h : ( g in {x : G | x  x⁻¹ }.to_finset, g) = 1,
    {
        apply prod_finset_distinct_inv;
        finish,
    },
    have H : ( (g : G), g) = ( x in {x : G | x  two_torsion_subgroup G}.to_finset, x)
            * ( x in {x : G | x  x⁻¹ }.to_finset, x),
    {
        --simp [finset.prod_union],
        simp at *,
        rw  finset.prod_union,
        {
            congr,
            ext1,
            simp [finset.coe_inj],
            safe,
            suffices hh : a  two_torsion_subgroup G, tauto,
            have a2: a * a = 1 := eq_inv_iff_mul_eq_one.mp h_1,
            tauto,
        },
        {
            simp [finset.disjoint_iff_disjoint_coe],
            exact hdisj,
        }
    },
    {
        rw [H, h],
        simp at *,
        apply finset.prod_subtype,
        finish,
    },
end

Alex J. Best (Jul 02 2020 at 20:41):

Its a nice result, I'd say we should have (some version) it in mathlib!
I made some comments inline: it looks pretty good to me, maybe more lemmas and less long proofs would be more manageable though, like for the last statement you could have a lemma that
prod of elements of G is prod of the two torsion times prod of things not their own inverse.
then a lemma that the prod of things that are not their own inverse of any group is one, all as separate lemmas which are combined at the end (basically all of the have's in the last proof could be lemmas)

import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic

open_locale classical big_operators
/- General comments
 1. You can add @[to_additive] to generate additive versions of these lemmas if you like
 2. you use tactics like clarify, finish, safe, a lot, these things can be a little slow, but they
    are convenient, so might be best to separate out some of the times they are used as separate lemmas
    whose proof is just by finish or whatever, so that they don't get re-run all the time -/

set_option profiler true -- you can use this too see time spent on proofs

lemma prod_finset_distinct_inv {α : Type*} [comm_group α] {s : finset α} :
  ( x  s, x⁻¹  s)  ( x  s, x⁻¹  x)  ( x in s, x) = 1 :=
begin
apply finset.case_strong_induction_on s,  by tauto,
intros a s a_notin_s H h1 h2,
specialize H (finset.erase s a⁻¹) (finset.erase_subset (a⁻¹) s),
have r : ( x in (finset.erase s a⁻¹), x) = 1,
{
  apply H,
  {
    intros x h,
    suffices : ¬x = a  x⁻¹  s, by simpa,
    split,
    begin finish, end, -- this takes ages
    suffices : x⁻¹  a, from finset.mem_of_mem_insert_of_ne (h1 x (finset.mem_insert_of_mem (finset.mem_of_mem_erase h))) this,
    -- replaced finish with an explicit proof,
    by_contradiction hh,
    push_neg at hh,
    induction hh,
    simpa using finset.ne_of_mem_erase h,
    -- replaced finish with an explicit proof and don't name a short term that is only used once now
  },
  {
    intros x h,
    apply h2,
    exact finset.mem_insert_of_mem (finset.mem_of_mem_erase h)
  }
},
{
  rw finset.prod_insert a_notin_s,
  suffices hkey : ( x in s, x) = a⁻¹,
  exact mul_eq_one_iff_inv_eq.mpr (eq.symm hkey),
  have ainv_notin_s1 : a⁻¹  finset.erase s a⁻¹ := finset.not_mem_erase a⁻¹ s,
  have ainv_in_s : a⁻¹  s,
  {
    have ainv_in_s1 : a⁻¹  insert a s := h1 a (finset.mem_insert_self a s),
    suffices : a⁻¹  a, from finset.mem_of_mem_insert_of_ne ainv_in_s1 this, -- by exact can almost always be removed!
    -- as it is just openening tactic mode then returning to term mode
    exact h2 a (finset.mem_insert_self a s)
  },
  {
    rw [finset.insert_erase ainv_in_s,finset.prod_insert ainv_notin_s1,r],
    exact mul_one a⁻¹
  },
},
end

def two_torsion_subgroup (G : Type*) [comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
  one_mem' := by simp,
  mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
  begin
    dsimp, -- use tidy? and tidy will tell you what it did in this case it only did dsimp at *, and we can just change it to dsimp
    rw [mul_mul_mul_comm a b a b, ha, hb],
    exact mul_one 1, -- exact instead of refine
  end,
  inv_mem' := λ a (ha : a * a = 1), by {dsimp, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha} --same with tidy
}

lemma prod_all_eq_prod_two_torsion {G : Type*} [comm_group G] [fintype G]:
 g : G, g =  g : two_torsion_subgroup G, g := -- don't need brackets
begin
    have hdisj : disjoint {x : G | x  two_torsion_subgroup G} {x : G | x  x⁻¹ },
    {
        intros x hx,
        cases hx with h1 h2,
        norm_num,
        have hA : x * x = 1, by assumption,
        suffices hB : x * x  1, by exact h2 (false.rec (x = x⁻¹) (hB hA)),
        clear hA h1,
        simpa [ mul_eq_one_iff_eq_inv] using h2, -- simpa .. using instead of simp .. at .., assumption
    },
    have h : ( g in {x : G | x  x⁻¹ }.to_finset, g) = 1,
    {
        apply prod_finset_distinct_inv;
        finish,
    },
    have H : ( (g : G), g) = ( x in {x : G | x  two_torsion_subgroup G}.to_finset, x)
            * ( x in {x : G | x  x⁻¹ }.to_finset, x),
    {
        --simp [finset.prod_union],
        -- using squeeze_simp we see that simp only used one lemma here, which was ne.def
        -- didn't seem like this was really changing anything so remove it!
        rw  finset.prod_union,
        {
            congr,
            ext1,
            simp only [true_iff, finset.mem_univ, set.mem_to_finset, ne.def, finset.mem_union, set.mem_set_of_eq],
            rw [two_torsion_subgroup, eq_inv_iff_mul_eq_one], --neater proof
            exact classical.em _,
        },
        {
            simpa only [finset.disjoint_iff_disjoint_coe, set.coe_to_finset],
            -- simp then exact (hypothesis) can be written as simpa
        }
    },
    {
        rw [H, h],
        simp, -- once again simp wasnt doing much to most goals
        apply finset.prod_subtype,
        finish,
    },
end

Johan Commelin (Jul 02 2020 at 20:45):

Probably relevant: prod_involution

Marc Masdeu (Jul 03 2020 at 10:35):

Thanks @Alex J. Best for the review! I have incorporated your suggestions, although I see no way of coming up with this

suffices : x⁻¹  a, from finset.mem_of_mem_insert_of_ne (h1 x (finset.mem_insert_of_mem (finset.mem_of_mem_erase h))) this,

on my own without spending half an hour trying different things. Would be nice if the finish tactic gave something back as a hint!

@Johan Commelin : I was aware of prod_involution (this is the one that wilson's theorem uses, right?), but wanted to prove the version that I needed using tactics.

Next step (we have a "summer project" with @Xavier Xarles) will be to prove that the product of all the elements of a finite elementary abelian 2-group of order > 2 is 1...

Jalex Stark (Jul 03 2020 at 13:54):

To expand on Johan's point, applying prod_involution reduces the problem to four much easier sorries.

import data.fintype.card
import data.set.finite
import tactic

open_locale classical big_operators
open finset

lemma prod_finset_distinct_inv
{α : Type*} [comm_group α] {s : finset α}
(hs1 :  x  s, x⁻¹  s)
(hs2 :  x  s, x⁻¹  x)
:  x in s, x = 1 :=
begin
  apply @prod_involution _ _ _ _ _ (λ a ha, a⁻¹),
  { intros, rw mul_inv_self },
  { intros, apply hs2, assumption },
  { intros, simp, },
  { intros, apply hs1, assumption, },
end

Alex J. Best (Jul 07 2020 at 06:23):

Marc Masdeu said:

Would be nice if the finish tactic gave something back as a hint!

I asked about this once and was told more or less that the output would be unreadable and no quicker than just running finish again unfortunately: https://github.com/leanprover-community/mathlib/issues/1451#issuecomment-533151071

Marc Masdeu (Jul 10 2020 at 09:10):

Jalex Stark said:

To expand on Johan's point, applying prod_involution reduces the problem to four much easier sorries.

Thanks @Jalex Stark , we knew about this but it seemed like killing flies with cannons, so we set to prove directly what we exactly wanted. But in the long run, I agree your approach is the right one.

Marc Masdeu (Jul 10 2020 at 09:13):

And now I can't even start the next lemma:

variables {G : Type*} [comm_group G] [fintype G]

-- given G two torsion and 1 ≠ g ∈ G, there is H < G of index 2 with g ∉ H
lemma element_avoidance {g : G} (h₁ : g  1) (h₂ : g * g = 1):
  (H : subgroup G) , (g  H  ( x : H, x * x = 1)  {x : G | x * x = 1} = H  (left_coset g H)):=
begin
    apply nat.case_strong_induction_on (fintype.card G),
end

I want to do a proof by induction on the size of G, but it complains at the first step. I can't quite make sense of the error. In trying to debug what was going on, I went for a much stupider lemma, which I can't do either!

lemma stupid {g : G} (h₁ : g  1) (h₂ : g * g = 1):
  (H : subgroup G) ,  H = H :=
begin
    use G, -- Complains!
end

Alex J. Best (Jul 10 2020 at 09:45):

One way to get G as a subgroup of itself is to think of the ordering on subgroups by inclusion, G is then tthe maximal, or top element, so lean understands the symbol \top for G as a sub of itself.

lemma stupid {g : G} (h₁ : g  1) (h₂ : g * g = 1):
  (H : subgroup G) ,  H = H :=
begin
    use ,
end

Alex J. Best (Jul 10 2020 at 09:49):

Also, be cautious using the arrow directly, if you want to coerce something try (thing : Type) to tell lean which type to coerce it to, lean will print the up arrow but it can be underdetermined what you want the arrow to mean so just putting the type you want can save headaches.

Marc Masdeu (Jul 10 2020 at 09:50):

Yes but isn't this like cheating? I would expect that there would be some kind of coertion mechanism that would work in this case. In particular, use (G : subgroup G) is more like what I'd like to work, and it doesn't. Recall that I want to really do the non-stupid lemma by induction...

Alex J. Best (Jul 10 2020 at 09:54):

As for your first question lean gets a bit confused because it doesn't see the cardinality of G, or even G really in your goal, maybe its possible to make it work, but it seems less hassle to set this up more explicitly as a statement parameterised by the caridinality of the group

lemma element_avoidance_aux {n : } : (fintype.card G = n)   {g : G} (h₁ : g  1) (h₂ : g * g = 1),
  (H : subgroup G) , (g  H  ( x : H, x * x = 1)  {x : G | x * x = 1} = H  (left_coset g H)):=
begin
  apply nat.case_strong_induction_on n,
end

your original statement is then obtained as element_avoidance_aux (rfl _) or something like that.

Alex J. Best (Jul 10 2020 at 09:59):

Marc Masdeu said:

Yes but isn't this like cheating? I would expect that there would be some kind of coertion mechanism that would work in this case. In particular, use (G : subgroup G) is more like what I'd like to work, and it doesn't. Recall that I want to really do the non-stupid lemma by induction...

I agree some automatic coercion would be nice, I'm just not sure how the setup would go. It doesn't seem to me to fit the coercion model: G is a type and you can't make a coercion from any random type to subgroup G, only from G itself.

Top is a bit weird to look at at first, but its short to type, and you get all the lemmas about order (every subgroup is contained in top, nothing contains top, etc for free.

Alex J. Best (Jul 10 2020 at 10:26):

I was confused but: Ohhh I get it HH is index 2 only in the 2-torsion.

Kevin Buzzard (Jul 10 2020 at 14:01):

Coercing G into subgroup G is a dependent coercion which I don't think is possible

Marc Masdeu (Jul 27 2020 at 08:35):

OK so I'm Leaning again, and managed to prove the element_avoidance lemma, modulo proving the "obvious" fact that a finite subgroup has finitely many subgroups:

import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic
import basic

open_locale classical big_operators

variables {G : Type*} [comm_group G] [fintype G]

lemma finite_subgroups_of_finite_group : {X : subgroup G | true}.finite :=
begin
    sorry
end

Is this something easy to do?

Kenny Lau (Jul 27 2020 at 08:36):

it injects to set G

Kenny Lau (Jul 27 2020 at 08:36):

also instead of that you want to say fintype (subgroup G)?

Marc Masdeu (Jul 27 2020 at 08:37):

The exact statement that I need in my proof is this one, but maybe what you suggest is also OK?

Kenny Lau (Jul 27 2020 at 08:38):

import group_theory.subgroup
import data.fintype.card
import data.set.finite
import tactic

noncomputable theory
open_locale classical big_operators

variables {G : Type*} [comm_group G] [fintype G]

instance : fintype (subgroup G) :=
fintype.of_injective (coe : subgroup G  set G) $ λ _ _, subgroup.ext'

lemma finite_subgroups_of_finite_group : {X : subgroup G | true}.finite :=
set.finite.of_fintype _

Kenny Lau (Jul 27 2020 at 08:39):

(edited)

Marc Masdeu (Jul 27 2020 at 08:44):

Wow!! I am trying to make sense of what just happened there... I have trouble understanding finset, fintype,... And also the instance thingy. But thanks so much @Kenny Lau !

Marc Masdeu (Jul 27 2020 at 09:36):

After minimal cleaning, this is what I got:

instance : fintype (subgroup G) := fintype.of_injective (coe : subgroup G  set G) $ λ _ _, subgroup.ext'

-- given a finite group G  and g ∈ G of order 2, there is H < G  with g ∉ H and such that G[2] = H \cup g H.
lemma element_avoidance {g : G}  (h₁ : g  1) (h₂ : g * g = 1):
  (H : subgroup G) ,
  (g  H 
  ( (x : G), x  H  x * x = 1) 
  {x : G | x * x = 1} = H  (left_coset g H))
  :=
begin
    let s := {X : subgroup G | g  X  ( x : G, x  X  x*x = 1)},
    have sfin : s.finite := set.finite.of_fintype _,
    have snonempty : set.nonempty s,
    {
        use ,
        split,
        exact h₁,
        intros x hx,
        rw subgroup.mem_bot at hx,
        rw hx,
        exact mul_one 1,
    },
    let existsH := set.finite.exists_maximal_wrt id s sfin snonempty,
    simp only [and_imp, exists_prop, id.def, set.mem_set_of_eq] at existsH,
    cases existsH with a ha,
    use a,
    split,
    exact ha.1.1,
    split,
    exact ha.1.2,
    -- We have defined a as the maximal subgroup of G satisfying
    -- 1) g ∉ a
    -- 2) ∀ x ∈ a, x*x = 1
    -- Now we must show that a ∪ ga = twotorsion(G)
    apply set.subset.antisymm,
    {
        -- Prove that twotorsion(G) ⊆ a u ga
        intros x hx,
        dsimp at hx,
        rcases ha with   ha1, hmax  ,
        cases ha1 with hga hatwotors,

        by_contradiction h,
        have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
        let xua : subgroup G :=
        {
            carrier := a  left_coset x a,
            one_mem' := or.inl (subgroup.one_mem a),
            mul_mem' :=
            begin
            intros u v hu hv,
            cases hv with hv1 hv2,
            {
                cases hu with hu1 hu2,
                {
                    exact or.inl (subgroup.mul_mem a hu1 hv1),
                },
                {
                    right,
                    rw [mem_left_coset_iff, mul_assoc],
                    rw mem_left_coset_iff at hu2,
                    exact is_submonoid.mul_mem hu2 hv1,
                }
            },
            {
                cases hu with hu1 hu2,
                {
                    right,
                    rw [mul_comm, mem_left_coset_iff, mul_assoc],
                    rw mem_left_coset_iff at hv2,
                    exact is_submonoid.mul_mem hv2 hu1,
                },
                {
                    left,
                    rw mem_left_coset_iff at hu2 hv2,
                    have H : x⁻¹ * x⁻¹ * u * v  a,
                    {
                        norm_cast at hu2 hv2 ,
                        rw [mul_comm, mul_assoc, mul_assoc v _, mul_comm v _],
                        exact subgroup.mul_mem a hv2 hu2,
                    },
                    rw [x_eq_xinv, hx, one_mul] at H,
                    exact H,
                },
            },
            end,
            inv_mem' :=
            begin
                intros u hu,
                cases hu with hu1 hu2,
                {
                    exact or.inl (is_subgroup.inv_mem hu1),
                },
                {
                    right,
                    rw mem_left_coset_iff at hu2 ,
                    norm_cast at hu2 ,
                    rw [subgroup.inv_mem_iff, mul_inv, inv_inv, inv_inv],
                    rw x_eq_xinv at hu2,
                    exact hu2,
                }
            end
        },
        have hxinxua :  y : G, y  xua  (y  a  y  left_coset x a), by apply subgroup.mem_coe,
        specialize hmax xua,
        have g_notin_xua : g  xua,
        {
            clear hmax,
            by_contradiction cont,
            cases cont with c1 c2,
            {
                solve_by_elim,
            },
            {
                rw mem_left_coset_iff at c2,
                have h2: x  left_coset g a,
                {
                    rw set.mem_union_eq at h,
                    push_neg at h,
                    exact h.right,
                },
                rw mem_left_coset_iff at h2,
                suffices h3: g⁻¹ * x  a, by solve_by_elim,
                norm_cast at *,
                rw [subgroup.inv_mem_iff, mul_inv, mul_comm, inv_inv],
                exact c2,
            }
        },
        specialize hmax g_notin_xua,
        have h_twotors : ( (y : G), y  xua  y * y = 1),
        {
            intros y hy,
            rw hxinxua at hy,
            cases hy,
            {
                apply hatwotors,
                exact subgroup.mem_coe.mp hy,
            },
            {
                rw mem_left_coset_iff at hy,
                have HH :  w  a, x⁻¹ * y = w, by tauto,
                cases HH with w hw,
                cases hw with hw1 hw2,
                have hhy : y = x * w := eq_mul_of_inv_mul_eq hw2,
                calc
                y * y = (x * w) * (x * w): congr (congr_arg has_mul.mul hhy) hhy
                ...   = (x * x) * (w * w): mul_mul_mul_comm x w x w
                ...   = w * w : mul_left_eq_self.mpr hx
                ...   = 1      : hatwotors w hw1,
            }
        },
        specialize hmax h_twotors,
        have htriv : a  xua,
        {
            rw subgroup.le_def,
            intros y hy,
            rw hxinxua,
            left,
            exact hy,
        },
        specialize hmax htriv,
        have hc : x  a,
        {
            norm_cast at *,
            rw hmax,
            clear sfin snonempty s hga hatwotors h g_notin_xua htriv h_twotors h₁ h₂ hmax,
            dsimp at *,
            rw hxinxua,
            right,
            rw mem_left_coset_iff,
            exact quotient_group.eq.mp rfl,
        },
        have hl : x  a,
        {
            rw set.mem_union at h,
            push_neg at h,
            exact h.left
        },
        solve_by_elim,
    },
    {
        -- prove that twotorsion(G) ⊇ a u ga
        intros x hx,
        by_cases (x  a),
        tauto,
        {
            have H : (x  left_coset g a),
            {
                rw set.mem_union at hx,
                tauto,
            },
            suffices x_is_twotors : x * x = 1, by tauto,
            clear hx h,
            have H2 :  (x : G), x  a  x * x = 1, by tauto,
            rw mem_left_coset_iff at H,
            specialize H2  (g⁻¹ * x) H,
            have H3 : g = g⁻¹ := eq_inv_of_mul_eq_one h₂,
            by calc
            x * x = g * g * x * x : by simp only [h₂, one_mul]
            ...   = g⁻¹ * g⁻¹ * x * x : by rw  H3
            ...   = g⁻¹ * x * g⁻¹ * x : by rw mul_right_comm g⁻¹ g⁻¹ x
            ...   = g⁻¹ * x * (g⁻¹ * x) : by exact mul_assoc (g⁻¹ * x) g⁻¹ x
            ...   = 1 : by exact H2,
        }
    },
end

Scott Morrison (Jul 27 2020 at 09:52):

Please please turn that into 10 separate lemmas. :-)

Marc Masdeu (Jul 27 2020 at 14:08):

Scott Morrison said:

Please please turn that into 10 separate lemmas. :-)

Have 6 so far...and done for the day :-).

variables {G : Type*} [comm_group G] [fintype G]

instance : fintype (subgroup G) := fintype.of_injective (coe : subgroup G  set G) $ λ _ _, subgroup.ext'

/-
If a is a subgroup of G[2] and x ∈ G[2], then a ∪ x *l a is a subgroup.
-/
def insert_twotors_to_twotors {x : G} {a : subgroup G}
  (hx : x * x = 1) (ha :  g : G, g  a  g * g = 1) : subgroup G :=
{
  carrier := a  left_coset x a,
  one_mem' := or.inl (subgroup.one_mem a),
  mul_mem' :=
  begin
    intros u v hu hv,
    --rcases? hu hv,-- with ⟨ hu1, hu2⟩ | ⟨  hv1, hv2⟩ ,
    cases hv with hv1 hv2,
    repeat {cases hu with hu1 hu2},
    {
      exact or.inl (subgroup.mul_mem a hu1 hv1),
    },
    {
      right,
      rw [mem_left_coset_iff, mul_assoc],
      rw mem_left_coset_iff at hu2,
      exact is_submonoid.mul_mem hu2 hv1,
    },
    {
      right,
      rw [mul_comm, mem_left_coset_iff, mul_assoc],
      rw mem_left_coset_iff at hv2,
      exact is_submonoid.mul_mem hv2 hu1,
    },
    {
      left,
      rw mem_left_coset_iff at hu2 hv2,
      have H : x⁻¹ * x⁻¹ * u * v  a,
      {
          norm_cast at hu2 hv2 ,
          rw [mul_comm, mul_assoc, mul_assoc v _, mul_comm v _],
          exact subgroup.mul_mem a hv2 hu2,
      },
      have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
      rw [x_eq_xinv, hx, one_mul] at H,
      exact H,
    }
  end,
  inv_mem' :=
  begin
      intros u hu,
      cases hu with hu1 hu2, by exact or.inl (is_subgroup.inv_mem hu1),
      {
          right,
          rw mem_left_coset_iff at hu2 ,
          norm_cast at hu2 ,
          rw [subgroup.inv_mem_iff, mul_inv, inv_inv, inv_inv],
          have x_eq_xinv : x = x⁻¹ := eq_inv_of_mul_eq_one hx,
          rw x_eq_xinv at hu2,
          exact hu2,
      }
  end
}
/--
If g ∈ G[2] and a ≤ G[2], then a ∪ g l* a ⊆ G[2].
--/
lemma twotorsion_contains_a_and_ga {g : G} {a : subgroup G}
  (h₁ : g * g = 1) (h₂ :  (x : G), x  a  x * x = 1) :
    a  left_coset g a  {x : G | x * x = 1} :=
begin
  -- prove that twotorsion(G) ⊇ a u ga
  intros x hx,
  by_cases (x  a), tauto,
  have H : (x  left_coset g a),
  {
      rw set.mem_union at hx,
      norm_cast at hx,
      tauto,
  },
  suffices x_is_twotors : x * x = 1, by tauto,
  clear hx h,
  have H2 :  (x : G), x  a  x * x = 1, by tauto,
  rw mem_left_coset_iff at H,
  specialize H2  (g⁻¹ * x) H,
  have H3 : g = g⁻¹ := eq_inv_of_mul_eq_one h₁,
  by calc
  x * x = g * g * x * x : by simp only [h₁, one_mul]
  ...   = g⁻¹ * g⁻¹ * x * x : by rw  H3
  ...   = g⁻¹ * x * g⁻¹ * x : by rw mul_right_comm g⁻¹ g⁻¹ x
  ...   = g⁻¹ * x * (g⁻¹ * x) : by exact mul_assoc (g⁻¹ * x) g⁻¹ x
  ...   = 1 : by exact H2,
end

/--
Suppose a ≤ G[2], and g ∉ a.
Then if x ∈ G[2] and x ∉ g l* a,
then g ∉ ⟨ x, a ⟩.
--/
lemma g_notin_xua {x g: G} {a : subgroup G}
  (hg : g  a)
  (hx : x * x = 1)
  (ha :  y : G, y  a  y * y = 1)
  (hgx : x  left_coset g a) :
    (g  insert_twotors_to_twotors hx ha) :=
begin
  by_contradiction cont,
  cases cont,
  by contradiction,
  {
      rw mem_left_coset_iff at *,
      suffices : g⁻¹ * x  a, by solve_by_elim,
      norm_cast at *,
      rw [subgroup.inv_mem_iff, mul_inv, mul_comm, inv_inv],
      exact cont,
  }
end

/--
If x ∈ G[2] and a ≤ G[2], then ⟨ x, a ⟩ ≤ G[2].
--/
lemma xua_twotors {x : G} {a : subgroup G}
  (hx : x * x = 1)
  (ha :  y : G, y  a  y * y = 1) :
    ( (y : G), y  (insert_twotors_to_twotors hx ha)  y * y = 1) :=
begin
  intros y hy,
  let xua := insert_twotors_to_twotors hx ha,
  have hxinxua :  y : G, y  xua  (y  a  y  left_coset x a), by apply subgroup.mem_coe,
  rw hxinxua at hy,
  cases hy, by exact ha y (subgroup.mem_coe.mp hy),
  {
    rw mem_left_coset_iff at hy,
    have HH :  w  a, x⁻¹ * y = w, by tauto,
    rcases HH with  w , hw1, hw2⟩⟩,
    have hhy : y = x * w := eq_mul_of_inv_mul_eq hw2,
    calc
    y * y = (x * w) * (x * w): congr (congr_arg has_mul.mul hhy) hhy
    ...   = (x * x) * (w * w): mul_mul_mul_comm x w x w
    ...   = w * w : mul_left_eq_self.mpr hx
    ...   = 1      : ha w hw1,
  }
end

/--
G[2] ≤ ⟨g, a⟩
--/
lemma twotorsion_containedin_a_union_ga {g : G} {a : subgroup G}
      (h₁ : g * g = 1) (h₂ :  (x : G), x  a  x * x = 1)
      (hga : g  a)
      (hmax :  (a' : subgroup G), g  a'  ( (x : G), x  a'  x * x = 1)  a  a'  a = a') :
      {x : G | x * x = 1}  a  left_coset g a :=
begin
  -- Prove that twotorsion(G) ⊆ a u ga
  intros x hx,
  dsimp at hx,
  by_contradiction h,
  rw set.mem_union at h,
  push_neg at h,
  let xua := insert_twotors_to_twotors hx h₂,
  have hxinxua :  y : G, y  xua  (y  a  y  left_coset x a), by apply subgroup.mem_coe,
  have g_notin_xua : g  xua, by exact g_notin_xua hga hx h₂ h.right,
  have h_twotors : ( (y : G), y  xua  y * y = 1), by exact xua_twotors hx h₂,
  have a_eq_xua : a = xua := hmax xua g_notin_xua h_twotors (λ y hy, or.inl hy),
  have x_in_a : x  a,
  {
      norm_cast at *,
      rw [a_eq_xua, hxinxua, mem_left_coset_iff],
      right,
      simp only [subgroup.mem_coe, mul_left_inv],
      exact subgroup.one_mem a
  },
  norm_cast at h,
  have hl := h.left,
  trivial,
end

-- given G two torsion and 1 ≠ g ∈ G, there is H < G of index 2 with g ∉ H
lemma element_avoidance {g : G}  (h₁ : g  1) (h₂ : g * g = 1):
  (H : subgroup G) ,
  (g  H 
  ( (x : G), x  H  x * x = 1) 
  {x : G | x * x = 1} = H  (left_coset g H))
  :=
begin
    let s := {X : subgroup G | g  X  ( x : G, x  X  x*x = 1)},
    have sfin : s.finite := set.finite.of_fintype _,
    have snonempty : set.nonempty s,
    {
        use ,
        split,
        exact h₁,
        intros x hx,
        rw subgroup.mem_bot at hx,
        rw hx,
        exact mul_one 1,
    },
    let existsH := set.finite.exists_maximal_wrt id s sfin snonempty,
    simp only [and_imp, exists_prop, id.def, set.mem_set_of_eq] at existsH,
    cases existsH with a ha,
    use a,
    repeat {split},
    exact ha.1.1,
    exact ha.1.2,
    -- We have defined a as the maximal subgroup of G satisfying
    -- 1) g ∉ a
    -- 2) ∀ x ∈ a, x*x = 1
    -- Now we must show that a ∪ ga = twotorsion(G)
    apply set.subset.antisymm,
    apply twotorsion_containedin_a_union_ga h₂ ha.1.2 ha.1.1 ha.2,
    exact twotorsion_contains_a_and_ga h₂ ha.1.2,
end

Marc Masdeu (Jul 29 2020 at 16:13):

And I still don't see the need to change the topic title... Here's another place that I've got stuck:

def two_torsion_subgroup (G : Type*)[comm_group G] : subgroup G :=
{ carrier := {z : G | z * z = 1},
  one_mem' := by simp,
  mul_mem' := λ a b (ha : a * a = 1) (hb : b * b = 1),
  begin
    tidy,
    rw [mul_mul_mul_comm a b a b, ha, hb],
    refine mul_one 1,
  end,
  inv_mem' := λ a (ha : a * a = 1), by {tidy, rw mul_inv_eq_one, refine inv_eq_of_mul_eq_one ha}
}

lemma two_prods_are_equal {G : Type*} [comm_group G] [fintype G]:
(( (g : (two_torsion_subgroup G)), g) : G) = ( (g : G) in (two_torsion_subgroup G).carrier.to_finset, g ):=
begin
  sorry
end

I don't manage to prove the lemma, which to me is just two different ways of writing in Lean the same exact product. I also don't see why I can't apply finset.prod_congr...

Thanks Lean community!

Kevin Buzzard (Jul 29 2020 at 16:30):

This is exactly the sort of thing which makes lean hard for mathematicians to use

Kevin Buzzard (Jul 29 2020 at 16:32):

The official answer is probably that this is #xy and you should decide once and for all how you want to talk about this subset instead of switching between different ways of talking about it

Kevin Buzzard (Jul 29 2020 at 16:34):

It wouldn't surprise me if you ended up with two different witnesses to finiteness of the set you're taking a product over and then nothing will work anyway and you'll have to get the forensic experts in

Kevin Buzzard (Jul 29 2020 at 16:35):

Did you try library_search?

Johan Commelin (Jul 29 2020 at 16:36):

@Marc Masdeu Sorry for the pain...

Johan Commelin (Jul 29 2020 at 16:36):

The reason that finset.prod_congr doesn't work is because it assumes you are taking products indexed by the same type. But in your case the LHS is a subtype of the type on the right.

Johan Commelin (Jul 29 2020 at 16:37):

So you probably need to rw the LHS using something like finset.prod_subtype.

Kevin Buzzard (Jul 29 2020 at 16:37):

PS unrelated -- tidy is only supposed to be used at the end of a proof. You might want to replace it with tidy? and then with the output of what it says it's doing. It might not be doing much at all.

Johan Commelin (Jul 29 2020 at 16:37):

I agree that we shouldn't need to experience this pain. But I don't know how to solve it.

Johan Commelin (Jul 29 2020 at 16:38):

Maybe better simp-lemmas?

Kevin Buzzard (Jul 29 2020 at 16:50):

Delete fintype ;-)

Kevin Buzzard (Jul 29 2020 at 16:50):

Or at least don't tell mathematicians about it

Kevin Buzzard (Jul 29 2020 at 16:52):

I don't know how to solve this. We offer several ways of doing a product over a finite set and this is problematic

Kevin Buzzard (Jul 29 2020 at 16:53):

The problem is even more basic than this, we offer three ways to take the intersection of a bunch of sets

Marc Masdeu (Jul 29 2020 at 16:54):

Oh well. I understand that if I choose different ways of writing the same, then I'll have to deal with coercions and the like. I'm very surprised though that this is so hard!

I got into this because I am trying to prove some lemmas about products of elements of a finite abelian multiplicative group G. Which way should I be using? I'm happy to redo parts of what I already have.

Mario Carneiro (Jul 29 2020 at 16:57):

This should be generalized to a lemma about prod

Kevin Buzzard (Jul 29 2020 at 16:58):

The issue of course Marc is that if you only prove the result about one of them, then sooner or later someone will need it for the other variant :-)

Mario Carneiro (Jul 29 2020 at 16:58):

I think something like prod (g : S), f g = prod g in T, f g if S = T

Mario Carneiro (Jul 29 2020 at 16:59):

where S = T needs some coe or to_finset or something

Marc Masdeu (Jul 29 2020 at 17:00):

Here's my real problem (to avoid xy): I have proven this lemma

(∏ g : G, g) = (∏ g : two_torsion_subgroup G, g)

and this one:

 ∃ (H : subgroup G) ,
  (g ∉ H ∧
  (∀ (x : G), x ∈ H → x * x = 1) ∧
  {x : G | x * x = 1} = H ∪ (left_coset g H))

The one that I'd like to prove next is:

lemma prod_identity {g : G} (h₁ :  x : G, x * x = 1) (h₂ : g  1):
 ( x : G, x) = g^((fintype.card G / 2) : )

and along the way I thought that I would easily be able to prove

(( x : two_torsion_subgroup G, x) : G) = (( x : H, x) : G) * ( x : left_coset g H, x )

for the subgroup H given by the previous lemma. I have already proven that the two sets (H and g *l H) are disjoint, so it seemed easy...

Marc Masdeu (Jul 29 2020 at 17:01):

Mario Carneiro said:

I think something like prod (g : S), f g = prod g in T, f g if S = T

I'll try to see if I can write a proof for this...

Kevin Buzzard (Jul 29 2020 at 17:04):

That looks messy and unmathematical (but important)

Kevin Buzzard (Jul 29 2020 at 17:06):

You look like you're on the right track but now things are going to get a bit nasty.

Kevin Buzzard (Jul 29 2020 at 17:08):

I've never used these finite products before but it looks to me like you're taking a product over a finite type and I think you'd be much better off taking a product over a finite subset of a type

Kevin Buzzard (Jul 29 2020 at 17:09):

Because then the proof that a product over H union gH equals the product over H times the product over gH will be much easier

Marc Masdeu (Jul 29 2020 at 17:10):

Well for me the most confusing thing is that I deal at the same time with a group and a subgroup of it, and then the product may run over subsets of either. I don't know whether I should first coerce everything as elements of the big group, and then take the corresponding set (finset?) or take the set corresponding to the element of the subgroup.

Johan Commelin (Jul 29 2020 at 17:14):

Kevin Buzzard said:

I've never used these finite products before but it looks to me like you're taking a product over a finite type and I think you'd be much better off taking a product over a finite subset of a type

Yup, I suggest trying to avoid the subtype

Kevin Buzzard (Jul 29 2020 at 17:14):

My gut feeling is that you'd be better off always working with subsets of the big group

Johan Commelin (Jul 29 2020 at 17:14):

(Sometimes they are useful... but most of the time I would avoid them.)

Marc Masdeu (Jul 29 2020 at 17:25):

I'm affraid this is not what @Mario Carneiro was asking for, right?

lemma two_products {α β: Type*} {s : finset α} [comm_monoid β] {t : set α} [fintype t] {f : α  β}
(h: s = t.to_finset) :
( g in s, f g) = ( g in t.to_finset, f g) := congr_fun (congr_arg finset.prod h) (λ (g : α), f g)

Mario Carneiro (Jul 29 2020 at 17:26):

You want t to be a finset

Mario Carneiro (Jul 29 2020 at 17:26):

and h could be for example \forall x, x \in s <-> x \in t

Mario Carneiro (Jul 29 2020 at 17:27):

and s should be a set, with g : s on the left

Johan Commelin (Jul 29 2020 at 17:27):

That's just prod_congr, right?

Mario Carneiro (Jul 29 2020 at 17:27):

if you have prod g in s on both sides it's just congr

Johan Commelin (Jul 29 2020 at 17:27):

Sure, but there is a lemma prod_congr

Mario Carneiro (Jul 29 2020 at 17:27):

the point here is that it's two different kinds of summations on each side

Mario Carneiro (Jul 29 2020 at 17:28):

g : s on the left and g in t on the right

Marc Masdeu (Jul 29 2020 at 17:28):

Oh I see. Yes, it's also confusing because the symbol is the same...If s is a finset then one can abbreviate g in s with g : s, according to what's written in big_operators.lean

Mario Carneiro (Jul 29 2020 at 17:28):

prod g : s is really prod (g:s) in univ

Mario Carneiro (Jul 29 2020 at 17:29):

prod g in s is therefore not the same (syntactically) as prod g : s even if s is a finset (the latter being prod g in (univ : finset s))

Mario Carneiro (Jul 29 2020 at 17:30):

but there should be a theorem proving they are equal

Marc Masdeu (Jul 29 2020 at 17:30):

OK now trying to prove this:

lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : set α} [fintype t] {f : α  β}
 (h:  x, x  s  x  t) : ( g : s, f g) = ( g in t.to_finset, f g)

Mario Carneiro (Jul 29 2020 at 17:30):

still drop the to_finset

Mario Carneiro (Jul 29 2020 at 17:31):

t : finset A

Mario Carneiro (Jul 29 2020 at 17:31):

and no fintype t assumption

Johan Commelin (Jul 29 2020 at 17:32):

rw ← finset.prod_subtype, apply finset.prod_congr should get you moving again

Marc Masdeu (Jul 29 2020 at 17:35):

Not for me, @Johan Commelin ... I am trying this, as Mario suggested:

lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : finset α} {f : α  β}
 (h:  x, x  s  x  t) : ( g : s, f g) = ( g in t, f g) :=

and the first rw gives me 4 goals...

Mario Carneiro (Jul 29 2020 at 17:37):

So now we have to start hunting through the finset and big_operator API to prove this

Mario Carneiro (Jul 29 2020 at 17:38):

It helps to understand what the theorem actually says, without all the nice notations. The left product is
(finset.univ {x // x \in s}).prod (\lam x, f x.1), and the right is t.prod (\lam x : A, f x)

Mario Carneiro (Jul 29 2020 at 17:40):

so you need something that talks about applying an injection (in this case x.1) to change the index type

Mario Carneiro (Jul 29 2020 at 17:44):

I'm surprised this or something like it hasn't been proved yet. Anyway the general theorem about index changes is prod_bij

Marc Masdeu (Jul 29 2020 at 17:45):

Do mem_to_finset or coe_to_finset help? I don't know if you are trying a socratic dialogue here...

Mario Carneiro (Jul 29 2020 at 17:46):

You should start the proof by applying prod_bij, which has a ton of assumptions that you can fill in

Marc Masdeu (Jul 29 2020 at 17:47):

OK, I'll try.

Mario Carneiro (Jul 29 2020 at 17:48):

You won't need mem_to_finset and such because to_finset doesn't appear in the statement anymore

Marc Masdeu (Jul 29 2020 at 17:52):

When I apply prod_bij, some of the goals contain a m_1. This means that it couldn't figure out what I really was applying, right?

Marc Masdeu (Jul 29 2020 at 17:53):

This is the first goal:

  (a : s) (ha : a  finset.univ), ?m_1 a ha  t

Mario Carneiro (Jul 29 2020 at 17:54):

If you use refine prod_bij _ _ _ _ _ _ _, you can give the functions in the first few underscores, so that you don't get any ?m_1 a ha business

Mario Carneiro (Jul 29 2020 at 17:57):

I think the function is \lam x _, x.1

Marc Masdeu (Jul 29 2020 at 18:12):

lemma two_products {α β: Type*} {s : set α} [fintype s] [comm_monoid β] {t : finset α} {f : α  β}
 (h:  x, x  s  x  t) : ( g : s, f g) = ( g in t, f g) :=
begin
refine finset.prod_bij (λ x _, x.1) _ _ _ _,
{
  intros a ha,
  specialize h a,
  apply h.mp,
  exact subtype.mem a,
},
{
  intros a ha,
  refl,
},
{
  intros a1 a2 h1 h2,
  exact subtype.eq,
},
{
  intros b hb,
  specialize h b,
  use b,
  rw h,
  exact hb,
  split,
  apply finset.mem_univ,
  exact rfl,
}
end

Patrick Massot (Jul 29 2020 at 18:19):

This all sounds like issues that were obviously solved in mathcomp before formalizing the odd order theorem, but this observation is taboo here.

Mario Carneiro (Jul 29 2020 at 18:21):

This is a hole in the library. Of course the proof isn't nice

Mario Carneiro (Jul 29 2020 at 18:21):

the correct proof is to cite this theorem

Mario Carneiro (Jul 29 2020 at 18:21):

but the theorem didn't exist

Marc Masdeu (Jul 29 2020 at 18:22):

Is anyone working in improving the user experience with sets/finsets/fintypes and the like? It is basic enough that it can cause problems in many places...

Marc Masdeu (Jul 29 2020 at 18:23):

Patrick Massot said:

This all sounds like issues that were obviously solved in mathcomp before formalizing the odd order theorem, but this observation is taboo here.

Please elaborate, the story sounds potentially interesting!

Mario Carneiro (Jul 29 2020 at 18:26):

The best way to solve these problems is to have a really complete library of basic lemmas

Mario Carneiro (Jul 29 2020 at 18:27):

finset itself has a fairly complete API, and big_operators do too, for the most part. Like I said I'm surprised this was missed

Mario Carneiro (Jul 29 2020 at 18:28):

I see that algebra.big_operators.basic doesn't import fintype so it's impossible to state this theorem in that file. So maybe it is in another file and I missed it

Patrick Massot (Jul 29 2020 at 18:28):

Marc, the story is: some very smart people spend six years working on how to do finite groups in a proof assistant very close to Lean. They wrote several papers about the clever tricks they found the most useful. Sentences like "Well for me the most confusing thing is that I deal at the same time with a group and a subgroup of it," were at the heart of those papers. So we ignore them.

Mario Carneiro (Jul 29 2020 at 18:28):

I didn't watch closely when algebra.big_operators got split into pieces

Mario Carneiro (Jul 29 2020 at 18:31):

eh, found it

Mario Carneiro (Jul 29 2020 at 18:31):

src#finset.prod_subtype

Patrick Massot (Jul 29 2020 at 18:32):

In the same way, there is a huge subgroup refactor going on. Those Coq people told us repeatedly that they found a very simple criterion to see whether we get this right: painlessly state and prove the third isomorphism theorem. So we invest a lot of time in the refactor and never discuss how this test will go once the refactor will be done (I asked the question several time and never got any answer).

Marc Masdeu (Jul 29 2020 at 18:41):

Do you think that the 3rd iso theorem will go bad after this, then??

Kevin Buzzard (Jul 29 2020 at 18:44):

Patrick, my impression in the odd order work is that they solve this by never talking about the cardinality of a type. Every group is a subgroup of a large ambient group and they only have one notion of cardinality, that of a subset of a group.

As for refactoring subgroups, I think that the third isomorphism theorem should be easy with bundled subgroups but I can't check until Friday. We have a really nice map and comap for group homs. We have N and K normal in G and N a subset of K, we have a construction making a subgroup a group. I don't envisage any problems

Mario Carneiro (Jul 29 2020 at 19:23):

Here's the statement

import group_theory.quotient_group data.equiv.mul_add

variables {α : Type*} [group α]

def image_normal {G H} [group G] [group H]
  (f : G  H) [is_group_hom f] (hf : function.surjective f)
  (s : set G) [normal_subgroup s] : normal_subgroup (f '' s) :=
begin
  rintro _ a, h, rfl b,
  obtain b, rfl := hf b,
  refine ⟨_, normal_subgroup.normal a h b, _⟩,
  rw [is_mul_hom.map_mul f, is_mul_hom.map_mul f, is_group_hom.map_inv f],
end

structure normal_subgroup' (α) [group α] :=
(carrier : set α) [is_normal : normal_subgroup carrier]

attribute [instance] normal_subgroup'.is_normal

def to_subgroup (s : normal_subgroup' α) : subgroup α := subgroup.of s.carrier

instance normal_subgroup'.coe_subgroup : has_coe (normal_subgroup' α) (subgroup α) := to_subgroup

instance normal_subgroup'.coe_normal_subgroup (s : normal_subgroup' α) :
  normal_subgroup (s : set α) := normal_subgroup'.is_normal _

instance normal_subgroup'.coe_coe_normal_subgroup (s : normal_subgroup' α) :
  normal_subgroup ((s : subgroup α) : set α) := normal_subgroup'.is_normal _

instance : preorder (normal_subgroup' α) := preorder.lift normal_subgroup'.carrier

def normal_subgroup'.image {G H} [group G] [group H] (f : G →* H) (hf : function.surjective f)
  (s : normal_subgroup' G) : normal_subgroup' H :=
by haveI := image_normal f hf s; exact f '' s

namespace quotient_group

def quotient' [group α] (s : normal_subgroup' α) : Type* := quotient ((s : subgroup α) : set α)

variables [group α] {s : normal_subgroup' α}

instance quotient_group.group' (s : normal_subgroup' α) : group (quotient' s) :=
quotient_group.group s

def mk' : α  quotient' s := quotient.mk'

instance mk'.is_group_hom : is_group_hom (mk' : α  quotient' s) := quotient_group.is_group_hom _

def mk_hom : α →* quotient' s := monoid_hom.of mk'

variable (s)
def below (t : normal_subgroup' α) : normal_subgroup' (quotient' s) :=
t.image mk_hom $ by rintro i⟩; exact ⟨_, rfl

end quotient_group

theorem third_isomorphism_thm {G} [group G] {H K : normal_subgroup' G} (h : H  K) :
  quotient_group.quotient' (quotient_group.below H K) * quotient_group.quotient' H :=
sorry

Mario Carneiro (Jul 29 2020 at 19:25):

the proof is easier if you have all the hom functions doing equalizer tricks

Kevin Buzzard (Jul 29 2020 at 20:11):

is_group_hom is deprecated

Mario Carneiro (Jul 29 2020 at 20:20):

I know?

Mario Carneiro (Jul 29 2020 at 20:20):

For the purpose of simplifying the proof, I'm using the deprecated lemmas to prove the bundled ones. In a proper refactor you would rewrite the proofs

Mario Carneiro (Jul 29 2020 at 20:22):

The hard part here, as ever, is just setting up statements - ignore the proofs, which are all trivial anyway

Mario Carneiro (Jul 29 2020 at 20:22):

I only had to prove one theorem about is_group_hom which was missing from the library (image_normal)

Kevin Buzzard (Jul 29 2020 at 20:30):

In the bundling subgroup refactor we still don't bundle normal subgroups. I don't know what I feel about this. In the group theory game we're going to bundle them

Mario Carneiro (Jul 29 2020 at 20:32):

I know, I wondered about this as well. I think there is a good argument for bundling them - quotient is naturally a function on it, and the whole family ker/im/map/comap/ complete lattice structure exists for them

Mario Carneiro (Jul 29 2020 at 20:33):

the downside is that now we have a more complicated coercion graph

Marc Masdeu (Jul 30 2020 at 10:46):

OK, back to finsets... Here's a puzzle which doesn't involve unions and the such:

variables {G : Type*} [comm_group G] [fintype G]

lemma fintype_card_eq_finset_card' : fintype.card G =
       finset.card ((( : subgroup G) : set G).to_finset):=
begin
    sorry
end

Kenny Lau (Jul 30 2020 at 10:49):

import data.fintype.card group_theory.subgroup

variables {G : Type*} [comm_group G] [fintype G]

open_locale classical

lemma fintype_card_eq_finset_card' :
  fintype.card G = finset.card ((( : subgroup G) : set G).to_finset):=
begin
  unfold fintype.card, congr, rw subgroup.coe_top, convert set.to_finset_univ.symm,
end

Kenny Lau (Jul 30 2020 at 10:49):

we need @Kevin Buzzard 's fincard

Marc Masdeu (Jul 30 2020 at 10:55):

Thanks for teaching me the convert tactic, @Kenny Lau !

Kenny Lau (Jul 30 2020 at 10:55):

cheers

Kevin Buzzard (Jul 30 2020 at 11:15):

I don't know if I pushed it to the group theory game repo. If I didn't then it's inaccessible until Friday evening

Marc Masdeu (Jul 31 2020 at 14:29):

Thanks to @Johan Commelin, @Kenny Lau , @Kevin Buzzard, @Mario Carneiro (and probably others that on Zulip that I am forgetting) I have managed to formalize (the proof of) a non-trivial group-theory statement:

theorem prod_identity_general {G : Type*} [comm_group G] [fintype G] {g : G} (h1 : g  1) (h2 : g * g = 1) :
 ( x : G, x) = g^(fintype.card (two_torsion_subgroup G) / 2)

I'll try next to apply it to (Z/nZ)^*...

Carl Friedrich Bolz-Tereick (Aug 01 2020 at 01:26):

Awesome! Is your code online somewhere?


Last updated: Dec 20 2023 at 11:08 UTC