2.8. Injections, bijections
Composition, restriction
The composite of any 2 functions f,g such that Im f
⊂ Dom g is defined by
g⚬f = ((Dom f) ∋ x ↦
g(f(x)))
(f : E →
F ∧ g : F → G) ⇒ g⚬f
: E → G
(This notation will be abusively kept if g is a functor, in which case
this is a schema of definitions).
Similarly with more than 2 functions: adding a third one h :
G →H to the above conditions, we define
h⚬g⚬f
= (h⚬g)⚬f = h⚬(g⚬f) = (E
∋ x ↦ h(g(f(x))))
The restriction of a function f to a set A ⊂ Dom f is
f_{A} =
(A ∋ x ↦ f(x)) = f⚬Id_{A}.
Gr(f_{A}) = (Gr f)_{A}
f[A] = Im(f_{A})
∀_{Fnc} f,g, Gr g ⊂ Gr f
⇔ (Dom g ⊂ Dom f ∧ g = f_{Dom g})
When g is a restriction of f, we also say that f is an extension of
g.
Injections, bijections, inverse
A function f is called injective
(or : an injection ), if
^{t}Gr f is a functional graph:
Inj f ⇔ 
(∀x≠x′∈Dom f, f(x) ≠
f(x′)) 
⇔ 
(∀x,x′∈Dom f, f(x) = f(x′)
⇒ x=x′) 
(f : E ↪ F) ⇔ 
(f : E → F ∧ Inj f) 
Im f ⊂ F ⇒ 
(Inj f ⇔ ∀y∈F, !:f_{•}(y)) 
The inverse of any injection f, is the function
f^{ 1} with graph ^{t}Gr f:
f^{ 1} = ℩f_{•}
= (Im f ∋ y ↦ ℩f_{•}(y))
Gr(f^{ 1}) = ^{t}Gr f
(f^{ 1})^{1} = f.
A function f : E → F is said bijective
(or a bijection) from E onto F, if it is both injective and surjective :
f : E ↔ F ⇔ 
(f : E → F ∧ ∀y∈F,
∃!: f_{•}(y)) 
⇔ 
(f : E ↪ F ∧ Im f = F) 
⇔ 
(f : E ↠ F ∧ Inj f) 
⇒ 
f^{ 1}: F ↔ E. 
In particular Id_{E} : E ↔ E.
Diverse properties
Proposition. Let f : E → F
and g : F → G. Then
(Inj f ∧ Inj g) ⇒ Inj(g⚬f)
 Inj(g⚬f) ⇒ Inj f
 Im(g⚬f) = g[Im f] ⊂ Im g.
Proofs:
 ∀x,y∈E,
g(f(x)) = g(f(y)) ⇒
f(x) = f(y) ⇒ x = y.
 ∀x,y ∈ E, f(x) = f(y)
⇒ g(f(x)) = (g(f(y)) ⇒
x = y.
 ∀z∈G, z ∈ Im(g⚬f) ⇔
(∃x∈E, g(f(x))=z) ⇔
(∃y∈ Imf, g(y)=z) ⇔ z
∈ g[Imf]. ∎
From 3. we can obviously deduce
Im(g⚬f) = G ⇒ Im g = G
Im f = F ⇒ Im(g⚬f) = Im g
(f:E ↠ F) ⇒ (g:F
↠ G ⇔ g⚬f:E ↠ G)
Let f : E → F, and a function g with Dom g = F.
Then, easily,
g⚬f
= Id_{E} 
⇔ (∀x∈E, ∀y∈F,
f(x) = y ⇒ g(y) = x)


⇔ Gr f ⊂ ^{t}Gr g
⇔ (∀y∈F, f_{•}(y)⊂{g(y)}) 

⇔ (∀x∈E,
f(x)∈g_{•}(x))
⇔ (Inj f ∧ g_{Im f} = f^{ 1}) 

⇒ (Im f = F ⇔
g = f^{ 1} ⇔ (Inj g ∧ Im g ⊂ E)) 
Proof of the nonobvious step : (g⚬f
= Id_{E} ∧ Inj g ∧ Im g ⊂ E) ⇒
(∀y∈F, g(f(g(y))) =
g(y) ∴ y = f(g(y)) ∈ Im f)
Proposition. (f : E → F ∧ g : F
→ E ∧ g⚬f = Id_{E}) ⇒ (Im f = F ⇔
Inj g ⇔ f⚬g = Id_{F} ⇔ g = f^{ 1}).
Proof : (Inj g
∧ g⚬f⚬g = g⚬Id_{F})
⇒ f⚬g = Id_{F}.
∎
Proposition. 1) If f,g are injective and Im f = Dom g,
then (g⚬f)^{1} = f^{ 1}⚬g^{1}.
2) If f,h : E→F and g : F→E then
(g⚬f = Id_{E} ∧ h⚬g = Id_{F})
⇔ ((g : F ↔ E) ∧ f = h = g^{−1}).
Proofs:
1) ∀x∈Dom f, ∀y∈ Im g, (g⚬f)(x) = y
⇔ f(x) = g^{1}(y) ⇔ x =
(f^{ 1}⚬g^{1})(y).
Other method: (g⚬f)^{1}
= (g⚬f)^{1}⚬g⚬g^{1} =
(g⚬f)^{1}⚬g⚬f⚬f^{ 1}⚬g^{1}
= f^{ 1}⚬g^{1}.
2) We deduce f = h from f = h⚬g⚬f
= h, or from Gr f ⊂ ^{t}Gr g
⊂ Gr h. The rest is obvious.∎
Canonical functions
For any objects x,y we shall say that x
determines y if there is an invariant functor T (known but
kept implicit) such that T(x) = y. Then the role of y as
free variable can be played by the term T(x), thus by
the use of x.
Similarly, a function f : E → F
will be said canonical if it is defined as E ∋ x ↦ T(x)
where T is some invariant functor.
Examples of important canonical injections
:
 E ⊂ F ⇒
