Preimages of Iic

Stream: Is there code for X?

[Peter Kosenko]

I have proven a short lemma about preimages of Iic, is there an existing theorem in mathlib, or a nice way to do it using GaloisConnection? I don't understand GaloisConnections well enough to find a suitable statement.

lemma Monotone_map.icc {A : Type*} [Nonempty A] [LinearOrder A]
  {f : A → A} (hmon : StrictMono f) {g : A → A}
  (hrinv : g.RightInverse f) (x : A) :
  f⁻¹' (Iic x) = Iic (g x) := by
  ext y; simp only [mem_preimage, mem_Iic]
  constructor
  · intro h
    by_contra h'; push_neg at h'
    apply hmon at h';
    rw [hrinv x] at h'; grind
  · intro h
    apply (StrictMono.monotone hmon) at h
    exact le_of_le_of_eq h (hrinv x)

[Snir Broshi]

I suspect hmon.orderIsoOfRightInverse f g hrinv might help, not sure which Galois connection you're referring to specifically

[Aaron Liu]

Peter Kosenko said:

or a nice way to do it using GaloisConnection? I don't understand GaloisConnections well enough to find a suitable statement.

This is exactly the defining property of a galois connection:

import Mathlib

open Set
lemma GaloisConnection.preimage_Iic {α β : Type*} [Preorder α] [Preorder β]
    {l : α → β} {u : β → α} (h : GaloisConnection l u) (x : β) :
    l ⁻¹' (Iic x) = Iic (u x) :=
  Set.ext fun y => h y x

[Peter Kosenko]

This looks very nice, thank you!

[Snir Broshi]

Ooh, it does solve the theorem

import Mathlib
open Set
lemma Monotone_map.icc {A : Type*} [LinearOrder A]
    {f : A → A} (hmon : StrictMono f) {g : A → A}
    (hrinv : g.RightInverse f) (x : A) :
    f ⁻¹' (Iic x) = Iic (g x) := by
  let h := hmon.orderIsoOfRightInverse f g hrinv |>.to_galoisConnection
  exact Set.ext fun y => h y x