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

instance Finset.functor [(P : Prop) → Decidable P] : Functor Finset

Because Finset.image requires a DecidableEq instance for the target type, we can only construct Functor Finset when working classically.

Equations

• One or more equations did not get rendered due to their size.

instance Finset.lawfulFunctor [(P : Prop) → Decidable P] : LawfulFunctor Finset

@[simp]

theorem Finset.fmap_def {α β : Type u} [(P : Prop) → Decidable P] {s : Finset α} (f : α → β) : f <$> s = image f s

Pure

instance Finset.pure : Pure Finset

Equations

• Finset.pure = { pure := fun {α : Type ?u.6} (x : α) => {x} }

@[simp]

theorem Finset.pure_def {α : Type u_1} : pure = singleton

Applicative functor

instance 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 fun (f : α → β) => image f s

@[simp]

theorem Finset.seqLeft_def {α β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset β) : s <* t = if t = ∅ then ∅ else s

@[simp]

theorem Finset.seqRight_def {α β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset β) : s *> t = if s = ∅ then ∅ else t

theorem Finset.image₂_def [(P : Prop) → Decidable P] {α β γ : Type u} (f : α → β → γ) (s : Finset α) (t : 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.

instance Finset.lawfulApplicative [(P : Prop) → Decidable P] : LawfulApplicative Finset

instance Finset.commApplicative [(P : Prop) → Decidable P] : CommApplicative Finset

Monad

instance Finset.instMonad [(P : Prop) → Decidable P] : Monad Finset

Equations

• Finset.instMonad = Monad.mk

@[simp]

theorem Finset.bind_def [(P : Prop) → Decidable P] {α β : Type u_1} : (fun (x1 : Finset β) (x2 : β → Finset α) => x1 >>= x2) = sup

instance Finset.instLawfulMonad [(P : Prop) → Decidable P] : LawfulMonad Finset

Alternative functor

instance Finset.instAlternative [(P : Prop) → Decidable P] : Alternative Finset

Equations

• Finset.instAlternative = Alternative.mk (fun {α : Type ?u.20} => ∅) fun {α : Type ?u.20} (s : Finset α) (t : Unit → Finset α) => s ∪ t ()

Traversable functor

def Finset.traverse {α β : Type u} {F : Type u → Type u} [Applicative F] [CommApplicative F] [DecidableEq β] (f : α → F β) (s : Finset α) : F (Finset β)

Traverse function for Finset.

Equations

• Finset.traverse f s = Multiset.toFinset <$> Multiset.traverse f s.val

@[simp]

theorem Finset.id_traverse {α : Type u} [DecidableEq α] (s : Finset α) : traverse pure s = s

@[simp]

theorem Finset.map_comp_coe {α β : Type u} (h : α → β) : Functor.map h ∘ Multiset.toFinset = Multiset.toFinset ∘ Functor.map h

@[simp]

theorem Finset.map_comp_coe_apply {α β : Type u} (h : α → β) (s : Multiset α) : image h s.toFinset = (h <$> s).toFinset

theorem Finset.map_traverse {α β γ : Type u} {G : Type u → Type u} [Applicative G] [CommApplicative G] (g : α → G β) (h : β → γ) (s : Finset α) : Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s