set vs subtype

Stream: new members

[Alex Zhang]

If in an involved example :

import data.fintype.card
variables {I : Type*} [fintype I]
example :

I want to construct objects which are of type set I or are subtypes of I, and then mainly work on the cardinals of those object.
Which is a better defn for these objects? {i : I | p i} or {i : I // p i}?

[Alex Zhang]

Which one would be more convenient?

[Eric Wieser]

If you use {i : I | p i} as a type you're really using ↥{i : I | p i} aka {i : I // i ∈ {j : I | p j}}

[Eric Wieser]

So it's usually better to state lemmas as {i : I // p i} or even just subtype p which means the same thing

[Eric Wieser]

Otherwise you risk ending up with (∈ {j : I | p j}) as a really silly (but thankfully defeq) spelling of p in some places

[Yakov Pechersky]

If you have fintype, then you can use finset.filter. That will be nicer to prove things about the cardinality than juggling set.finite.to_finset.card

[Alex Zhang]

Is there a defined notion of "union" of subtypes?

[Alex Zhang]

Is there a way of declaring things like {i : I | p i} as a finset directly as I is a fintype here? @Yakov Pechersky

[Yakov Pechersky]

(finset.univ.filter p)

[Eric Rodriguez]

there's also ⊕ but that's probably not gonna be nice to use (and is a disjoint union, not a normal one)

[Eric Wieser]

It might help if you can give more context so we can un- #xy this

[Alex Zhang]

I was looking for some general suggestions before going into details. I will post more specific problems when I get.

[Alex Zhang]

Your suggestions have been very helpful for a good start!

[Alex Zhang]

Is there any version of statements that the card of the union of two disjoint finsets or subtype of a fintype is the sum of their separate cardinals?

[Eric Wieser]

docs#fintype.card_sum?

[Eric Wieser]

docs#finset.card_union_eq?

[Eric Wieser]

Note how I just guessed the names based on what the statement would be, which is especially powerful combined with vscode autocomplete

[Alex Zhang]

Could anyone please give some suggestions on proving

import data.fintype.card
import data.matrix.basic

variables {I : Type*} [fintype I]
open fintype matrix
open_locale big_operators

lemma row_dot_product_split (H : matrix I I ℚ) (i₁ i₂ : I) :
dot_product (H i₁) (H i₂) =
∑ j : {j : I // H i₁ j = H i₂ j}, H i₁ j.1 * H i₂ j.1 +
∑ j : {j : I // H i₁ j ≠ H i₂ j}, H i₁ j.1 * H i₂ j.1 :=
begin
  simp [dot_product],
  --rw [← finset.sum_to_finset_eq_subtype] fails,
end

[Alex Zhang]

I don't know why the quoted out tactic fails.

[Eric Wieser]

You might have an easier time if you generalize your problem:

lemma sum_subtype_split {α β} [fintype α] [add_comm_monoid β] (f : α → β) (p : α → Prop) [decidable_pred p] :
  ∑ j, f j =
    ∑ j : {j : α // p j}, f j + ∑ j : {j : α //¬ p j}, f j :=
begin
  sorry
end

lemma dot_product_split {R} [semiring R] (v w : I → R) :
  dot_product v w =
    ∑ j : {j : I // v j = w j}, v j * w j + ∑ j : {j : I // v j ≠ w j}, v j * w j :=
sum_subtype_split _ _

[Yakov Pechersky]

This is just the thing we discussed yesterday:

variables {I : Type*} [fintype I]
open fintype matrix
open_locale big_operators

attribute [to_additive] prod_dite

lemma sum_subtype_split {α β} [fintype α] [add_comm_monoid β] (f : α → β) (p : α → Prop) [decidable_pred p] :
  ∑ j, f j =
    ∑ j : {j : α // p j}, f j + ∑ j : {j : α //¬ p j}, f j :=
by simp [←fintype.sum_dite (λ a _, f a) (λ a _, f a)]

lemma dot_product_split {R} [decidable_eq R] [semiring R] (v w : I → R) :
  dot_product v w =
    ∑ j : {j : I // v j = w j}, v j * w j + ∑ j : {j : I // v j ≠ w j}, v j * w j :=
by { simp [dot_product, ←fintype.sum_dite (λ j _, v j * w j) (λ j _, v j * w j)] }

[Yakov Pechersky]

Are you trying to split the sum onto the support and not support?

[Alex Zhang]

Yakov Pechersky said:

Are you trying to split the sum onto the support and not support?

No, temporarily not.

[Yakov Pechersky]

You can also split the f into an ite

[Alex Zhang]

by using simp only?

[Yakov Pechersky]

import data.fintype.card
import data.matrix.basic

variables {I : Type*} [fintype I]
open fintype matrix
open_locale big_operators

attribute [to_additive] prod_dite

@[to_additive]
lemma prod_filter_univ {R} [comm_monoid R] (p : I → Prop) [decidable_pred p] (f : I → R) :
  ∏ i in finset.filter p finset.univ, f i = ∏ i : subtype p, f i :=
finset.prod_bij (λ a pa, ⟨a, by simpa using pa⟩) (by simp) (by simp) (by simp) (by simp)

lemma dot_product_split {R} [decidable_eq R] [semiring R] (v w : I → R) :
  dot_product v w =
    ∑ j : {j : I // v j = w j}, v j * w j + ∑ j : {j : I // v j ≠ w j}, v j * w j :=
begin
  have : dot_product v w = ∑ i : I, if v i = w i then v i * w i else v i * w i,
  { simp only [dot_product, if_t_t] },
  rw this,
  rw finset.sum_ite,
  rw sum_filter_univ,
  rw sum_filter_univ,
end

[Alex Zhang]

Very cool!

[Eric Wieser]

I think sum_filter_univ is PR-worthy

[Eric Wieser]

Frankly that's the statement I expected docs#finset.sum_subtype to have

[Yakov Pechersky]

finset.prod_subtype is better for rewrites:

@[to_additive]
lemma prod_filter_univ {R} [comm_monoid R] (p : I → Prop) [decidable_pred p] (f : I → R) :
  ∏ i in finset.filter p finset.univ, f i = ∏ i : subtype p, f i :=
begin
  rw ←finset.prod_subtype,
  simp
end

[Thomas Laraia]

Is there already a way to extend this to a union in mathlib?

[Thomas Laraia]

Although I am experimenting with the notation fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H).

[Eric Wieser]

Can you give a #mwe with imports and variables?

[Yakov Pechersky]

Induction on k will be the way here. But you should express it in terms of finset.card instead.

[Thomas Laraia]

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 algebra.big_operators.basic

@[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] (q : G)
variables (H : subgroup G) [fintype H]

open function

open_locale big_operators

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}:
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,
  simp_rw h₁,
  have : fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H),
end

[Thomas Laraia]

Yakov Pechersky said:

Induction on k will be the way here. But you should express it in terms of finset.card instead.

Ah alright I'll work to make that adjustment.

[Eric Wieser]

Either that or rewriting by docs#fintype.card_sigma, and then showing an equivalence between ⋃ i, left_coset (γ i) H and \Sigma i, left_coset (γ i) H

[Eric Wieser]

When we say an mwe, we mean something like:

variables ...

example : fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H) := sorry

i.e. code that doesn't contain any of the context needed to arrive at that goal

[Thomas Laraia]

Aaaah alright I'll redo it for practice sake

[Eric Wieser]

Lean can likely produce one for you if you put extract_goal after your have

[Eric Wieser]

Which is something that is mentioned at #mwe

[Thomas Laraia]

import tactic
import group_theory.coset
import data.fintype.card
import algebra.big_operators.basic

example {G : Type} {k : ℕ}
  [fintype G]
  [group G]
  (H : subgroup G)
  [fintype ↥H]
  {γ : fin k → G}
  {h₂ : injective (λ (i : fin k), left_coset (γ i) ↑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) :
  fintype.card (↥⋃ (i : fin k), left_coset (γ i) ↑H) =
    ∑ (i : fin k), fintype.card ↥(left_coset (γ i) ↑H) :=
begin
  admit,
end

[Thomas Laraia]

Which was through extract_goal vs

import tactic
import group_theory.coset
import data.fintype.card
import algebra.big_operators.basic

variables {G : Type} [fintype G] [group G] (q : G)
variables (H : subgroup G) [fintype H] (k : ℕ) {γ : fin k → G}

open_locale big_operators

example : fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H) := sorry

[Thomas Laraia]

Eric Wieser said:

Either that or rewriting by docs#fintype.card_sigma, and then showing an equivalence between ⋃ i, left_coset (γ i) H and \Sigma i, left_coset (γ i) H

I see what's happening here though. Either way cheers.

[Eric Wieser]

Note that that example is false, it's only true with injective (λ (i : fin k), left_coset (γ i) ↑H)

[Thomas Laraia]

That's hypothesis h2, isn't it? Or have I written something wrong?

[Thomas Laraia]

Aaaah I see in the mwe

[Thomas Laraia]

import tactic
import group_theory.coset
import data.fintype.card
import algebra.big_operators.basic

open function

variables {G : Type} [fintype G] [group G] (q : G)
variables (H : subgroup G) [fintype H] (k : ℕ) {γ : fin k → G}

open_locale big_operators

example {h₂ : injective (λ i, left_coset (γ i) H)} : fintype.card (⋃(i : fin k), left_coset (γ i) H) = ∑ (i : fin k), fintype.card (left_coset (γ i) H) := sorry

Right this makes sense.

[Eric Wieser]

Here's the equiv I'm thinking of:

/-- The union of a family of disjoint sets is isomorphic to the disjoint union -/
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 }

[Thomas Laraia]

I can't for the life of me figure out why my VSC has an issue with sigma.subtype_ext

[Eric Wieser]

Maybe you have a (very) old version of mathlib

[Eric Wieser]

Oh, that exists already as docs#set.Union_eq_sigma_of_disjoint

[Eric Wieser]

And should probably be renamed to say equiv not eq.