A new exercice for Mathematics in lean

Stream: new members

[Nicolas Rolland]

This could be some additional exercice for mathematics in lean, for the S02_Functions.lean

-- universel
def pull_image  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set β  :=
  { y : β | f ⁻¹' {y} ⊆ s }

example :   f ⁻¹' v ⊆ s ↔  v ⊆ pull_image f s   := by
  sorry

around the exercice

example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
  sorry

[Nicolas Rolland]

and here is a solution, in my own beginner style ..

import Mathlib.Tactic

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)

open Function
open Set


-- The subset hyperdoctrine
-- If a type α is seen as a set, an element of Set α is a subset of the set α.
-- That set of subsets has to be endowed with its categorical structure of (sub)set inclusion, and a proper functor be written etc ... to be a 'hyperdoctrine'

-- push_image ⊣ preimage ⊣ pull_image

-- `preimage` defined in library looks like this
def mypreimage {α : Type u} {β : Type v} (f : α → β) : Set β -> Set α := fun s ↦ { x | f x ∈ s }

--existentiel
def push_image {α : Type u_1} {β : Type u_2} (f : α → β) : Set α -> Set β  := fun s ↦ {f a | a ∈ s}

-- push_image ⊣ pre
example : push_image f s ⊆ v ↔ s ⊆ preimage f v := by
  constructor
  {. intro h
     exact fun x (xs : x ∈ s) ↦ xs |> mem_image_of_mem f |> h
  }
  show s ⊆ f ⁻¹' v → f '' s ⊆ v
  intro h
  rintro y ⟨x, xs, rfl⟩ -- y ∈ f '' s <=> ∃ x, x ∈ s ^ y = f x
  exact h xs


-- universel
def pull_image  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Set β  :=
  { y : β | preimage f {y} ⊆ s }

-- pre ⊣ pull_image
example :  preimage f v ⊆ s ↔  v ⊆ pull_image f s   := by
 constructor
 { exact fun (h: f ⁻¹' v ⊆ s) ↦ by
      intro x (xv: x ∈ v)
      intro u (fux: u ∈ f ⁻¹' {x})
      have xsingletoninv : {x} ⊆ v := singleton_subset_iff.mpr xv
      exact fux |> preimage_mono xsingletoninv |> h }
 exact fun (h : v ⊆ pull_image f s ) ↦ by
  intro x (fxv: x ∈ f ⁻¹' v)
  have hx : x ∈ f ⁻¹' (pull_image f s) := preimage_mono h fxv
  have : f ⁻¹' (pull_image f s) ⊆ s := by
      intro x (hx : preimage f {f x} ⊆ s)
      have : x ∈ preimage f {f x} :=  f x |> mem_singleton
      exact hx (this)
  exact this hx

[Junyan Xu]

This is docs#Set.subset_kernImage_iff

[Nicolas Rolland]

thank you for the ref !

It has a much shorter proof, worth its salt

/-- `kernImage f s` is the set of `y` such that `f ⁻¹ y ⊆ s`. -/
def kernImage (f : α → β) (s : Set α) : Set β :=
  { y | ∀ ⦃x⦄, f x = y → x ∈ s }

protected theorem preimage_kernImage : GaloisConnection (preimage f) (kernImage f) := fun a _ =>
  ⟨fun h _ hx y hy =>
    have : f y ∈ a := hy.symm ▸ hx
    h this,
    fun h x (hx : f x ∈ a) => h hx rfl⟩

[Anatole Dedecker]

I don’t understand, shorter than what? Indeed we also have the galois connection lemma as docs#Set.preimage_kernImage

[Anatole Dedecker]

But indeed we could add some exercises about Galois connections, that’s always fun to formalize