lagrange theorem declaration

Stream: new members

[Thomas Laraia]

I am working on partitioning G into the left cosets of H, and my last hiccup is the equality of any given section of the partition with a left coset of H. I see that the issue is using =, but I'm not sure what I could use in its stead to complete the statement.

import tactic
import group_theory.coset
import data.set.basic
import group_theory.order_of_element

@[ext] structure partition (α : Type) :=
(C : set (set α))
(Hnonempty : ∀ X ∈ C, (X : set α).nonempty)
(Hcover : ∀ a, ∃ X ∈ C, a ∈ X)
(Hdisjoint : ∀ X Y ∈ C, (X ∩ Y : set α).nonempty → X = Y)

variables {G : Type} [fintype G] [group G]
variable (H : subgroup G)

open partition

lemma lagrange (P : partition G) (h: ∀ (X : P.C), ∃ (g : G), X = left_coset g H ) :
fintype.card H ∣ fintype.card G := --the size of the subgroup H divides the size of the group G
begin
  sorry,
  --partition G into left cosets of H
  --G is finite, so exists g₁, g₂, ..., gₖ s.t. g₁H, ..., gₖH partition G,
  --Then |G| = |g₁H| + |g₂H| + ... + |gₖH|
  --         = |H| + |H| + ... |H|
  --         = k|H|, k is number of distinct left cosets of H in H
  --Thus |H| divides |G| and the goal is fulfilled
end

[Eric Wieser]

I think you have confused : and ∈ there; this works: lemma lagrange (P : partition G) (h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H ) :

[Eric Wieser]

Although your hypothesis isn't needed, and the statement is already in mathlib: docs#subgroup.card_subgroup_dvd_card:

/-- the size of the subgroup H divides the size of the group G -/
lemma lagrange (P : partition G) [fintype H] (h : ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H) :
  fintype.card H ∣ fintype.card G :=
H.card_subgroup_dvd_card  -- oops I didn't use `h` or `P` at all

[Thomas Laraia]

Do you need to declare H as fintype if you've done so for G and make H a subgroup of G?

[Eric Wieser]

Yes, because you want your lemma to say "this works for any proof that H is finite, not just the one derived by filtering G"

[Eric Wieser]

For your case it probably doesn't matter, but that's why mathlib has both

[Eric Wieser]

