finset cosets

Stream: new members

[Xavier Xarles]

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!

[Kenny Lau]

#backticks

[Kenny Lau]

you can use finset.image

[Xavier Xarles]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Xavier Xarles]

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

[Kenny Lau]

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

[Dan Stanescu]

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.

[Patrick Massot]

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

[Dan Stanescu]

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

[Reid Barton]

read all the error messages!

[Reid Barton]

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

[Reid Barton]

I think there actually isn't a coercion

[Reid Barton]

as crazy as that seems

[Dan Stanescu]

Reid Barton said:

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

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

[Reid Barton]

ah, there's a has_lift

[Reid Barton]

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

[Dan Stanescu]

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

[Reid Barton]

You need the up arrow.

[Dan Stanescu]

I tried that too. Maybe I made a mistake?

[Dan Stanescu]

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

[Xavier Xarles]

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

[Alex J. Best]

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₂

[Xavier Xarles]

nice. thanks!