Valuations on lattices

A valuation on a lattice is a function v into an additive commutative monoid satisfying the modular law v (a ⊔ b) + v (a ⊓ b) = v a + v b; it is positive when it is strictly monotone. Cardinality of finite sets is the model example (Finset.card), and finitely additive set functions — MeasureTheory.AddContent on a ring of sets, a measure on the measurable sets — are the set-lattice instances. Mathlib states the modular law per instance (Finset.card_union_add_card_inter, Set.ncard_union_add_ncard_inter, MeasureTheory.measure_union_add_inter) with no common structure; this file supplies it, together with Birkhoff's theorem that a lattice carrying a positive valuation is modular. [UPSTREAM] candidate.

Main declarations

• IsLatticeValuation v — the modular law; additive on disjoint pairs once v ⊥ = 0 (IsLatticeValuation.map_sup_of_disjoint).
• IsPositiveValuation v — a strictly monotone valuation.
• IsPositiveValuation.isModularLattice — a lattice with a positive valuation into a cancellative monoid is modular.
• Finset.card is a positive valuation.

References

• [birkhoff-1967], Chapter X

class IsLatticeValuation {α : Type u_1} {M : Type u_2} [Lattice α] [AddCommMonoid M] (v : α → M) : Prop

A lattice valuation: v (a ⊔ b) + v (a ⊓ b) = v a + v b.

• map_sup_add_map_inf (a b : α) : v (a ⊔ b) + v (a ⊓ b) = v a + v b

class IsPositiveValuation {α : Type u_1} {M : Type u_2} [Lattice α] [AddCommMonoid M] [Preorder M] (v : α → M) extends IsLatticeValuation v : Prop

A positive valuation: a strictly monotone lattice valuation.

• map_sup_add_map_inf (a b : α) : v (a ⊔ b) + v (a ⊓ b) = v a + v b
• strictMono : StrictMono v

theorem IsLatticeValuation.map_sup_of_disjoint {α : Type u_1} {M : Type u_2} [Lattice α] [OrderBot α] [AddCommMonoid M] (v : α → M) [IsLatticeValuation v] {a b : α} (h0 : v ⊥ = 0) (h : Disjoint a b) : v (a ⊔ b) = v a + v b

A valuation vanishing at ⊥ is additive on disjoint pairs.

theorem IsPositiveValuation.isModularLattice {α : Type u_1} {M : Type u_2} [Lattice α] [AddCommMonoid M] [Preorder M] [IsRightCancelAdd M] (v : α → M) [IsPositiveValuation v] : IsModularLattice α

A lattice carrying a positive valuation into a cancellative monoid is modular: for x ≤ z, the elements x ⊔ y ⊓ z ≤ (x ⊔ y) ⊓ z have the same join and meet with y, hence the same valuation, hence coincide.

instance instIsPositiveValuationFinsetNatCard {α : Type u_1} [DecidableEq α] : IsPositiveValuation Finset.card