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

Equations

• (_ : LawfulFunctor Finset) = (_ : LawfulFunctor Finset)

@[simp]

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

Pure

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 Finset.applicative [(P : Prop) → Decidable P] : Applicative Finset

Equations

• Finset.applicative = let src := Finset.functor; let src_1 := Finset.pure; Applicative.mk

@[simp]

theorem Finset.seq_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset (α → β)) : (Seq.seq t fun (x : Unit) => s) = Finset.sup t fun (f : α → β) => Finset.image f s

@[simp]

theorem Finset.seqLeft_def {α : Type u} {β : Type u} [(P : Prop) → Decidable P] (s : Finset α) (t : Finset β) : (SeqLeft.seqLeft s fun (x : Unit) => t) = if t = ∅ then ∅ else s

@[simp]

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

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

Equations

• (_ : LawfulApplicative Finset) = (_ : LawfulApplicative Finset)

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

Equations

• (_ : CommApplicative Finset) = (_ : CommApplicative Finset)

Monad

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

Equations

• Finset.instMonadFinset = let src := Finset.applicative; Monad.mk

@[simp]

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

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

Equations

• (_ : LawfulMonad Finset) = (_ : LawfulMonad Finset)

Alternative functor

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

Equations

• Finset.instAlternativeFinset = let src := Finset.applicative; Alternative.mk (fun {α : Type u_1} => ∅) fun {α : Type u_1} (s : Finset α) (t : Unit → Finset α) => s ∪ t ()

Traversable functor

def Finset.traverse {α : Type u} {β : 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 α) : Finset.traverse pure s = s

@[simp]

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

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