Images, preimages, subsets and their relation to injective and surjective functions.

ss.lean

import set_theory.cardinal
import tactic

open_locale cardinal

variables {X Y : Type} {f : X → Y} {A : set X} {B : set Y}

-- Mostre que `A ⊆ f⁻¹ (f A)`
lemma ex1 : A ⊆ f ⁻¹' (f '' A) :=
begin
  change ∀ a, a ∈ A → a ∈ f ⁻¹' (f '' A),
  intros a ha,
  change f a ∈ f '' A,
  change ∃ x, x ∈ A ∧ f x = f a,
  use a,
  split,
  { exact ha },
  { refl }
end

-- Mostre que, se `f` for injetora, então `A = f⁻¹ (f A)`.
example : function.injective f → A = f ⁻¹' (f '' A) :=
begin
  intro hf,
  change ∀ x y, f x = f y → x = y at hf,
  ext a,
  split,
  { apply set.subset_preimage_image },
  { intro ha,
    change f a ∈ f '' A at ha,
    change ∃ x, x ∈ A ∧ f x = f a at ha,
    rcases ha with ⟨x, hx₁, hx₂⟩,
    have h := hf x a hx₂,
    rw h at hx₁,
    assumption }
end

-- Encontre um exemplo explícito de uma função `f : X → Y` e um subconjunto
-- `A ⊆ X`, tais que `A ⊊ f⁻¹ (f A)`.
--
-- Note: it would have been better to use `set.ssubset`.
notation A ` ⊊ ` B := A ⊆ B ∧ A ≠ B

example {x x' : X} (hx : x ≠ x') (y : Y) :
  ∃ (f : X → Y) (A : set X), A ⊊ f ⁻¹' (f '' A) :=
begin
  let f : X → Y := function.const X y,
  let A : set X := {x},
  use f,
  use A,
  split,
  { apply set.subset_preimage_image },
  { change A = f ⁻¹' (f '' A) → false,
    intro h,
    have : x' ∈ f ⁻¹' (f '' A),
    { change f x' ∈ f '' A,
      change f x' ∈ f '' {x},
      rw set.image_singleton,
      change f x' = f x,
      refl },
    rw ←h at this,
    change x' ∈ {x} at this,
    change x' = x at this,
    change x = x' → false at hx,
    apply hx,
    symmetry,
    assumption }
end

example (hX : #X ≤ 1) :
  ¬ ∃ (f : X → Y) (A : set X), A ⊊ f ⁻¹' (f '' A) :=
begin
  rintros ⟨f, A, h₁, h₂⟩,
  refine h₂ (le_antisymm h₁ _),
  intros x hx,
  suffices : function.injective f,
  { rcases hx with ⟨x', hx'₁, hx'₂⟩,
    rwa this hx'₂ at hx'₁, },
  rw cardinal.le_one_iff_subsingleton at hX,
  intros x₁ x₂ _,
  exact @subsingleton.elim _ hX x₁ x₂
end

example (hX : #Y = 0) :
  ¬ ∃ (f : X → Y) (A : set X), A ⊊ f ⁻¹' (f '' A) :=
begin
  rintros ⟨f, A, h₁, h₂⟩,
  refine h₂ (le_antisymm h₁ _),
  intro x,
  let y := f x,
  exfalso,
  apply cardinal.ne_zero_iff_nonempty.mpr,
  { exact nonempty.intro y },
  { assumption }
end

-- Mostre que `f (f⁻¹ B) ⊆ B`.
example : f '' (f ⁻¹' B) ⊆ B :=
begin
  change ∀ b, b ∈ f '' (f ⁻¹' B) → b ∈ B,
  intros b hb,
  change ∃ x, x ∈ f ⁻¹' B ∧ f x = b at hb,
  change ∃ x, f x ∈ B ∧ f x = b at hb,
  rcases hb with ⟨x, hx₁, hx₂⟩,
  rw hx₂ at hx₁,
  assumption
end

-- Mostre que, se `f` for sobrejetora, então `f⁻¹ (f B) = B`.
example : function.surjective f → f '' (f ⁻¹' B) = B :=
begin
  intro hf,
  change ∀ y, ∃ x, f x = y at hf,
  ext b,
  split,
  { apply set.image_preimage_subset },
  { intro hb,
    change ∃ x, x ∈ f ⁻¹' B ∧ f x = b,
    change ∃ x, f x ∈ B ∧ f x = b,
    specialize hf b,
    cases hf with x hx,
    use x,
    split,
    { rw hx,
      assumption },
    { assumption } }
end

-- Encontre um exemplo explícito de uma função `f : X → Y` e um subconjunto
-- `B ⊆ Y`, tais que `f⁻¹ (f B) ⊊ B`.
example {y y' : Y} (hy : y ≠ y') :
  ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B :=
begin
  let f : X → Y := function.const X y,
  let B : set Y := set.univ,
  use f,
  use B,
  split,
  { apply set.image_preimage_subset },
  { change f '' (f ⁻¹' B) = B → false,
    intro h,
    change f '' (f ⁻¹' set.univ) = B at h,
    change f '' set.univ = B at h,
    rw set.image_univ at h,
    have hX : nonempty X,
    { rw set.ext_iff at h,
      simp only [set.mem_range] at h,
      simp only [set.mem_univ] at h,
      simp only [iff_true] at h,
      specialize h y,
      cases h with x hx,
      exact nonempty.intro x },
    rw @set.range_const _ _ hX at h,
    have : ∀ y', y' ∈ {y},
    { intros y',
      rw h,
      apply set.mem_univ },
    change ∀ y', y' = y at this,
    specialize this y',
    apply hy,
    symmetry,
    assumption },
end

example (hX : ¬ nonempty X) (hY : nonempty Y) :
  ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B :=
begin
  unfreezeI,
  cases hY with y,
  let f : X → Y := function.const X y,
  let B : set Y := {y},
  use f,
  use B,
  split,
  { rintros _ ⟨x, _⟩,
    exfalso,
    apply hX,
    exact nonempty.intro x },
  { suffices : f ⁻¹' B = ∅,
    { intro h,
      rw [this, set.ext_iff] at h,
      specialize h y,
      simpa [B] using h },
    ext x,
    exfalso,
    apply hX,
    exact nonempty.intro x }
end

example (hX : nonempty X) (hY : #Y ≤ 1) :
  ¬ ∃ (f : X → Y) (B : set Y), f '' (f ⁻¹' B) ⊊ B :=
begin
  rintros ⟨f, A, h₁, h₂⟩,
  refine h₂ (le_antisymm h₁ _),
  intros y hy,
  rw cardinal.le_one_iff_subsingleton at hY,
  cases hY with hY,
  unfreezeI,
  cases hX with x,
  use x,
  specialize hY (f x) y,
  simpa [hY]
end