Formalisation of the Bourbaki-Witt Theorem

Stream: new members

[Finn Mortimore]

Hi all,
Long time lurker. I have finally tried my hand at a LEAN project by formalising the Boubaki-Witt Theorem using the proof in Lang's Algebra. Would appreciate any and all feedback on my code (especially on whether/how I could have used CompleteSemilatticeInf to use a minimal admissible set instead of reproving specific instances of more general lemmas). Based on the 1000+ theorems list on the community website, I believe this is the first formalisation of the theorem and would love to contribute it to the library if possible (after of course making any necessary changes!).

import Mathlib.Order.PreOrder.Chain
import Mathlib.Data.Set.Lattice

section

variable {α : Type} [LE α]

@[ext]
structure neChain (α : Type) [LE α] where
  carrier : Set α
  ne : ∃ x, x ∈ carrier
  Chain' : IsChain (· ≤ ·) carrier

instance : SetLike (neChain α) α where
  coe := neChain.carrier
  coe_injective' _ _ := neChain.ext

end

class CCPO (α : Type) [Nonempty α] extends PartialOrder α where
  cSup : neChain α → α
  le_cSup (c : neChain α) (a : α) : a ∈ c.carrier → a ≤ cSup c
  cSup_le (c : neChain α) (a : α) : (∀ b ∈ c.carrier, b ≤ a) → cSup c ≤ a

structure Inflationary (α : Type) [PartialOrder α] where
  toFun : α → α
  inflationary (x : α) : x ≤ toFun x

instance {α : Type} [PartialOrder α] : CoeFun (Inflationary α) (fun _ ↦ α → α) where
  coe := Inflationary.toFun

open CCPO Set

section

variable {α : Type} [Nonempty α] [CCPO α] {a : α} {f : Inflationary α}

-- We change the definition of admissible set to include '∀ x ∈ B, a ≤ x'
structure IsAdmissible (a : α) (f : Inflationary α) (B : Set α) : Prop where
  a_mem : a ∈ B
  image_self_sub : f '' B ⊆ B
  cSup_mem : ∀ (T : neChain α), ↑T ⊆ B → cSup T ∈ B
  a_min : ∀ x ∈ B, a ≤ x

abbrev A (a : α) : Set α := {x | a ≤ x}

lemma AIsAdmissible (a : α) (f : Inflationary α) : IsAdmissible a f (A a) := by
  apply IsAdmissible.mk
  · exact le_refl a
  · rintro _ ⟨_, a_le, rfl⟩
    exact le_trans a_le (f.inflationary _)
  · rintro T T_sub_A
    have ⟨_, mem_T⟩ := T.ne
    apply le_trans (T_sub_A mem_T) (le_cSup _ _ mem_T)
  · exact fun _ h => h

def M (a : α) (f : Inflationary α) : Set α :=
  ⋂₀ {B | IsAdmissible a f B}

lemma mem_M_iff {x : α} (a : α) (f : Inflationary α) :
  x ∈ M a f ↔ ∀ B ∈ {B | IsAdmissible a f B}, x ∈ B := by
    unfold M
    exact mem_sInter

lemma MIsAdmissible (a : α) (f : Inflationary α) : IsAdmissible a f (M a f) where
  a_mem := by
    rw [mem_M_iff]
    exact fun _ h => h.a_mem
  image_self_sub := by
    rintro x ⟨y, y_mem_M, rfl⟩
    rw [mem_M_iff]
    rintro _ IsAdmissible
    exact IsAdmissible.image_self_sub ⟨y, ⟨mem_sInter.1 y_mem_M _ IsAdmissible, rfl⟩⟩
  cSup_mem := by
    intro T T_sub_M
    rw [mem_M_iff]
    intro _ IsAdmissible
    exact IsAdmissible.cSup_mem T (subset_trans T_sub_M (sInter_subset_of_mem IsAdmissible))
  a_min := by
    intro _ x_mem_M
    rw [mem_M_iff a f] at x_mem_M
    exact (x_mem_M (A a) (AIsAdmissible a f))

