card

Stream: new members

[Alex Zhang]

Is there any built-in lemma that picks distinct elements of a given type such as picking three as follows?

import data.fintype.card
variables {I : Type*} [fintype I] [nonempty I]
open fintype
lemma Hadamard_matrix.order_aux1 (h1 : card I ≠ 1) (h2 : card I ≠ 2) :
∃ i j k : I, i ≠ j ∧ i ≠ k ∧ j ≠ k :=
sorry

My formulation might be bad btw.

[Kevin Buzzard]

I would first prove card >= 3 and then dig into the definition of fintype

[Alex Zhang]

An easier one is perhaps

import data.fintype.card
variables {I : Type*} [fintype I] [nonempty I]
open fintype
lemma ex2 (h1 : card I ≠ 1) :
∃ i j: I, i ≠ j:=
begin
  have i:= classical.arbitrary I,
  use I,
 sorry,
end

[Alex Zhang]

A generalized one

lemma ex {n : ℕ} (h : card I ≥ n) :
∃ (a : (fin n) → I), ∀ i j, i ≠ j → a i ≠ a j :=
sorry

[Alex Zhang]

Are there any relevant or equivalent built-in lemmas to the above ones?

[Shing Tak Lam]

Alex Zhang said:

An easier one is perhaps

import data.fintype.card
variables {I : Type*} [fintype I] [nonempty I]
open fintype
lemma ex2 (h1 : card I ≠ 1) :
∃ i j: I, i ≠ j:=
begin
  have i:= classical.arbitrary I,
  use I,
 sorry,
end

I think the case where the size isn't 1 is probably quite a bit easier than the general case

import data.fintype.card
variables {I : Type*} [fintype I] [nonempty I]
open fintype
lemma ex2 (h1 : card I ≠ 1) :
∃ i j: I, i ≠ j:=
begin
  by_contra h,
  push_neg at h,
  apply h1,
  rw fintype.card,
  let i : I := classical.arbitrary I,
  have h2 : {i} = (finset.univ : finset I),
  { rw finset.eq_univ_iff_forall,
    intros x,
    rw finset.mem_singleton,
    apply h },
  simp [←h2]
end

[Alex Zhang]

@Shing Tak Lam Do you have any idea about ex3 and ex?

[Alex Zhang]

I will read your proof in detail after a nap.

[Eric Wieser]

This is quite straightforward:

import data.fintype.card

variables {I : Type*} [fintype I]

open fintype

lemma ex1 (h1 : card I = 3) : ∃ i j k : I, i ≠ j ∧ i ≠ k ∧ j ≠ k :=
begin
  have f := equiv_fin_of_card_eq h1,
  refine ⟨f.symm 0, f.symm 1, f.symm 2,
    and.imp f.symm.injective.ne (and.imp f.symm.injective.ne f.symm.injective.ne) _⟩,
  sorry -- `0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2`, all in `fin 3`
end

I don't know how to close those fin goals, but they're at least "very obviously true" rather than "handwavingly true"

[Shing Tak Lam]

dec_trivial works for the sorry there

[Alex Zhang]

equiv_fin_of_card_eq is the lemma I am looking for!!

[Eric Wieser]

A fin_embedding_of_lt_card would be convenient for your use case

[Yakov Pechersky]

docs#fin.cast_le_order_iso would help

[Eric Wieser]

Maybe something like this:

def trunc_fin_embedding_of_card_eq {α} [fintype α] [decidable_eq α] {n : ℕ} (h : n ≤ fintype.card α) :
  trunc (fin n ↪ α) :=
(trunc_equiv_fin α).map (λ e, (fin.cast_le h).to_embedding.trans e.symm.to_embedding)

def trunc_embedding_fin_of_card_le {α} [fintype α] [decidable_eq α] {n : ℕ} (h : fintype.card α ≤ n) :
  trunc (α ↪ fin n) :=
(trunc_equiv_fin α).map (λ e, e.to_embedding.trans (fin.cast_le h).to_embedding)

[Yakov Pechersky]

This is all pretty #xy. It's easier to just postulate the existence of such elements, then show the cardinality of their finset is le than the cardinality of the fintype.

[Alex Zhang]

Is there any version of coded lemma stating that the card of the unit group of a finite field F is exactly F.card - 1?
Also not exactly sure what the definition of "the unit group of finite field" in mathlib will be handy and is supposed to be used. Perhaps units F?

[Kevin Buzzard]

You should think about how you want to prove this and write down a step-by-step proof and then formalise it. My advice: stop using natural number subtraction, it just makes your life worse. Rewrite everything as addition.

[Kevin Buzzard]

Why not explicitly write an equiv between F and option (units F) and then deduce the addition version from results about card of option?

[Johan Commelin]

@Alex Zhang Did you look at src/field_theory/finite/basic.lean?

