galois insertion (co)atoms

Stream: Is there code for X?

[Jireh Loreaux]

I found myself proving something like these lemmas twice recently, so I realized this generalization should exist. Do we have this somewhere that I missed? Of course, there would be versions that apply to coinsertions too.

galois insertion (co)atom lemmas

import order.atoms

section order_top

variables {α β : Type*} [partial_order α] [partial_order β] [order_top α] [order_top β]
variables {l : α → β} {u : β → α} (gi : galois_insertion l u)
include gi

lemma galois_insertion.is_coatom_of_l_top (htop : l ⊤ = ⊤) {b : β} (hb : is_coatom (u b)) :
  is_coatom b :=
let ⟨hb₁, hb₂⟩ := hb in
  ⟨mt (congr_arg u) (gi.gc.u_top.symm ▸ hb₁),
   λ b' hb', htop ▸ gi.l_u_eq b' ▸ congr_arg l (hb₂ _ (gi.strict_mono_u hb'))⟩

lemma galois_insertion.is_coatom_iff [is_coatomic α] (htop : l ⊤ = ⊤)
  (h_coatom : ∀ a, is_coatom a → u (l a) = a) {b : β} : is_coatom b ↔ is_coatom (u b) :=
begin
  refine ⟨λ hb, _, λ hb, gi.is_coatom_of_l_top htop hb⟩,
  have hb_ne : u b ≠ ⊤ := λ h, hb.1 $ htop ▸ gi.l_u_eq b ▸ congr_arg l h,
  obtain ⟨a, ha, hab⟩ := (eq_top_or_exists_le_coatom (u b)).resolve_left hb_ne,
  have : l a = b := (hb.le_iff.mp ((gi.l_u_eq b ▸ gi.gc.monotone_l hab) : b ≤ l a)).resolve_left
    (λ hla, ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)),
  exact this ▸ (h_coatom a ha).symm ▸ ha,
end

end order_top

section order_bot

variables {α β : Type*} [partial_order α] [partial_order β] [order_bot α] [order_bot β]
variables {l : α → β} {u : β → α} (gi : galois_insertion l u)
include gi

lemma galois_insertion.is_atom_of_u_bot (hbot : u ⊥ = ⊥) {b : β} (hb : is_atom (u b)) :
  is_atom b :=
let ⟨hb₁, hb₂⟩ := hb in
  ⟨λ hb, hb₁ $ hbot ▸ congr_arg u hb, λ b' hb',
   gi.gc.l_bot ▸ gi.l_u_eq b' ▸ congr_arg l (hb₂ (u b') (gi.strict_mono_u hb'))⟩

lemma galois_insertion.is_atom_iff [is_atomic α] (hbot : u ⊥ = ⊥)
  (h_atom : ∀ a, is_atom a → u (l a) = a) {b : β} : is_atom b ↔ is_atom (u b) :=
begin
  refine ⟨λ hb, _, λ hb, gi.is_atom_of_u_bot hbot hb⟩,
  have hb_ne : u b ≠ ⊥ := λ h, hb.1 $ gi.gc.l_bot ▸ gi.l_u_eq b ▸ congr_arg l h,
  obtain ⟨a, ha, hab⟩ := (eq_bot_or_exists_atom_le (u b)).resolve_left hb_ne,
  have : l a = b := (hb.le_iff.mp ((gi.l_u_eq b ▸ gi.gc.monotone_l hab) : l a ≤ b)).resolve_left
    (λ hla, ha.1 (hbot ▸ h_atom a ha ▸ congr_arg u hla)),
  exact this ▸ (h_atom a ha).symm ▸ ha,
end

end order_bot

[Jireh Loreaux]

Supposing not, where would be a good place to put them? In order/atoms?