Zulip Chat Archive

Stream: new members

Topic: finset cosets


view this post on Zulip Xavier Xarles (Jul 03 2020 at 14:33):

Hi all!

I just started learning lean (done the natural number game and some other exercices)

I am having troubles in a very easy definition: I would like to define the coset of a finset of a comm_group with respect to an element of that group. Looking at how it is define the (left)coset for sets, it looks easy. But I don't know how to construct the map (λ x, g * x) for finsets. Any suggestions are very well received. I tried diferent approaches but no one seems to work.

def coset {G : Type*}[comm_group G](s : set G)(g : G): set G := (λ x, g * x) '' s
def finset_coset {G : Type*}[comm_group G](s : finset G)(g : G): finset G := ???

Thanks in advance!

view this post on Zulip Kenny Lau (Jul 03 2020 at 14:35):

#backticks

view this post on Zulip Kenny Lau (Jul 03 2020 at 14:36):

you can use finset.image

view this post on Zulip Xavier Xarles (Jul 03 2020 at 14:41):

thanks, but I am not sure how....

view this post on Zulip Mario Carneiro (Jul 03 2020 at 14:41):

finset.image (λ x, g * x) s I think

view this post on Zulip Kenny Lau (Jul 03 2020 at 14:43):

import data.finset.basic

def coset {G : Type*} [comm_group G] (s : set G) (g : G) : set G :=
(λ x, g * x) '' s

def finset_coset {G : Type*} [comm_group G] (s : finset G) (g : G) : finset G :=
finset.map ⟨λ x, g * x, mul_right_injective g s

open_locale classical
noncomputable def finset_coset' {G : Type*} [comm_group G] (s : finset G) (g : G) : finset G :=
finset.image (λ x, g * x) s

view this post on Zulip Xavier Xarles (Jul 03 2020 at 14:47):

I see, thanks, I understand the problem was saying about computability...

view this post on Zulip Kenny Lau (Jul 03 2020 at 15:00):

A wise mathematician once said, "a wise mathematician puts open_locale classical and noncomputable theory on the top of their every file"

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:16):

Somewhat related, so I didn't start a new topic. If one hasfs : finset ℝ in the environment, can this be coerced into fs : set ℝ? Just this usual coercion notation doesn't work here.

view this post on Zulip Patrick Massot (Jul 03 2020 at 15:18):

We probably need more information about your situation here. #mwe if possible.

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:29):

This is along the lines of what I need.

import data.real.basic
import topology.basic
import tactic

open function

namespace w1
def equiv (A : set ) (B : set ) : Prop :=  f : A  B, bijective f
def idr :    := λ x, x
def fin_ne (X : set ) : Prop :=  (n : ), equiv X ( finset.image idr (finset.range (n+1)) ) -- fails

end w1

view this post on Zulip Reid Barton (Jul 03 2020 at 15:32):

read all the error messages!

view this post on Zulip Reid Barton (Jul 03 2020 at 15:32):

or wait, maybe this is an extra mwe-induced error

view this post on Zulip Reid Barton (Jul 03 2020 at 15:33):

I think there actually isn't a coercion

view this post on Zulip Reid Barton (Jul 03 2020 at 15:33):

as crazy as that seems

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:34):

Reid Barton said:

or wait, maybe this is an extra mwe-induced error

Sorry, there's another equiv. I'll edit my mwe.

view this post on Zulip Reid Barton (Jul 03 2020 at 15:35):

ah, there's a has_lift

view this post on Zulip Reid Barton (Jul 03 2020 at 15:35):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finset.20-.3E.20set.20coercion/near/202788552

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:36):

Yes, but it doesn't just work like usual.

view this post on Zulip Reid Barton (Jul 03 2020 at 15:37):

You need the up arrow.

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:37):

I tried that too. Maybe I made a mistake?

view this post on Zulip Dan Stanescu (Jul 03 2020 at 15:38):

Oh wait, I got it to work now. Thank you @Reid Barton

view this post on Zulip Xavier Xarles (Jul 03 2020 at 19:49):

one more think: I have a finitype subgroup of a comm_group G but I want to use it as a finset in G. I tried to make a definition but it didn't work . I am not sure how to build really definitions.

import data.finset.basic
noncomputable theory
open_locale classical

def finset_subgroup {G : Type*} [comm_group G] {s : subgroup G} [h₂: fintype s]: finset G:=
have hfin : fintype (s.carrier), by solve_by_elim,
s.carrier.to_finset

Thanks

view this post on Zulip Alex J. Best (Jul 03 2020 at 20:30):

I think the whole finset-fintype-finite set setup is a bit confusing, but I played around a bit and ended up with

def finset_subgroup {G : Type*} [comm_group G] {s : subgroup G} [h₂: fintype s] : finset G:=
@set.to_finset _ s.carrier h₂

view this post on Zulip Xavier Xarles (Jul 03 2020 at 20:35):

nice. thanks!


Last updated: May 10 2021 at 23:11 UTC