Order theory of `Fintype`s

Stream: new members

[Thomas Waring]

I have proved some elementary results for the order theory of Fintypes — I would appreciate advice as to whether it would be suitable for Mathlib, & if so where it should go. Let me know if this should be in a different channel, or should be a draft / feedback_wanted PR. The results are (using the API from Mathlib.Data.Finset.Lattice.Fold)

• A nonempty Fintype SemilatticeSup has an order top
• A nonempty Fintype SemilatticeInf has an order bottom
• A nonempty Fintype DistribLattice with a decidable order relation is a Heyting algebra

For my purposes these were conveniences for defining a small Heyting algebra, but they seem elementary & general enough that they might be more widely useful — let me know :-)

For reference, the full code is

import Mathlib.Order.Heyting.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Finset.Lattice.Fold

instance instFintypeOrderTop (α : Type _) [Fintype α] [SemilatticeSup α] [Nonempty α] :
    OrderTop α where
  top := Finset.sup' Finset.univ Finset.univ_nonempty id
  le_top a := Finset.le_sup' id (Finset.mem_univ a)

instance instFintypeOrderBot (α : Type _) [Fintype α] [SemilatticeInf α] [Nonempty α] :
    OrderBot α where
  bot := Finset.inf' Finset.univ Finset.univ_nonempty id
  bot_le a := Finset.inf'_le id (Finset.mem_univ a)

instance instFintypeHImp (α : Type _) [Fintype α] [Lattice α] [Nonempty α]
  [DecidableRel (· ≤ · : α → α → Prop)] : HImp α where
  himp a b := by
    let himpSet : Set α := {c | c ⊓ a ≤ b}
    have : Fintype ↑himpSet := setFintype himpSet
    exact himpSet.toFinset.sup id

instance instFintypeHeyting (α : Type _) [Fintype α] [DistribLattice α] [Nonempty α]
  [DecidableRel (· ≤ · : α → α → Prop)] : HeytingAlgebra α where
  le_himp_iff a b c := by
    simp_rw [instFintypeHImp, Set.toFinset_setOf]
    constructor <;> intro h
    · suffices himp b c ⊓ b ≤ c by
        trans himp b c ⊓ b
        · refine inf_le_inf_right b ?_
          simpa [instFintypeHImp]
        · assumption
      simp [instFintypeHImp, Finset.sup_inf_distrib_right]
    · apply Finset.le_sup (f := id); simpa
  compl a := himp a Bot.bot
  himp_bot _ := rfl

[Yaël Dillies]

Hey! How does this interact with file#Data/Fintype/Order ?