(also, you can't derive it by filtering G unless you have [decidable_pred (∈ H)])

[Thomas Laraia]

import group_theory.coset
import data.set.basic
import group_theory.order_of_element
import data.fintype.basic
import week_1.Part_D_relations


variables {G : Type} [fintype G] [group G]
variables (H : subgroup G) [fintype H]

open function

lemma coset_sizes_long : ∀ (g : G), fintype.card (left_coset g H) = fintype.card H :=
begin
  intro g,
  let f := (λ H, left_coset g H),
  --I take issue with only needing to show injection to prove bijection
  --I'm not convinced the function should be from set G to set G
  --or at least cannot be implied that easily
  --the proof from FPM we proved both injection and surjection
  --we need map H → gH
  have h₂ : injective f,
  {refine set.image_injective.mpr _,
  dsimp,
  exact mul_right_injective g,
  },
  have h₃ : bijective f,
  exact fintype.injective_iff_bijective.mp h₂,
  have h₄ : H ≃ left_coset g H,
  {sorry,},
  exact fintype.card_congr (equiv.symm h₄),
end

Yeah just in a spot of pain. I see that I can pretty much jump to the end using

lemma coset_sizes : ∀ (g : G), fintype.card (left_coset g H) = fintype.card H :=
begin
  intro g,
  have h₄ : H ≃ left_coset g H,
  exact (subgroup.left_coset_equiv_subgroup g).symm,
  exact fintype.card_congr (equiv.symm h₄),
end

but that just skips the whole part where I learn.
I see why Lean thinks it only needs to be injective, as then since we're going from set G to set G and G is finite, the function is bijective, but then I must've defined something incorrectly because I'm fairly sure you need to prove both injection and surjection.

[Eric Wieser]

(The first code snippet is highlighted badly because you forgot the line break between ``` and import tactic)

[Thomas Laraia]

right, cheers for highlighting that

[Eric Wieser]

I think src#injective_iff_surjective is the core of the thing you take issue with

[Thomas Laraia]

Sorry if this is a bit long but I'm checking if we've accidentally done something like used a fact to prove a fact. In proving Lagrange's Theorem we didn't end up making a partition but we did use the injective function and showed the cosets are disjoint. Would love to know if this is a solid proof, no worries if it's a bit too long/tedious to check.

import tactic
import group_theory.coset
import data.set.basic
import group_theory.order_of_element
import data.equiv.basic
import data.fintype.card
import data.finset.basic
import data.list.defs
import data.sigma.basic
import algebra.big_operators.basic

open subgroup

open function

variables {G : Type} [fintype G] [group G] (g : G)
variables (H : subgroup G) [fintype H]

lemma coset_sizes_mathlib [decidable_pred (∈ left_coset g H)]: fintype.card (left_coset g H) = fintype.card H :=
begin
  have h₄ : H ≃ left_coset g H,
  exact (subgroup.left_coset_equiv_subgroup g).symm,
  exact fintype.card_congr (equiv.symm h₄),
end

open_locale big_operators

def is_refl_type {X:Type}(S: X→ X→ Prop):= -- Def 1 --
∀ a:X, S a a

def is_symm_type {X:Type}(S: X→ X→ Prop):= -- Def 2 --
∀ a b:X, S a b→ S b a

def is_trans_type {X:Type}(S:X→ X→ Prop):= -- Def 3 --
∀ a b c:X, S a b→ S b c→ S a c

def is_equiv_type {X:Type}(S:X→ X→ Prop):= -- Def 4--
is_refl_type S ∧ is_symm_type S
∧ is_trans_type S

def equiv_class_type {X:Type}(S:X→ X→ Prop)(a:X):= -- Def 5 --
{x:X | S x a}

def left_coset_rel: G→ G→ Prop:=
λa:G,λb:G, left_coset a H = left_coset b H

lemma left_coset_rel_is_refl:is_refl_type (left_coset_rel H):=
begin
  unfold is_refl_type,
  intro a,
  unfold left_coset_rel,
end

lemma left_coset_rel_is_symm:is_symm_type (left_coset_rel H):=
begin
  unfold is_symm_type,
  intros a b f,
  unfold left_coset_rel at *,
  symmetry,
  exact f,
end

lemma left_coset_rel_is_trans:is_trans_type (left_coset_rel H):=
begin
  unfold is_trans_type,
  intros a b c f g,
  unfold left_coset_rel at *,
  rw g at f,
  exact f,
end

lemma left_coset_rel_is_equiv:is_equiv_type (left_coset_rel H):=
begin
  split,
  exact left_coset_rel_is_refl H,
  split,
  exact left_coset_rel_is_symm H,
  exact left_coset_rel_is_trans H,
end

lemma in_coset(x:G):x∈ left_coset x H:=
begin
  unfold left_coset,
  simp,
  exact one_mem H,
end

lemma equiv_class_is_coset(a:G):
equiv_class_type (left_coset_rel H) a=left_coset a H:=
begin
  ext1,
  split,

  intro f,
  unfold equiv_class_type at f,
  simp at *,
  unfold left_coset_rel at f,
  rw ← f,
  apply (in_coset H) x,

  intro g,
  unfold equiv_class_type,
  simp at *,
  rw left_coset_rel,
  ext1,
  split,
  intro h,
  unfold left_coset at *,
  simp at *,
  have temp: a⁻¹ * x_1 = (a⁻¹ * x) * (x⁻¹ * x_1):=begin
    rw mul_assoc,
    rw ← mul_assoc x x⁻¹,
    simp,
  end,
  rw temp,
  apply (mul_mem H) g h,
  intro h,
  unfold left_coset at *,
  simp at *,
  have g_inv:=(inv_mem H) g,
  simp at g_inv,
  have temp: x⁻¹ * x_1 = (x⁻¹ * a) * (a⁻¹ * x_1):=begin
    rw mul_assoc,
    rw ← mul_assoc a a⁻¹,
    simp,
  end,
  rw temp,
  apply (mul_mem H) g_inv h,
end

lemma in_equiv_class {X:Type}{S:X→ X→ Prop}
(h: is_equiv_type S)(a:X):
a∈ equiv_class_type S a:= -- Lemma 7 --
begin
  cases h with p q,
  apply p a,
end

lemma equiv_iff_same_class {X:Type}{S:X→ X→ Prop}
(h: is_equiv_type S)(a:X)(b:X):
S a b ↔ equiv_class_type S a=equiv_class_type S b
:=  -- Lemma 9 --
begin
  have rfl:=h.1,
  have sym:=h.2.1,
  have tran:=h.2.2,
  split,

  /- → -/
  intro f,
  --cases h with rfl st,
  --cases st with sym tran,
  rw set.subset.antisymm_iff,
  split,
  /- → ⊆-/
  intros x g,
  apply tran x a b g f,
  /- → ⊇ -/
  intros x g,
  have t:=sym a b f,
  apply tran x b a g t,

  /- ← -/
  intro f,
  have u:=in_equiv_class h a,
  rw f at u,
  exact u,
end

lemma equiv_iff_class_intersect{X:Type}{S:X→ X→ Prop}
(h: is_equiv_type S)(a:X)(b:X):
S a b ↔ (equiv_class_type S a ∩ equiv_class_type S b).nonempty
:= --Lemma 10 --
begin
  have rfl:=h.1,
  have sym:=h.2.1,
  have tran:=h.2.2,
  split,

  /- → -/
  intro f,
  rw set.nonempty,
  use a,
  rw set.mem_inter_eq,
  split,
  have t:=in_equiv_class h a,
  exact t,
  exact f,

  /- ← -/
  intro f,
  cases f with x fx,
  rw set.mem_inter_eq at fx,
  cases fx with fxp fxq,
  have t:=sym x a fxp,
  apply tran a x b t fxq,
end

lemma same_class_iff_intersect{X:Type}{S:X→ X→ Prop}
(h: is_equiv_type S)(a:X)(b:X): -- Lemma 11 --
equiv_class_type S a = equiv_class_type S b ↔
(equiv_class_type S a ∩ equiv_class_type S b).nonempty:=
begin
  have p:=equiv_iff_same_class h a b,
  have q:=equiv_iff_class_intersect h a b,
  rw p at q,
  exact q,
end

noncomputable def equiv.set.sigma_of_disjoint {ι α : Type*} (S : ι → set α) (hS : ∀ i j, i ≠ j → disjoint (S i) (S j)) :
  (↥⋃ i, S i) ≃ Σ (a : ι), ↥(S a) :=
{ to_fun := λ u, begin
    have h := set.mem_Union.mp u.prop,
    exact ⟨h.some, u, h.some_spec⟩,
  end,
  inv_fun := λ s, ⟨s.2, set.mem_Union.mpr ⟨s.1, s.2.prop⟩⟩,
  left_inv := λ u, subtype.ext rfl,
  right_inv := λ s, sigma.subtype_ext (begin
    dsimp,
    generalize_proofs h,
    by_contra hfst,
    apply set.not_disjoint_iff.mpr ⟨(s.snd : α), h.some_spec, s.snd.prop⟩ (hS h.some s.fst hfst),
  end) rfl }


lemma lagrange_long_sum_attempt_3
{k : ℕ} -- (P : partition G)
-- (h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H)
{γ : fin k → G}
{h₂ : injective (λ i, left_coset (γ i) H)}
{h₃ : (⋃(i : fin k), left_coset (γ i) H) = set.univ}
[∀ (i : fin k), decidable_pred (∈ left_coset (γ i) H)] [decidable_pred (∈ ⋃(i : fin k), left_coset (γ i) H)]:
fintype.card H ∣ fintype.card G := --the size of the subgroup H divides the size of the group G
begin
  --partition G into left cosets of H `done`

  --G is finite, so exists g₁, g₂, ..., gₖ s.t. g₁H, ..., gₖH partition G `done?`

  have h₄ : fintype.card set.univ = fintype.card G,
  exact fintype.of_equiv_card (equiv.set.univ G).symm,
  rw ← h₄,
  refine dvd_of_mul_left_eq _ _,
  exact k,
  /-have h₁ : coe_sort set.univ = coe_sort (⋃(i : fin k), left_coset (γ i) H),
  exact congr_arg coe_sort h₃.symm,
  simp_rw h₁,-/

  have h_left_coset: ∀ i j:fin k ,i≠ j→ disjoint (left_coset (γ i) H) (left_coset (γ j) H):=begin
    intros i j f,
    unfold disjoint,
    simp,
    intros x g,
    simp at *,
    cases g with g_i g_j,
    have ne:left_coset (γ i) H ≠ left_coset (γ j) H, --by h2
      unfold injective at h₂,
      by_contradiction K,
      push_neg at K,
      specialize h₂ K,
      apply f h₂,
    contrapose ne,
    simp,
    rw ← equiv_class_is_coset H at *,
    rw ← equiv_class_is_coset H at *,
    have intersect:((equiv_class_type (left_coset_rel H) (γ i))∩
    (equiv_class_type (left_coset_rel H) (γ j))).nonempty:=begin
      rw set.nonempty_def,
      use x,
      simp,
      split,
      exact g_i,
      exact g_j,
    end,
    rw same_class_iff_intersect (left_coset_rel_is_equiv H) _ _,
    exact intersect,
  end,

  have h₆ : (⋃ i, left_coset (γ i) H) ≃ (Σ i, left_coset (γ i) H),
  exact equiv.set.sigma_of_disjoint (λ (i : fin k), left_coset (γ i) ↑H) h_left_coset,

  have h₇ : fintype.card (⋃(i : fin k), left_coset (γ i) H) = fintype.card set.univ,
  have temp:(⋃(i : fin k), left_coset (γ i) H) ≃ set.univ:=equiv.cast _,
  apply fintype.card_congr temp,
  rw h₃,

  have h₅ : fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H),
  rw ← fintype.card_sigma,
  exact fintype.card_congr h₆,

  rw ← h₇,
  rw h₅,
  have : ∑ (i : fin k), fintype.card (left_coset (γ i) H) = ∑ (i : fin k), fintype.card H,

  have : ∀ (i : fin k), fintype.card (left_coset (γ i) H) = fintype.card H,
  intro i,
  exact coset_sizes_mathlib (γ i) H,
  simp_rw this,

  rw this,
  simp,
end

[Eric Wieser]

In a previous thread I showed you that equiv.set.sigma_of_disjoint already existed so there is no need to define it yourself

[Eric Wieser]

Your have ne : is docs#function.injective.ne, h₂.ne f

[Thomas Laraia]

Perfect I'll make those adjustments. Thank you for your input throughout!

[Eric Wieser]

Are you aware your is_equiv_type exists already as docs#equivalence? It's not clear to me to what extent you are trying to prove things from scratch for pedagogical reasons (as your final result is obviously in mathlib already), and to what extent you are trying to learn about and leverage other parts of mathlib.

[Thomas Laraia]

is_equiv_type is part of a parallel project that a group member is working on to define equivalence relations from the ground up. I originally used equivalence, but we wanted to prove that the left cosets formed a partition and he was more comfortable working in the foundation he laid. I would normally have used docs#equivalence otherwise.

[Thomas Laraia]

I see your point though, it's not quite consistent when I use something that already exists.

[Thomas Laraia]

We ended up not using the partition as well, which is unfortunate.