mathlib3 documentation

data.finset.functor

Functoriality of finset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[protected, instance]
def finset.functor [Π (P : Prop), decidable P] :
functor finset

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

Equations
source
@[protected, instance]
def finset.is_lawful_functor [Π (P : Prop), decidable P] :
is_lawful_functor finset
source
@[simp]
theorem finset.fmap_def {α β : Type u} [Π (P : Prop), decidable P] {s : finset α} (f : α → β) :
f <$> s = finset.image f s

Pure #

source
@[protected, instance]
def finset.has_pure  :
has_pure finset
Equations
source
@[simp]
theorem finset.pure_def {α : Type u_1} :
has_pure.pure = has_singleton.singleton

Applicative functor #

source
@[protected, instance]
def finset.applicative [Π (P : Prop), decidable P] :
applicative finset
Equations
source
@[simp]
theorem finset.seq_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset (α → β)) :
t <*> s = t.sup (λ (f : α → β), finset.image f s)
source
@[simp]
theorem finset.seq_left_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset β) :
s <* t = ite (t = ∅) ∅ s
source
@[simp]
theorem finset.seq_right_def {α β : Type u} [Π (P : Prop), decidable P] (s : finset α) (t : finset β) :
s *> t = ite (s = ∅) ∅ t
source
theorem finset.image₂_def [Π (P : Prop), decidable P] {α β γ : Type u_1} (f : α → β → γ) (s : finset α) (t : finset β) :
finset.image₂ f s t = f <$> s <*> t

finset.image₂ in terms of monadic operations. Note that this can't be taken as the definition because of the lack of universe polymorphism.

source
@[protected, instance]
def finset.is_lawful_applicative [Π (P : Prop), decidable P] :
is_lawful_applicative finset
source
@[protected, instance]
def finset.is_comm_applicative [Π (P : Prop), decidable P] :
is_comm_applicative finset

Monad #

source
@[protected, instance]
def finset.monad [Π (P : Prop), decidable P] :
monad finset
Equations
source
@[simp]
theorem finset.bind_def [Π (P : Prop), decidable P] {α β : Type u_1} :
has_bind.bind = finset.sup
source
@[protected, instance]
def finset.is_lawful_monad [Π (P : Prop), decidable P] :
is_lawful_monad finset

Alternative functor #

source
@[protected, instance]
def finset.alternative [Π (P : Prop), decidable P] :
alternative finset
Equations

Traversable functor #

source
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
source
@[simp]
theorem finset.id_traverse {α : Type u} [decidable_eq α] (s : finset α) :
finset.traverse id.mk s = s
source
@[simp]
theorem finset.map_comp_coe {α β : Type u} (h : α → β) :
functor.map h ∘ multiset.to_finset = multiset.to_finset ∘ functor.map h
source
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