mathlib documentation

data.finset.functor

Functoriality of `finset` #

This file defines the functor structure of finset.

TODO #

Currently, all instances are classical because the functor classes want to run over all types. If instead we could state that a functor is lawful/applicative/traversable... between two given types, then we could provide the instances for types with decidable equality.

Functor #

@[protected, instance]

def finset.functor [Π (P : Prop), decidable P] :

Because finset.image requires a decidable_eq instance for the target type, we can only construct functor finset when working classically.

Equations

finset.functor = {map := λ (α β : Type u_1) (f : α → β) (s : finset α), finset.image f s, map_const := λ (α β : Type u_1), (λ (f : β → α) (s : finset β), finset.image f s) ∘ function.const β}

@[protected, instance]

def finset.is_lawful_functor [Π (P : Prop), decidable P] :

is_lawful_functor finset

@[simp]

theorem finset.fmap_def {α β : Type u} [Π (P : Prop), decidable P] {s : finset α} (f : α → β) :

f <$> s = finset.image f s

Pure #

@[protected, instance]

def finset.has_pure :

has_pure finset

Equations

finset.has_pure = {pure := λ (α : Type u_1) (x : α), {x}}

@[simp]

theorem finset.pure_def {α : Type u_1} :

has_pure.pure = has_singleton.singleton

Applicative functor #

@[protected, instance]

def finset.applicative [Π (P : Prop), decidable P] :

applicative finset

Equations

finset.applicative = applicative.mk

@[simp]

theorem finset.seq_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset (α → β)) :

t <*> s = t.sup (λ (f : α → β), finset.image f s)

@[simp]

theorem finset.seq_left_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset β) :

s <* t = ite (t = ∅) ∅ s

@[simp]

theorem finset.seq_right_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset β) :

s *> t = ite (s = ∅) ∅ t

@[protected, instance]

def finset.is_lawful_applicative [Π (P : Prop), decidable P] :

is_lawful_applicative finset

@[protected, instance]

def finset.is_comm_applicative [Π (P : Prop), decidable P] :

is_comm_applicative finset

Monad #

@[protected, instance]

def finset.monad [Π (P : Prop), decidable P] :

Equations

finset.monad = monad.mk

@[simp]

theorem finset.bind_def [Π (P : Prop), decidable P] {α β : Type u_1} :

has_bind.bind = finset.sup

@[protected, instance]

def finset.is_lawful_monad [Π (P : Prop), decidable P] :

is_lawful_monad finset

Alternative functor #

@[protected, instance]

def finset.alternative [Π (P : Prop), decidable P] :

alternative finset

Equations

finset.alternative = {to_applicative := {to_functor := applicative.to_functor finset.applicative, to_has_pure := applicative.to_has_pure finset.applicative, to_has_seq := applicative.to_has_seq finset.applicative, to_has_seq_left := applicative.to_has_seq_left finset.applicative, to_has_seq_right := applicative.to_has_seq_right finset.applicative}, to_has_orelse := {orelse := λ (α : Type u_1), has_union.union}, failure := λ (α : Type u_1), ∅}

Traversable functor #

def finset.traverse {α β : Type u} {F : Type u → Type u} [applicative F] [is_comm_applicative F] [decidable_eq β] (f : α → F β) (s : finset α) :

F (finset β)

Traverse function for finset.

Equations

finset.traverse f s = multiset.to_finset <$> multiset.traverse f s.val

@[simp]

theorem finset.id_traverse {α : Type u} [decidable_eq α] (s : finset α) :

finset.traverse id.mk s = s

@[simp]

theorem finset.map_comp_coe {α β : Type u} (h : α → β) :

functor.map h ∘ multiset.to_finset = multiset.to_finset ∘ functor.map h

theorem finset.map_traverse {α β γ : Type u} {G : Type u → Type u} [applicative G] [is_comm_applicative G] (g : α → G β) (h : β → γ) (s : finset α) :

functor.map h <$> finset.traverse g s = finset.traverse (functor.map h ∘ g) s