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_reducible]

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

• Finset.functor = { map := fun {α β : Type ?u.1} (f : α → β) (s : Finset α) => Finset.image f s }

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_reducible]

instance Finset.pure : Pure Finset

Equations

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

@[simp]

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

Applicative functor

@[instance_reducible]

instance Finset.applicative [(P : Prop) → Decidable P] : Applicative Finset

Equations

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

@[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_reducible]

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

Equations

• Finset.instMonad = { toApplicative := Finset.applicative, bind := fun {α β : Type ?u.1} => Finset.sup }

@[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_reducible]

instance Finset.instAlternativeMonad [(P : Prop) → Decidable P] : AlternativeMonad Finset

Equations

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

instance Finset.instLawfulAlternative [(P : Prop) → Decidable P] : LawfulAlternative Finset

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 = pure 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