Id_{E} : E ↪ F
 (x ↦ {x}) : E ↪ ℘(E)
 Gr : F^{E} ↪ ℘(E×F).
A bijection f will be
said bicanonical if both f and f^{−1}
are canonical.
When a bijection f : E ↔ F
is canonical (resp. bicanonical), we shall write f : E ⥬ F
(resp. f : E ⇌ F); or, with its defining
functor φ as φ : E ⥬ F which means that (E
∋ x ↦ φ(x)) is injective with image F.
We shall write E ⥬ F (resp. E ⇌ F)
to mean the existence of a canonical (resp. bicanonical) bijection,
that is kept implicit. These will often look
like equality properties on numbers, as the existence of a bijection between
finite sets implies the equality of their numbers of elements.
Canonical bijections can fail to be bicanonical especially when their defining functor
is not injective:
V_{2}^{E} ⥬ ℘(E)
E ≠ ∅ ⇒ {x}^{E} ⥬ {x}
E×{x} ⥬ E
E×F ⇌ F×E
E×{x} ⇌ {x}×E
⇌ E^{{x}}
E×{0} ⇌ E.
This metarelation between sets is preserved by
constructions: if E ⥬ E′ and F ⥬
F′ then ℘(E) ⥬ ℘(E'), E×F ⥬
E′×F′ and F^{E}
⥬ F′^{E′} (using the direct image of the graph), and the same for ⇌.
This is how transposition (E×F ⇌ F×E) extends to both
graphs and operations:
℘(E×F) ⇌ ℘(F×E)
G^{E×F} ⇌ G^{F×E}
∀f∈G^{E×F}, ^{t}f
= (F×E∋(x,y) ↦ f(y,x)) ∈
G^{F×E}.
Sums of functions
The binder ∐ of sum of sets
defines canonical bijections (whose inverses, defined by R ↦
R⃗_{I}, depend on I):
(℘(E))^{I} ⥬ ℘(I×E)
∏_{i∈I} ℘(A_{i})
⥬ ℘(∐_{i∈I} A_{i})
Any sum of sets S = ∐_{i∈I} A_{i}
has its family of natural injections j_{i} given by the curried
ordered pair definer :
∀i∈I, j_{i} : A_{i}
↪ S.
The sum over I of functions f_{i}
where ∀i∈I, A_{i} = Dom f_{i} is defined by
∐_{i∈I} f_{i}
= (S ∋ (i,x) ↦ f_{i}(x))
g = ∐_{i∈I }f_{i} ⇔
(Dom g = S ∧ ∀i∈I, f_{i} =
g⚬j_{i} = g⃗(i))
It is the inverse of the currying of binary operations, which we shall denote like for graphs:
for any sets E, F and any operation (function) B with domain E×F ≠ ∅
(from which E and F can be restored as E = Dom Dom B and
F = Im Dom B, while if E×F = ∅ the notation can be abusively
kept while taking E and F from context),
B⃗ = (E ∋ x ↦
(F ∋ y ↦ B(x,y)))
B⃖ = ^{t}B⃗ = (F ∋ y ↦
(E ∋ x ↦ B(x,y))
Hence the canonical bijections (bicanonical if I = Dom S, thus if E ≠ ∅ in the
case I×E)
∀_{Set}F, ∏
i∈I
F^{Ai} ⥬ F^{S}
∀_{Set}E,F,
(F^{E})^{I} ⥬ F^{I×E}
(∀F : S → Set) ∏
i∈I
∏
x∈A_{i}
F_{(i,x)} ⥬ ∏
c∈SF_{c}
(E×F)×G ⇌ E×F×G
f ∈ (F^{E})^{I} ⇒ ∐
i∈I
Gr f_{i} ⊂ ℘(I×(E×F))
⇌ ℘((I×E)×F) ⊃ Gr ∐
i∈I
f_{i}
Product of functions or recurrying
Both curried forms R⃗ and R⃖ of graphs R ⊂
E×F are exchanged by a bijection ℘(F)^{E}
↔ ℘(E)^{F} defined with parameter F.
The similar bijection between both curried forms of operations with a given domain
I×E, is defined by the binder ⊓ of product of functions all with domain
E, and indexed by I :
(∀i∈I, Dom f_{i} =
E) ⇒ ⊓
i∈I
f_{i} = (E ∋ x ↦
(f_{i}(x))_{i∈I})
∀g, g = ⊓
i∈I
f_{i} ⇔ (g : E →
∏
i∈I
Im f_{i} ∧ ∀i∈I, f_{i}
= π_{i}⚬g)
(F : I → Set) ⇒ ⊓ : ∏
i∈I
F_{i}^{E} ⥬ (∏
i∈I
F_{i})^{E}
Set F ⇒ ⊓ : (F^{E})^{I} ⥬
(F^{I})^{E}
These bijections are canonical for nonempty families (I
≠ ∅) as only these determine E, and are usually bicanonical as their inverse uses
I which is definable when E ≠ ∅; anyway we shall abusively keep the
notation ⥬ for the general case while E remains fixed by the context.
A particular case is the binary product (I = V_{2}):
∀_{Fnc}f,g, Dom f = Dom g = E ⇒ f⊓g =
(E ∋ x ↦ (f(x),g(x)))
I^{E}×F^{E} ⇌
(I×F)^{E}
(∐
i∈I
F_{i})^{E} ⇌
∐
ϕ∈I^{E} ∏
x∈E
F_{ϕ(x)}
∀_{Fnc}f, Gr f = Im(Id_{Dom f} ⊓ f)
Other languages:
FR : 2.8. Injections, bijections