Minkowski sum of `Multiset` of `PFilter`

Stream: Is there code for X?

[Martin Dvořák]

Which parts of the following definition already exist?

import Mathlib.Order.PFilter
import Mathlib.Data.Multiset.Basic

variable {M : Type} [OrderedAddCommMonoid M]

private def addMink'' (x y : Set M) : Set M :=
  { a + b | (a ∈ x) (b ∈ y) }

private def addMink' (x y : Order.Ideal M) : Order.Ideal M :=
  let z := addMink'' x.carrier y.carrier
  have hz : Order.IsIdeal z := by
    constructor
    · sorry -- TODO `IsLowerSet`
    · obtain ⟨x₁, hx₁⟩ := x.nonempty
      obtain ⟨y₁, hy₁⟩ := y.nonempty
      exact ⟨x₁ + y₁, x₁, hx₁, y₁, hy₁, rfl⟩
    · sorry -- TODO `DirectedOn`
  hz.toIdeal

def addMink (x y : Order.PFilter M) : Order.PFilter M :=
  ⟨addMink' x.dual y.dual⟩

def Multiset.sumMink (s : Multiset (Order.PFilter M)) : Order.PFilter M :=
  s.foldl addMink sorry sorry -- I want `⟨{0 : M}⟩` for the base case

I would like to define Multiset.sumMink with as little manual work as possible.

[Yaël Dillies]

See file#Data/Set/Pointwise/Basic

[Eric Wieser]

open scoped Pointwise

instance : Add (Order.Ideal M) where
  add x y := {
    carrier := x.carrier + y.carrier
    lower' := sorry
    nonempty' := x.nonempty.add y.nonempty
    directed' := sorry

instance : Zero (Order.Ideal M) where
  zero := {
    carrier := 0
    lower' := sorry
    nonempty' := Set.zero_nonempty
    directed' := directedOn_singleton IsRefl.reflexive _ }

instance : AddCommMonoid (Order.Ideal M) :=
  SetLike.coe_injective.addCommMonoid (·.carrier) _ _ _

is probably a good start

[Eric Wieser]

Every one of those sorries should probably be a standalone lemma, though we might not have them already