[Alex Zhang]

Ah, I found it! finite_field.card_units

theorem finite_field.card_units {K : Type u_1} [field K] [fintype K] :
fintype.card (units K) = fintype.card K - 1

[Alex Zhang]

I defined the set of quadratic residues in a finite field F, then I want to prove the card of it is half of the unit group of F, as formalised in the code.
I gave three definitions in the #mwe (not quite sure which one is the most convenient for proving this). Could anyone please point me a direction for proving this equality? The way I currently think of is to use some version of
card (im f) * card (kernel f) = card units F as f is a group hom (not sure if it is the correct or a convenient way).

import tactic
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

variable (F)

def f := λ a : F, a * a

def quad_residues : set F := (λ a, a * a) '' ((@set.univ F) \ {0})

-- alternative defns
def quad_residues' := {b // ∃ a, a ≠ 0 ∧ a * a = b}
def quad_residues'' := {b // ∃ (a : units F), a * a = b}

instance : fintype (quad_residues F) := sorry

example (h: p ≠ 2) : (quad_residues F).to_finset.card * 2 = fintype.card F - 1 := sorry

[Yakov Pechersky]

Is it possible to construct an explicit isomorphism, even if it is noncomputable?

[Yakov Pechersky]

You could define is_quad_residue as a Prop, and use that in a finset.filter instead.

[Alex Zhang]

Would this def be helpful for proving the equality?

[Alex Zhang]

Ah, I found the defn of "kernel". https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#monoid_hom.ker
and I will leave for dinner for now.

[Yakov Pechersky]

How about this?

import tactic
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic

variables {F : Type*} [field F]

def is_quad_res (x : F) : Prop := ∃ (y : F), y ≠ 0 ∧ y * y = x

variables [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

open_locale classical

example (h: p ≠ 2) : ((finset.univ : finset F).filter is_quad_res).card = fintype.card F - 1 :=
begin
end

[Yakov Pechersky]

Is this correct?

variable (F)
def sq_hom : units F →* units F :=
⟨λ x, x * x, by simp, λ _ _, by simp [mul_assoc, mul_comm, mul_left_comm]⟩

variable {F}
lemma sq_hom_res_iff {p : ℕ} [char_p F p]
  (x : units F) : x ∈ (sq_hom F).ker ↔ is_quad_res (x : F) := sorry

[Alex Zhang]

example (h: p ≠ 2) : ((finset.univ : finset F).filter is_quad_res).card = fintype.card F - 1 :=
should be
example (h: p ≠ 2) : ((finset.univ : finset F).filter is_quad_res).card * 2 = fintype.card F - 1 :=

[Kevin Buzzard]

No. The squaring function has a kernel and an image. The quadratic residues are the stuff in the image. If p>2 then the kernel is +-1 which has size 2. Hence the first isomorphism theorem says that twice the size of the image equals the size of the units (Alex' version correctly adds this factor of 2)

[Kevin Buzzard]

The units of a finite field are cyclic, although this is not obvious. The quadratic residues are a subgroup, so they must hence be the kernel of the map raising a unit to the power (c-1)/2 where c is the size of the field

[Alex Zhang]

Yes, Kevin. I am still looking for the first iso thm in mathlib. Do you have any suggestion for proving the card equality? @Kevin Buzzard

[Kevin Buzzard]

Yes, use the first isomorphism theorem!

[Yakov Pechersky]

Yes, sorry for the missing * 2 typo. Thanks Kevin for the clarification, I was going through the proof using powers of (p - 1) / 2 and realized that I must have meant image and not kernel.

[Alex Zhang]

I found the first iso thm: https://leanprover-community.github.io/mathlib_docs/group_theory/quotient_group.html#quotient_group.quotient_ker_equiv_range

[Alex Zhang]

But there are still some gaps to card.

[Alex Zhang]

Ah, https://leanprover-community.github.io/mathlib_docs/group_theory/coset.html#subgroup.card_eq_card_quotient_mul_card_subgroup
seems to be useful

[Alex Zhang]

It is weird. Why can't ring close

import tactic
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic

variables {F : Type*} [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

variable (F)
def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by {ring})⟩

[Yakov Pechersky]

def sq_hom : units F →* units F :=
⟨λ x, x * x, by simp, λ _ _, by simp [mul_assoc, mul_comm, mul_left_comm]⟩

[Yakov Pechersky]

units F is not a ring.

[Yakov Pechersky]

def sq_hom : units F →* units F :=
⟨λ x, x * x, by simp, λ _ _, by simp [units.ext_iff]; ring⟩

[Yakov Pechersky]

import tactic
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic
import group_theory.quotient_group


variables {F : Type*} [field F]

def is_quad_res (x : F) : Prop := ∃ (y : F), y ≠ 0 ∧ y * y = x

lemma is_quad_res.ne_zero {x : F} (h : is_quad_res x) : x ≠ 0 :=
begin
  obtain ⟨y, hy, rfl⟩ := h,
  exact mul_ne_zero hy hy
end

variables [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]

variable (F)
def sq_hom : units F →* units F :=
⟨λ x, x * x, by simp, λ _ _, by simp [mul_assoc, mul_comm, mul_left_comm]⟩

variable {F}
lemma sq_hom_res_iff
  (x : units F) : x ∈ (sq_hom F).range ↔ is_quad_res (x : F) :=
begin
  simp only [sq_hom, is_quad_res, ne.def, monoid_hom.mem_range, monoid_hom.coe_mk],
  split,
  { rintro ⟨y, hy⟩,
    refine ⟨(y : F), _, _⟩,
    { simp only [units.ne_zero, not_false_iff] },
    { simp [←hy] } },
  { rintro ⟨y, hn, hy⟩,
    have key : is_unit y := is_unit.mk0 y hn,
    use key.unit,
    simp [units.ext_iff, key.unit_spec, hy] }
end

example [decidable_pred (@is_quad_res F _)] (h: p ≠ 2) :
  ((finset.univ : finset F).filter is_quad_res).card * 2 = fintype.card F - 1 :=
begin
  rw ←finite_field.card_units,
  -- probably some neater way of constructing this, but who cares
  let iso : ((finset.univ : finset F).filter is_quad_res ≃ (sq_hom F).range),
  { refine equiv.trans _ (equiv.subtype_equiv_right (λ x, (sq_hom_res_iff x).symm)),
    refine ⟨_, _, _, _⟩,
    { intro y,
      refine ⟨(is_unit.mk0 (y : F) (is_quad_res.ne_zero _)).unit, _⟩,
      { simpa using y.prop },
      { simpa [is_unit.unit_spec] using y.prop } },
    { rintro y,
      refine ⟨((y : units F) : F), _⟩,
      simpa using y.prop },
    { intro x,
      simp [is_unit.unit_spec] },
    { rintro ⟨x, hx⟩,
      simp [units.ext_iff, is_unit.unit_spec] } },
  have : ((finset.univ : finset F).filter is_quad_res).card = fintype.card (sq_hom F).range,
  { rw ←fintype.card_coe,
    convert fintype.card_congr iso },
  rw this,
  rw eq_comm,
  rw subgroup.card_eq_card_quotient_mul_card_subgroup ((sq_hom F).ker),
  congr' 1,
  { refine fintype.card_congr _,
    exact (quotient_group.quotient_ker_equiv_range _).to_equiv },
  { -- The kernel is {1, -1}, prove that elsewhere
    -- this is actually where the `(h : p ≠ 2)` hypothesis needs to be used
    sorry }
end

[Alex Zhang]

Cool, Yakov! I am also getting to the final part to prove that the card of the kernel is 2. Do you have any idea of proving that? @Yakov Pechersky

[Kevin Buzzard]

factor the quadratic?

[Yakov Pechersky]

Relatedly, a simpler puzzle:

lemma sq_hom_ker_eq_char_2 (h : p = 2) :
  (sq_hom F).ker = ⊥ :=
begin
  unfreezingI { subst h },
  refine le_antisymm (λ x hx, _) bot_le,
  simp only [monoid_hom.mem_ker, sq_hom, monoid_hom.coe_mk] at hx,
  simp only [subgroup.mem_bot],
  sorry
end

[Alex Zhang]

Thanks a lot for the proof!!

[Yakov Pechersky]

lemma sq_hom_ker_eq_char_2 (h : p = 2) :
  (sq_hom F).ker = ⊥ :=
begin
  unfreezingI { subst h },
  refine le_antisymm (λ x hx, _) bot_le,
  simp only [monoid_hom.mem_ker, sq_hom, monoid_hom.coe_mk, units.ext_iff, units.coe_one,
             units.coe_mul] at hx,
  rw ←pow_two at hx,
  haveI : fact (nat.prime 2) := ⟨nat.prime_two⟩,
  let iso : F ≃+* zmod 2,
  { refine (zmod.ring_equiv F _).symm,
    sorry
  },
  simp only [subgroup.mem_bot, units.ext_iff],
  apply iso.injective,
  have : ∀ z, iso z = iso.to_monoid_hom z,
  { intro,
    refl },
  simp [←hx, this]
end

[Alex Zhang]

Why is the goal at sorry fintype.card F = 2?

[Kevin Buzzard]

Are you claiming that every finite field of characteristic 2 has two elements? This is not true.

[Kevin Buzzard]

There's a field with elements 0,1,a,b with a^2=a+1=b and b^2=b+1=a. It has characteristic 2 and order 4.

[Alex Zhang]

Kevin Buzzard said:

Are you claiming that every finite field of characteristic 2 has two elements? This is not true.

I feel I got back to my third year (or second year) algebra course although I have got very sleepy :)

[Alex Zhang]

I have not set about proving card ker is 2 myself as I am too sleepy now.

[Yakov Pechersky]

I see, apologies for the wrong statement! I have never actually taken algebra at that level, and have been trying to learn it myself.

[Alex Zhang]

You have already given many helpful answers, Yakov. Many thanks! @Yakov Pechersky

[Yakov Pechersky]

I was not sure how to get Fermat's Little Theorem to work on arbitrary finite fields, but we have it for zmod p. So I faked it =/

[Kevin Buzzard]

Just like you can make the complexes by starting with the reals and throwing in a root of a real quadratic which doesn't have a real root, you can do the same with the field with two elements, throwing in a root of X^2=X+1. This polynomial mod 2 doesn't have 0 or 1 as a root, so throw a root in and you get something 2-dimensional over {0,1}.

[Kevin Buzzard]

Fermat's little theorem follows from the theorem in group theory that the order of the element divides the order of the group, applied to the unit group. This does not need the deeper fact that this group is cyclic

[Yakov Pechersky]

Ah, of course! I was just formalizing notes from Gross's class about this.

[Alex Zhang]

I have proved the card of the ker is 2, but have not sorted things out.

[Yakov Pechersky]

Did you prove it by explicitly showing that the ker is 1 and -1 for the appropriate p?

[Alex Zhang]

Yes, doing something like

lemma f_0 : (f F).ker.carrier = {1, -1} :=
begin
  rw ker,
  simp [f_ker, subgroup.comap, set.preimage, f],
  ext,
  simp,
  split,
  any_goals {intro h},
  { rw units.ext_iff at h,
    simp at h,
    have h' : ((x : F) + 1) * (x - 1) = 0,
    {simp [add_mul, mul_sub, h], ring},
    simp at h',
    cases h',
    {right, simp [units.ext_iff, eq_neg_of_add_eq_zero h'],},
    {left, simp [units.ext_iff, sub_eq_zero.mp h']}
  },
  cases h; simp [h]
end

[Yakov Pechersky]

Golfed:

lemma sq_hom_ker_eq : (sq_hom F).ker.carrier = {1, -1} :=
begin
  ext x,
  simp only [monoid_hom.mem_ker, set.mem_insert_iff, subgroup.mem_carrier, set.mem_singleton_iff,
             sq_hom, monoid_hom.coe_mk, units.ext_iff, units.coe_mul, units.coe_one, units.coe_neg],
  refine ⟨λ h, _, λ h, _⟩,
  { have h' : ((x : F) + 1) * (x - 1) = 0,
    { rw [add_mul, mul_sub, h], ring },
    rw mul_eq_zero at h',
    exact h'.symm.imp eq_of_sub_eq_zero eq_neg_of_add_eq_zero },
  { cases h;
    simp [h] }
end

[Damiano Testa]

Is there a way to recycle mul_self_eq_one_iff more efficiently? I feel that the proof of units.sq_one should be much shorter...

lemma monoid_hom.ker_mul_self {x : units F} : x ∈ monoid_hom.ker (sq_hom F) ↔ x * x = 1 := iff.rfl

lemma units.sq_one {F : Type*} [integral_domain F] {x : units F} :
  x * x = 1 ↔ x = 1 ∨ x = - 1 :=
begin
  convert @mul_self_eq_one_iff F _ x using 1; refine eq_iff_iff.mpr _,
  { exact ⟨congr_arg coe, λ h, units.eq_iff.mp h⟩ },
  { refine ⟨_, _⟩; rintros (h | h),
    { exact or.inl (by simp [h]) },
    { exact or.inr (by simp [h]) },
    { exact or.inl (by simpa using h) },
    { exact or.inr (units.ext (by simpa using h)) } },
end

lemma f_0 : (sq_hom F).ker.carrier = {1, -1} :=
by ext; simp [monoid_hom.ker_mul_self, units.sq_one]

[Damiano Testa]

Also, note that it might make sense to develop some API for the slightly more general version of sq_hom below.

def mul_self_hom (F : Type*) [comm_monoid F] : F →* F :=
⟨λ x, x * x, mul_one _, λ _ _, mul_mul_mul_comm _ _ _ _⟩

Your version, would be the above applied to units F.

Possibly, even for the more general nat-power map

def pow_self_hom (F : Type*) [comm_monoid F] (n : ℕ) : F →* F :=
⟨λ x, x ^ n, one_pow _, λ _ _, mul_pow _ _ _⟩

[Kevin Buzzard]

IIRC this map is already in mathlib

[Kevin Buzzard]

Or perhaps there's an old skool is_monoid_hom instance on the power map

[Damiano Testa]

Ah, in either case, it might make sense to generalize some of the lemmas above to work for this more general setting.