union of subgroups is the group

Stream: new members

[Thomas Laraia]

import group_theory.coset
import data.fintype.basic
import group_theory.order_of_element

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

open function

@[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)

lemma lagrange (P : partition G) (h: ∀ X, 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
  exact card_subgroup_dvd_card H,
end
--lmao I don't need any of
--`(P : partition G) (h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H )`
--this is very annoying

#check left_coset
lemma lagrange_long {k : ℕ} (P : partition G)
(h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H) {γ : fin k → G}
{h₁ : bijective γ}
{h₂ : ∀ (i j : fin k), left_coset (γ i) H ≠ left_coset (γ j) H}
{h₃ : (⋃(i : fin k), left_coset (γ i) H) = G}:
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`]
  let L := (⋃(i : fin k), left_coset (γ i) 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
  sorry,
end

I have an error in the hypothesis h₃, where I want to state that the union of all the subgroups make up the entire group, but I cannot use equality because there is a mismatch between set G and G itself. How can I get around this?

[Thomas Laraia]

Ignore the let L statement in the proof, have decided to create the union as a hypothesis in the beginning instead.

[Eric Wieser]

Can you fix the first line of your code so that it says ``` and not ```import tactic? ``` has to be on its own line, otherwise it interprets import tactic as the language to use for highlighting

[Eric Wieser]

How can I get around this?

The RHS should be set.univ G set.univ , ie "the set of all elements in G"

[Thomas Laraia]

Ah I see, I remember reading that, thank you!

[Thomas Laraia]

I have another type mismatch between set.univ G being a Prop and returning true and needing a set G. I think I can find the fix for this though, no worries.

[Thomas Laraia]

Such as perhaps (set.univ : set G).

[Eric Wieser]

Yes, you're right: docs#set.univ

[Eric Wieser]

set.univ by itself should work, it can work out set G from the LHS

[Thomas Laraia]

Is there a way then to prove that fintype.card G = fintype.card (set.univ : set G)? Seems almost trivial to say the size of a finite group is the same size as the subgroup with all the elements of the group.

[Kevin Buzzard]

import tactic
import data.fintype.card

example (G : Type) [fintype G] :
  fintype.card G = fintype.card (set.univ : set G) := by library_search

[Kevin Buzzard]

PS I would write it the other way around -- the more complex statement on the left.

[Thomas Laraia]

When I end up with a goal like fintype.card ↥H ∣ fintype.card ↥set.univ, all I want to do is dismantle the coercions that are popping up. There was the other topic where someone unfolded the coercion, but what I'm getting from that doesn't feel like guidance I know how to use.
image.png
I'll keep hacking away and maybe try another approach but have been stuck with these for a while.

[Eric Rodriguez]

can you post a #mwe? this seems like the canonical way to talk about the cardinality of a subgroup, unless maybe it's finset.card (H : set G)

[Eric Rodriguez]

there's also docs#finset.card_univ to help you on the right

[Thomas Laraia]

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

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

open function

@[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)

lemma lagrange (P : partition G) (h: ∀ X, 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
  exact card_subgroup_dvd_card H,
end
--lmao I don't need any of
--`(P : partition G) (h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H )`
--this is very annoying

lemma lagrange_long {k : ℕ} (P : partition G)
(h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H) {γ : fin k → G}
{h₁ : injective γ}
{h₂ : ∀ (i j : fin k), left_coset (γ i) H ≠ left_coset (γ j) H}
{h₃ : (⋃(i : fin k), left_coset (γ i) H) = (set.univ : set G)}:
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 : set G) = fintype.card G,
  exact fintype.of_equiv_card (equiv.set.univ G).symm,
  rw ← h₄,


  --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

[Thomas Laraia]

My next goal was to have fintype.card G to be equal to fintype.card of the union of the left cosets, and see if I could then split that up into a sum since the cosets are disjoint and there are a finite number of cosets.

[Thomas Laraia]

Although I'm not convinced I've found something in mathlib yet that I could use as a finite sum.

[Eric Wieser]

My next goal was to ....

Can you state this goal as a have?

[Thomas Laraia]

I gave that an attempt, but it I was a bit stuck using any hypotheses to rw and I don't think library_search yielded a result.

[Thomas Laraia]

Ideally I would now be able to use h₃ to rewrite and achieve the goal I said but there is the difference of the coercion.

[Yakov Pechersky]

Do you understand the difference between a type and a term? Do you understand the difference between fintype and finset? Do you understand the difference between fintype.card and finset.card?

[Yakov Pechersky]

docs#fintype.card_coe

[Yakov Pechersky]

Do you have a lemma that the cardinality of left cosets is the same? Do you know of a lemma that says that the cardinality of a bUnion of disjoint finsets is the sum of their cardinalities?

[Eric Wieser]

The difference is not just the coercion, one is about set.univ while the other is about finset.univ

[Eric Rodriguez]

I mean, do we actually have

example : fintype.card (set.univ : set G) = fintype.card G :=
begin
  exact fintype.of_equiv_card (equiv.set.univ G).symm
end

? this is library_search's best effort

[Eric Wieser]

Note that in the mwe we just used that lemma to introduce the coercion in the first place

[Eric Wieser]

But that's probably a fine simp lemma to add

[Thomas Laraia]

Hello again.

import tactic
import group_theory.coset
import data.set.basic
import group_theory.order_of_element
import data.equiv.basic
import data.fintype.basic
import data.finset.basic

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

open function

@[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)

lemma lagrange (P : partition G) (h: ∀ X, 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
  exact card_subgroup_dvd_card H,
end
--lmao I don't need any of
--`(P : partition G) (h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H )`
--this is very annoying

#check quotient_group.left_rel H
-- `The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.`





lemma lagrange_long [fintype H] {k : ℕ} (P : partition G)
(h: ∀ X, X ∈ P.C → ∃ (g : G), X = left_coset g H) {γ : fin k → G}
{h₂ : ∀ (i j : fin k), left_coset (γ i) H ≠ left_coset (γ j) H}
{h₃ : (⋃(i : fin k), left_coset (γ i) H) = set.univ}:
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₄,
  cases P,
  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,
  rw h₁,
  --rw ← h₃,

  -- I am going to need a lemma here to say the finite union of disjoint sets
  -- has the same size as the sum of the sizes of each set

  -- also, is there a way for me to use the left_cosets to make the partition
  -- instead of saying there is a partition and stating that each block
  -- is equal to some left


  /-have : {R // equivalence R} ≃ partition G,
  exact i_need_this G (left_coset_equiv set.univ),-/



  --have : equivalence (left_coset_equiv set.univ) ≃ partition G,
  --have h₅ : fintype.card (⋃(i : fin k), left_coset (γ i) H) = fintype.card set.univ,

  --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










lemma lagrange_long2 [fintype H] {k : ℕ} (P : setoid G)
(lft_cos_prtn : P = quotient_group.left_rel H){ γ : fin k → G}
{h₂ : ∀ (i j : fin k), left_coset (γ i) H ≠ left_coset (γ j) H}
{h₃ : (⋃(i : fin k), left_coset (γ i) H) = set.univ}:
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,
  unfold quotient_group.left_rel at lft_cos_prtn,
  sorry,
  --rw ← h₃,

  -- I am going to need a lemma here to say the finite union of disjoint sets
  -- has the same size as the sum of the sizes of each set

  -- also, is there a way for me to use the left_cosets to make the partition
  -- instead of saying there is a partition and stating that each block
  -- is equal to some left


  /-have : {R // equivalence R} ≃ partition G,
  exact i_need_this G (left_coset_equiv set.univ),-/



  --have : equivalence (left_coset_equiv set.univ) ≃ partition G,
  --have h₅ : fintype.card (⋃(i : fin k), left_coset (γ i) H) = fintype.card set.univ,

  --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

In lagrange_long, I am pushing forward with saying there is a partition and giving the partition a property, and I've added an extra hypothesis with a coe_sort, but am unable to use rw h₁. Does coe_sort send to different places? I'm rereading Yakov Pechersky's comment a lot to look for a better understanding, and am looking to understand the error I see. Is this just not a road I can travel down?

[Eric Wieser]

Can you show the goal state and error message where rw h₁ fails?

[Ruben Van de Velde]

rewrite tactic failed, motive is not type correct
  λ (_a : has_coe_to_sort.S (set G)),
    k * fintype.card ↥H = fintype.card ↥set.univ = (k * fintype.card ↥H = fintype.card _a)
state:
G : Type,
_inst_1 : fintype G,
_inst_2 : group G,
H : subgroup G,
_inst_3 _inst_4 : fintype ↥H,
k : ℕ,
γ : fin k → G,
h₂ : ∀ (i j : fin k), left_coset (γ i) ↑H ≠ left_coset (γ j) ↑H,
h₃ : (⋃ (i : fin k), left_coset (γ i) ↑H) = set.univ,
h₄ : fintype.card ↥set.univ = fintype.card G,
P_C : set (set G),
P_Hnonempty : ∀ (X : set G), X ∈ P_C → X.nonempty,
P_Hcover : ∀ (a : G), ∃ (X : set G) (H : X ∈ P_C), a ∈ X,
P_Hdisjoint : ∀ (X Y : set G), X ∈ P_C → Y ∈ P_C → (X ∩ Y).nonempty → X = Y,
h :
  ∀ (X : set G),
    X ∈ {C := P_C, Hnonempty := P_Hnonempty, Hcover := P_Hcover, Hdisjoint := P_Hdisjoint}.C →
    (∃ (g : G), X = left_coset g ↑H),
h₁ : ↥set.univ = ↥⋃ (i : fin k), left_coset (γ i) ↑H
⊢ k * fintype.card ↥H = fintype.card ↥set.univ

[Eric Wieser]

It's likely that the two set.univs refer to different types - both (set.univ : set nat) and (set.univ : set unit) will show as the same in the goal view. If you hover over them in the goal view, it will tell you which set.univ is being used.

[Eric Wieser]

Using simp_rw may also solve the problem

[Ruben Van de Velde]

Btw, your assumptions are inconsistent:

  have : false,
  { obtain rfl|this := nat.eq_zero_or_pos k,
    { haveI : is_empty (fin 0) := fin.is_empty,
      have : (⋃ (i : fin 0), left_coset (γ i) ↑H) = ∅,
      { rw set.ext_iff,
        simp only [not_exists, set.mem_empty_eq, set.mem_Union, iff_false],
        intros x i,
        exact fin.is_empty.elim i },
      rw [this] at h₃,
      have : is_empty G,
      { rw [←finset.univ_eq_empty', finset.univ_eq_empty, ←set.univ_eq_empty_iff, h₃], },
      exact this.elim' (1 : G) },
    { simpa using h₂ ⟨0, this⟩ ⟨0, this⟩ } },

[Eric Wieser]

I assume h₂ should have an i ≠ j in it?

[Yakov Pechersky]

Probably better stated as injectivity of the fun i, left_coset (gamma i) H

[Thomas Laraia]

Ah, that's a shame, did originally have {h₁ : injective γ} but removed it in case it was superfluous information, was going to look into readding it once I needed it.
Have also addressed {h₂ : ∀ (i j : fin k), i ≠ j → left_coset (γ i) H ≠ left_coset (γ j) H}, I think that is better.
I will look at
Ruben Van de Velde said:

Btw, your assumptions are inconsistent:

  have : false,
  { obtain rfl|this := nat.eq_zero_or_pos k,
    { haveI : is_empty (fin 0) := fin.is_empty,
      have : (⋃ (i : fin 0), left_coset (γ i) ↑H) = ∅,
      { rw set.ext_iff,
        simp only [not_exists, set.mem_empty_eq, set.mem_Union, iff_false],
        intros x i,
        exact fin.is_empty.elim i },
      rw [this] at h₃,
      have : is_empty G,
      { rw [←finset.univ_eq_empty', finset.univ_eq_empty, ←set.univ_eq_empty_iff, h₃], },
      exact this.elim' (1 : G) },
    { simpa using h₂ ⟨0, this⟩ ⟨0, this⟩ } },

to see if there is another thing that does not work here.

I am considering working backwards from the proof of lagrange's theorem in mathlib and seeing what it is made out of.

Eric Wieser said:

It's likely that the two set.univs refer to different types - both (set.univ : set nat) and (set.univ : set unit) will show as the same in the goal view. If you hover over them in the goal view, it will tell you which set.univ is being used.

I have no idea why, but I do not get any information when I hover in the infoview.

[Thomas Laraia]

Yakov Pechersky said:

Probably better stated as injectivity of the fun i, left_coset (gamma i) H

This function you mean is {γ : fin k → G}, correct?

[Eric Wieser]

No, the function Yakov means is the one they stated,. Yakov is suggestingh₂ : function.injective (λ i, left_coset (γ i) H), which is easier to work with than your corrected h₂ but otherwise equivalent.

[Thomas Laraia]

Ah I understand. Thank you!