Proving that C2 inside Z/n has size 2

Stream: new members

[Marc Masdeu]

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]

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]

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

[Marc Masdeu]

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

[Marc Masdeu]

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]

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

[Scott Morrison]

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]

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.