bijection in nLab

Contents

 Idea

A bijection is an isomorphism in Set.

Since Set is a balanced category, bijections can also be characterized as functions which are both injective (monic) and surjective (epic).

Definition

Given sets AA and BB, a function f:A→Bf:A \to B is a bijection if it comes with an inverse function f −1:B→Af^{-1}:B \to A such that for all elements b∈Bb \in B, f(f −1(b))=bf(f^{-1}(b)) = b and for all elements a∈Aa \in A, if f(a)=bf(a) = b, then a=f −1(b)a = f^{-1}(b)

∀b∈B.(f(f −1(b))=b∧∀a∈A.(f(a)=b⇒a=f −1(b)))\forall b \in B.(f(f^{-1}(b)) = b \wedge \forall a \in A.(f(a) = b \implies a = f^{-1}(b)))

The condition that f(f −1(b))=bf(f^{-1}(b)) = b could also be made more general, by any element a:Aa:A such that a=f −1(b)a = f^{-1}(b). This then becomes

∀a∈A.∀b∈B.((a= Af −1(b))⇒(f(a)= Bb))∧((f(a)= Bb)⇒(a= Af −1(b))\forall a \in A.\forall b \in B.((a =_A f^{-1}(b)) \implies (f(a) =_B b)) \wedge ((f(a) =_B b) \implies (a =_A f^{-1}(b))

This could be simplified down to the statement that f(a)=bf(a) = b if and only if a=f −1(b)a = f^{-1}(b).

∀a∈A.∀b∈B.((f(a)= Bb)⇔(a= Af −1(b))\forall a \in A.\forall b \in B.((f(a) =_B b) \iff (a =_A f^{-1}(b))

This is an adjoint equivalence between two thin univalent groupoids.

Terminology

In older literature, a bijection may be called a one-to-one correspondence, or (as a compromise) bijective correspondence.

See also

• equivalence of types
• one-to-one correspondence