## Stream: new members

### Topic: union of subgroups is the group

#### Thomas Laraia (Jul 23 2021 at 09:10):

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 (Jul 23 2021 at 09:11):

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

#### Eric Wieser (Jul 23 2021 at 09:14):

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 (Jul 23 2021 at 09:16):

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 (Jul 23 2021 at 09:20):

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

#### Thomas Laraia (Jul 23 2021 at 09:24):

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 (Jul 23 2021 at 09:25):

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

#### Eric Wieser (Jul 23 2021 at 09:26):

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

#### Eric Wieser (Jul 23 2021 at 09:27):

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

#### Thomas Laraia (Jul 24 2021 at 12:53):

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 (Jul 24 2021 at 12:55):

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 (Jul 24 2021 at 12:59):

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

#### Thomas Laraia (Jul 26 2021 at 11:09):

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 (Jul 26 2021 at 11:28):

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)

#### Thomas Laraia (Jul 26 2021 at 11:35):

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 (Jul 26 2021 at 11:36):

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 (Jul 26 2021 at 11:36):

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

#### Eric Wieser (Jul 26 2021 at 11:39):

My next goal was to ....

Can you state this goal as a have?

#### Thomas Laraia (Jul 26 2021 at 11:41):

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 (Jul 26 2021 at 11:42):

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 (Jul 26 2021 at 12:15):

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 (Jul 26 2021 at 12:17):

docs#fintype.card_coe

#### Yakov Pechersky (Jul 26 2021 at 12:19):

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 (Jul 26 2021 at 13:12):

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

#### Eric Rodriguez (Jul 26 2021 at 13:19):

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 (Jul 26 2021 at 13:27):

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

#### Eric Wieser (Jul 26 2021 at 13:27):

But that's probably a fine simp lemma to add

#### Thomas Laraia (Jul 28 2021 at 11:17):

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 (Jul 28 2021 at 11:18):

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

#### Ruben Van de Velde (Jul 28 2021 at 11:26):

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 (Jul 28 2021 at 11:27):

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 (Jul 28 2021 at 11:28):

Using simp_rw may also solve the problem

#### Ruben Van de Velde (Jul 28 2021 at 12:47):

  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 (Jul 28 2021 at 12:51):

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

#### Yakov Pechersky (Jul 28 2021 at 13:10):

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

#### Thomas Laraia (Jul 28 2021 at 13:32):

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:

  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 (Jul 28 2021 at 13:33):

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 (Jul 28 2021 at 13:37):

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 (Jul 28 2021 at 14:15):

Ah I understand. Thank you!

Last updated: Dec 20 2023 at 11:08 UTC