/- Clara L"oh 2021 -/
import tactic -- standard proof tactics
open classical -- we want to work in classical logic
/-
# Injective, surjective, bijective maps
-/
/- Injectivitiy -/
def is_injective
(X : Type*)
(Y : Type*)
(f : X → Y)
:= ∀ x : X, ∀ x' : X,
(f x = f x') → (x = x')
/- Surjectivity -/
def is_surjective
(X : Type*)
(Y : Type*)
(f : X → Y)
:= ∀ y : Y,
∃ x : X, f x = y
/- Bijectivity -/
def is_bijective
(X : Type*)
(Y : Type*)
(f : X → Y)
:= (is_injective X Y f) ∧ (is_surjective X Y f)
/- Simple inheritance properties
of injective, surjective, bijective maps-/
lemma bij_inj
(X : Type*)
(Y : Type*)
(f : X → Y)
(f_bijective: is_bijective X Y f)
: is_injective X Y f
:=
-- we extract the correct part of the and-statement
-- in the definition of is_bijective
by {exact and.elim_left f_bijective}
-- alternatively: by {exact f_bijective.1}
lemma bij_surj
(X : Type*)
(Y : Type*)
(f : X → Y)
(f_bijective: is_bijective X Y f)
: is_surjective X Y f
:=
-- we extract the correct part of the and-statement
-- in the definition of is_bijective
by {exact and.elim_right f_bijective}
-- alternatively: by {exact f_bijective.2}
lemma surj_inj_bij
(X : Type*)
(Y : Type*)
(f : X → Y)
(f_surjective: is_surjective X Y f)
(f_injective: is_injective X Y f)
: is_bijective X Y f
:=
-- we construct the and-statement
-- in the definition of is_bijective
-- in the correct order
by {exact and.intro f_injective f_surjective}
/- If a composition is injective,
then the first map is injective -/
lemma inj_comp_injfirst
(X : Type*)
(Y : Type*)
(Z : Type*)
(f : X → Y)
(g : Y → Z)
(gf_injective : is_injective X Z (g ∘ f))
: is_injective X Y f
:=
begin
-- we prove the all-statement (double ∀)
-- in the definition of is_injective
assume x : X,
assume x' : X,
-- we assume the hypothesis of the implication
-- in the definition of is_injective
assume f_xx' : f x = f x',
-- and then show that this implies x = x',
-- using injectivity of g ∘ f
have gf_xx' : (g ∘ f) x = (g ∘ f) x', from
calc (g ∘ f) x = g (f x) : by {simp}
... = g (f x') : by {simp[f_xx']}
... = (g ∘ f) x' : by {simp},
show x = x',
by {apply gf_injective, apply gf_xx'},
end
/- If a composition is surjective,
then the last map is surjective -/
lemma surj_comp_surjsecond
(X : Type*)
(Y : Type*)
(Z : Type*)
(f : X → Y)
(g : Y → Z)
(gf_surjective : is_surjective X Z (g ∘ f))
: is_surjective Y Z g
:=
begin
-- we prove the all-statement
-- in the definition of is_surjective
assume z : Z,
-- we use surjectivity of g ∘ f
have ex_x : ∃ x : X, (g ∘ f) x = z,
by {exact gf_surjective z},
-- we extract such a preimage
rcases ex_x with ⟨ x : X, gf_x_z⟩,
-- and use it to define a g-preimage of z
let y : Y := f x,
-- we construct the existential statement
-- in the definition of is_surjective,
-- by using the example y
use y,
-- it remains to show that y indeed is a g-preimage of z
show g y = z, from
calc g y = g (f x) : by {simp}
... = (g ∘ f) x : by {simp}
... = z : by {exact gf_x_z},
end
/- If the square of a self-map is bijective,
then the self-map is bijective -/
lemma square_bij_bij
(X : Type*)
(f : X → X)
(ff_bijective: is_bijective X X (f ∘ f))
: is_bijective X X f
:=
begin
-- the map f is injective
have f_injective: is_injective X X f, from
begin
-- the composition f ∘ f is bijective, whence injective
have ff_injective,
by {exact bij_inj X X (f ∘ f) ff_bijective},
-- thus, the first map (namely f) is injective
show _,
by {exact inj_comp_injfirst X X X f f ff_injective},
end,
-- the map f is surjective
have f_surjective: is_surjective X X f, from
begin
-- the composition f ∘ f is bijective, wehnce surjective
have ff_surjective,
by {exact bij_surj _ _ (f ∘ f) ff_bijective},
-- thus, the second map (namely f) is surjective
show _,
by {exact surj_comp_surjsecond _ _ _ f f ff_surjective},
end,
-- thus, f is bijective
show is_bijective X X f,
by {exact and.intro f_injective f_surjective},
-- alternatively: by {exact surj_inj_bij X X f f_surjective f_injective}
end
/- Some simple examples -/
/- The map {1,2,3} -> {1,2,3},
1 -> 1, 2 -> 1, 3 -> 2
is neither injective nor surjective -/
inductive A : Type
| A_1
| A_2
| A_3
def f
: A → A
| A.A_1 := A.A_1
| A.A_2 := A.A_1
| A.A_3 := A.A_2
lemma not_inj_f
: ¬ is_injective A A f
:=
begin
-- idea: f A_1 = f A_2, even though A_1 ≠ A_2
let x : A := A.A_1,
let x' : A := A.A_2,
-- x and x' are witnesses for non-injectivity:
have f_xx'_x_neg_x' : f x = f x' ∧ x ≠ x', from
begin
have f_xx' : f x = f x', by {simp[f]},
have x_neg_x' : x ≠ x', by {finish},
show _, by {exact and.intro f_xx' x_neg_x'},
end,
-- we move the negation to the innermost formula,
-- use x and x' as examples for the existential quantifier,
-- and then conclude via f_xx'_x_neg_x'
show _, from
begin
unfold is_injective,
push_neg,
use x,
use x',
exact f_xx'_x_neg_x',
end
end
lemma not_surj_f
: ¬ is_surjective A A f
:=
begin
-- we first move the negation through the all-quantifier
refine not_forall_of_exists_not _,
show ∃ y : A, ¬(∃ x : A, f x = y), by
begin
-- we show that A_3 does not lie in the image
use A.A_3,
have A3_not_in_im : ∀ x : A, ¬ f x = A.A_3, from
begin
assume x : A,
-- we now just consider all three cases
cases x,
case A.A_1 : {simp[f]}, -- alternatively: {finish}
case A.A_2 : {simp[f]},
case A.A_3 : {simp[f]},
end,
show _,
by {simp at *, exact A3_not_in_im}
end
end
/- The map {1,2} -> {1,2},
1 -> 2, 2 -> 1
is bijective -/
inductive B
| B_1
| B_2
def g : B → B
| B.B_1 := B.B_2
| B.B_2 := B.B_1
lemma bij_g
: is_bijective B B g
:=
begin
-- we check injectivity and surjectivity
-- by going through all the cases
have inj_g : is_injective B B g, from
begin
assume x : B,
assume x' : B,
assume g_xx' : g x = g x',
cases x,
case B.B_1 : begin cases x', finish, finish end,
case B.B_2 : begin cases x', finish, finish end,
end,
have surj_g : is_surjective B B g, from
begin
assume y : B,
cases y,
case B.B_1 : begin use B.B_2, finish end,
case B.B_2 : begin use B.B_1, finish end,
end,
show _,
by {exact surj_inj_bij _ _ g surj_g inj_g}
end
/- And (parts of) the same thing,
but with (types from) sets instead of sum types -/
def set_123 : set ℕ
:= {1,2,3}
lemma one_in_123 : 1 ∈ set_123
:= by {fconstructor,linarith}
lemma two_in_123 : 2 ∈ set_123
:= by {apply or.inr, finish}
lemma three_in_123 : 3 ∈ set_123
:= by {apply or.inr, finish}
def map_const1
: set_123 → set_123 --({1,2,3} : set ℕ) → ({1,2,3} : set ℕ)
:= λ ⟨x, _⟩, ⟨1, one_in_123⟩
def f'
: set_123 → set_123
:= λ ⟨x, x_in_123⟩,
if x = 3 then ⟨ 2, two_in_123 ⟩
else ⟨ 1, one_in_123 ⟩
lemma not_inj_f'
: ¬ is_injective set_123 set_123 f'
:=
begin
-- idea: f' 1 = f' 2, even though 1 ≠ 2
let x1 : ↥set_123 := ⟨ 1, one_in_123 ⟩,
let x2 : ↥set_123 := ⟨ 2, two_in_123 ⟩,
-- we move the negation through the first all-quantifier
refine (not_forall.mpr _),
-- we use A_1 as first input
use x1,
-- we move the negation through the second all-quantifier
refine (not_forall.mpr _),
-- we use A_2 as second input
use x2,
-- we use the definition of f'
by {finish},
end