lemma sub_M_eq_M {B : Set α} (h : IsAdmissible a f B) (h' : B ⊆ M a f) :
  B = M a f :=
    subset_antisymm h' (sInter_subset_of_mem h)

def IsExtremePt (a : α) (f : Inflationary α) (c : α) : Prop :=
  c ∈ M a f ∧ (∀ x ∈ M a f, x < c → f x ≤ c)

def Mc {c : α} (_ : IsExtremePt a f c) : Set α := {x ∈ M a f | x ≤ c ∨ f c ≤ x}

lemma image_mem_M {x : α} (x_mem_M : x ∈ M a f) : f x ∈ M a f := by
  apply (MIsAdmissible a f).image_self_sub
  use x

lemma Mc_eq_M {c : α} (cIsExtremePt : IsExtremePt a f c) : Mc cIsExtremePt = M a f := by
  apply sub_M_eq_M ?_ (sep_subset _ _)
  apply IsAdmissible.mk
  · exact ⟨(MIsAdmissible a f).a_mem, Or.inl ((MIsAdmissible a f).a_min c cIsExtremePt.1)⟩
  · rintro _ ⟨x, ⟨x_mem_M, (x_le_c | fc_le_x)⟩, rfl⟩ <;>
    refine ⟨image_mem_M x_mem_M, ?_⟩
    · rcases le_iff_lt_or_eq.1 x_le_c with (x_lt_c | rfl)
      · left; exact cIsExtremePt.2 x x_mem_M x_lt_c
      · right; exact le_refl _
    · right
      exact le_trans fc_le_x (f.inflationary x)
  · intro T T_sub_Mc
    refine ⟨(MIsAdmissible a f).cSup_mem _ (subset_trans T_sub_Mc (sep_subset _ _)), ?_⟩
    · by_cases c_IsUB_T : ∀ x ∈ T, x ≤ c
      · left; apply cSup_le T c c_IsUB_T
      · push_neg at c_IsUB_T
        rcases c_IsUB_T with ⟨x, x_mem_T, not_x_le_c⟩
        obtain fc_le_x := Or.resolve_left (T_sub_Mc x_mem_T).2 not_x_le_c
        right
        apply le_trans fc_le_x (le_cSup _ _ x_mem_T)
  · exact fun x ⟨x_mem_M, _⟩ => (MIsAdmissible a f).a_min x x_mem_M

lemma E_eq_M : {c | IsExtremePt a f c} = M a f := by
  apply sub_M_eq_M _ (sep_subset _ _)
  apply IsAdmissible.mk
  · refine ⟨(MIsAdmissible a f).a_mem, ?_⟩
    intro x x_mem_M hx
    exfalso
    exact lt_irrefl a (lt_of_le_of_lt ((MIsAdmissible a f).a_min x x_mem_M) hx)
  · rintro _ ⟨c, c_mem_E, rfl⟩
    refine ⟨image_mem_M c_mem_E.1, ?_⟩
    intro x x_mem_M x_lt_fc
    have x_mem_Mc := x_mem_M
    rw [← Mc_eq_M c_mem_E] at x_mem_Mc
    rcases x_mem_Mc with ⟨_, (x_le_c | fc_le_x)⟩
    · rcases le_iff_lt_or_eq.1 x_le_c with (x_lt_c | rfl)
      · exact le_trans (c_mem_E.2 _ x_mem_M x_lt_c) (f.inflationary c)
      · exact le_refl (f x)
    · exfalso
      exact lt_irrefl x (lt_of_lt_of_le x_lt_fc fc_le_x)
  · intro T T_sub_E
    refine ⟨(MIsAdmissible a f).cSup_mem _ (subset_trans T_sub_E (sep_subset _ _)), ?_⟩
    intro x x_mem_M x_lt_cSup
    by_cases h : ∀ c ∈ T, f c ≤ x
    · exfalso
      apply lt_irrefl x (lt_of_lt_of_le x_lt_cSup ?_)
      apply cSup_le
      intro c c_mem_T
      apply le_trans (f.inflationary c) (h c c_mem_T)
    · push_neg at h
      obtain ⟨c, c_mem_T, not_fc_le_x⟩ := h
      have x_mem_Mc := x_mem_M
      rw [← Mc_eq_M (T_sub_E c_mem_T)] at x_mem_Mc
      obtain (x_lt_c | rfl) := le_iff_lt_or_eq.1 (Or.resolve_right x_mem_Mc.2 not_fc_le_x)
      · exact le_trans ((T_sub_E c_mem_T).2 x x_mem_M x_lt_c) (le_cSup _ _ c_mem_T)
      · have b_mem_Mc := (MIsAdmissible a f).cSup_mem _ (subset_trans T_sub_E (sep_subset _ _))
        rw [← Mc_eq_M (T_sub_E c_mem_T)] at b_mem_Mc
        obtain ⟨_, (cSup_le_x | fx_le_cSup)⟩ := b_mem_Mc
        · exfalso
          apply lt_irrefl x (lt_of_lt_of_le x_lt_cSup cSup_le_x)
        · exact fx_le_cSup
  · exact fun x ⟨x_mem_M, _⟩ => (MIsAdmissible a f).a_min x x_mem_M

lemma mem_M_iff_IsExtremePt {c : α} : c ∈ M a f ↔ IsExtremePt a f c := by
  rw [← E_eq_M]
  rfl

lemma MIsChain : IsChain (· ≤ ·) (M a f) := by
  intro x xIsExtremePt y y_mem_Mx _
  rw [mem_M_iff_IsExtremePt] at xIsExtremePt
  rw [← Mc_eq_M xIsExtremePt] at y_mem_Mx
  obtain ⟨_, (y_le_x | fx_le_y)⟩ := y_mem_Mx
  · right; exact y_le_x
  · left; exact le_trans (f.inflationary x) fx_le_y
end

theorem BourbakiWitt {α : Type} [Nonempty α] [CCPO α] (f : Inflationary α) : ∃ x, f x = x := by
  let a : α := Classical.ofNonempty
  let b : α := cSup (neChain.mk (M a f) ⟨a, (MIsAdmissible a f).a_mem⟩ (MIsChain))
  use b
  apply le_antisymm _ (f.inflationary _)
  apply le_cSup _ _
  apply (MIsAdmissible a f).image_self_sub
  use b
  exact ⟨(MIsAdmissible a f).cSup_mem _ (subset_refl _), rfl⟩

[Matt Diamond]

FYI the first import has a capitalization issue... should be import Mathlib.Order.Preorder.Chain

[Matt Diamond]

for neChain.ne you could have also written carrier.Nonempty... using that gives you access to some useful lemmas via dot notation

[Niels Voss]

I think whether the capitalization issue affects you might be OS-dependent, which is why you might not have noticed it. It does need to be fixed before getting it into mathlib though

[Finn Mortimore]

Thank you both — I have implemented those suggestions. What are the next steps I would need to take to get this into mathlib (if there is a place for it)?