Zulip Chat Archive

Stream: new members

Topic: Proving that C2 inside Z/n has size 2


Marc Masdeu (Sep 02 2020 at 15:47):

Hi,

I have defined a usually-two-element subgroup C2 of zmod n:

def C2 (m : ) : subgroup (units (zmod m)) :=
{
    carrier := {1, -1},
    one_mem' := by simp,
    mul_mem' := λ a b (ha : a  {1, -1}) (hb : b  {1, -1}), by finish,
    inv_mem' := λ a (ha : a  {1, -1}), by finish,
}

(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

I want to prove that, if m > 2, then C2 (m) has size 2:

lemma one_neq_minus_one {m :  } (h : 2 < m) : \not (1 : units (zmod m)) = (-1 : units (zmod m)) :=
begin
    sorry
end

lemma two_torsion_subgroup_has_two_elements {m :  } (h : 2 < m) :
   fintype.card (C2 (m)) = 2 :=
begin
    sorry
end

I know how to prove the first lemma, I just want to prove the second one (which has no mathematical content, given the definition of C2 and the first lemma). Any hints?

Aside: I know that @Kevin Buzzard has twitched about finset, fincard,... and what I took of it is that it was a moving target mess. Is this still the case, or there have been any changes in mathlib?

Reid Barton (Sep 02 2020 at 15:49):

the strategy should be something like

  • fintype.card s = finset.card s
  • if x \notin s then finset.card (insert x s) = finset.card s + 1
  • if x \ne y then x \notin {y}

Reid Barton (Sep 02 2020 at 15:49):

There may also be some existing lemmas to shortcut the last steps

Marc Masdeu (Sep 02 2020 at 16:03):

I don't know how to write the first in Lean ( finset.card C2(p^r) does not typecheck)...

Marc Masdeu (Sep 02 2020 at 17:32):

Done! Thanks @Reid Barton ! It took me a while to see how these three statements would help me, but it was a neat exercise.

lemma two_torsion_subgroup_has_two_elements (h : 2 < m) :
   fintype.card (C2 (m)) = 2 :=
begin
    tactic.unfreeze_local_instances,
    dsimp at *,
    let S : finset (units (zmod m)) := {1, -1},
    have H :  x : units (zmod m), x  S  x  C2 m,
    {
        intro x,
        split;
        {
            intro hx,
            try {rw C2_mem at hx},
            finish,
        }
    },
    suffices : finset.card S = 2,
    {
        rw this,
        exact fintype.card_of_subtype S H,
    },
    have h1 :  (x : units (zmod m)),  (T : finset(units(zmod m))), (x  T  finset.card (insert x T) = finset.card T + 1),
    {
        intros x T hx,
        exact finset.card_insert_of_not_mem hx,
    },
    have h2 :  (x y: units (zmod m)), x  y  x  {y} := λ {a b : units (zmod m)}, finset.not_mem_singleton.mpr,
    specialize h2 1 (-1) (one_neq_minus_one h),
    let S' : finset (units (zmod m)) := {-1},
    specialize h1 1 S' h2,
    assumption,
end

Yakov Pechersky (Sep 02 2020 at 18:13):

Not sure how you defined the fintype instance on C2. What's the unfreeze step for?

Scott Morrison (Sep 03 2020 at 03:26):

Marc Masdeu said:

(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

When you're writing strutures and want more context, you can:

  • use an _, and Lean will show you the expected type at that position
  • use begin ... end to define a field, and you'll have the usual goal view. Usually once you've worked out what you're doing you'll want to "golf" this back to a term, if possible (at least for data fields)
  • you can also build structures entirely inside tactic mode, using refine_struct { .. } or indeed just fsplit (again, you may want to golf)
  • there is a hole command (type {| |}, and click on the light bulb) which can provide a "skeleton" for a structure definition, writing out the names of the fields you need to provide

Johan Commelin (Sep 03 2020 at 04:10):

Scott Morrison said:

Marc Masdeu said:

(I hope that this definition is correct. VSCode is not helping me in providing the context while writing this bit).

  • there is a hole command (type {| |}, and click on the light bulb) which can provide a "skeleton" for a structure definition, writing out the names of the fields you need to provide

The hole command also works with _ nowadays, so you can combine this point with the first point.


Last updated: Dec 20 2023 at 11:08 UTC