nLab inverse function

Redirected from "coherent inverse functions".

Contents

Definition

In set theory

Given sets AA and BB and a function f:ABf\colon A \to B, the inverse function of ff (if it exists) is the function f 1:BAf^{-1}\colon B \to A such that both composite functions ff 1f \circ f^{-1} and f 1ff^{-1} \circ f are identity functions. Note that ff has an inverse function if and only if ff is a bijection, in which case this inverse function is unique.

Inverse functions are inverse morphisms in the category Set of sets.

More generally, in any concrete category, the inverse of any isomorphism is given by the inverse of the corresponding function between underlying sets.

In type theory

In type theory, there are two different kinds of inverse functions, quasi-inverse functions, various kinds of more or less coherent quasi-inverse functions, and inverse functions.

For more on this see at equivalence in type theory.

 Quasi-inverse functions

Given types AA and BB and a function f:ABf:A \to B, a quasi-inverse function of ff is a function g:BAg:B \to A such that gg is a retraction and a section of ff.

b:B(f(g(b))= Bb)× a:A(a= Ag(f(a)))\prod_{b:B} (f(g(b)) =_B b) \times \prod_{a:A} (a =_A g(f(a)))

Equivalently, there are functions ϵ 0(a,b):(a= Ag(b))(f(a)= Bb)\epsilon_0(a, b):(a =_A g(b)) \to (f(a) =_B b) and η 0(a,b):(f(a)= Bb)(a= Ag(b))\eta_0(a, b):(f(a) =_B b) \to (a =_A g(b)) for all a:Aa:A and b:Bb:B.

a:A b:B((a= Ag(b))(f(a)= Bb))×((f(a)= Bb)(a= Ag(b)))\prod_{a:A} \prod_{b:B} ((a =_A g(b)) \to (f(a) =_B b)) \times ((f(a) =_B b) \to (a =_A g(b)))

A function f:ABf:A \to B might have multiple quasi-inverse functions. The type of quasi-inverses of ff is given by

QuasiInv(f) g:BA b:B(f(g(b))= Bb)× a:A(a= Ag(f(a)))\mathrm{QuasiInv}(f) \coloneqq \sum_{g:B \to A} \prod_{b:B} (f(g(b)) =_B b) \times \prod_{a:A} (a =_A g(f(a)))

nn-quasi inverse functions

There are also variants of quasi-inverse functions where they are the inverse functions for nn-truncated types.

For example, every function g:BAg:B \to A is a (-1)-quasi inverse function, because it is an inverse function for h-propositions AA and BB.

A quasi-inverse function is a 0-quasi inverse function, because it is an inverse function for h-sets AA and BB.

A 1-quasi-inverse function is a quasi-inverse function with functions ϵ 0(a,b):(a= Ag(b))(f(a)= Bb)\epsilon_0(a, b):(a =_A g(b)) \to (f(a) =_B b) and η 0(a,b):(f(a)= Bb)(a= Ag(b))\eta_0(a, b):(f(a) =_B b) \to (a =_A g(b)) for all a:Aa:A and b:Bb:B such that for all c:a= Ag(b)c:a =_A g(b) and d:f(a)= Bbd:f(a) =_B b, there are functions

ϵ 1(a,b,c,d):(ϵ 0(a,b,c)= f(a)= Bbd)(c= a= Ag(b)η 0(a,b,d))\epsilon_1(a, b, c, d):(\epsilon_0(a, b, c) =_{f(a) =_B b} d) \to (c =_{a =_A g(b)} \eta_0(a, b, d))
η 1(a,b,c,d):(c= a= Ag(b)η 0(a,b,d))(ϵ 0(a,b,c)= f(a)= Bbd)\eta_1(a, b, c, d):(c =_{a =_A g(b)} \eta_0(a, b, d)) \to (\epsilon_0(a, b, c) =_{f(a) =_B b} d)

This is an inverse function for h-groupoids AA and BB.

So on and so forth.

Inverse functions

Given types AA and BB and a function f:ABf:A \to B, an inverse function of ff is a function g:BAg:B \to A with a function ϵ(a,b):(f(a)= Bb)(a= Ag(b))\epsilon(a, b):(f(a) =_B b) \to (a =_A g(b)) for all a:Aa:A and b:Bb:B, such that for all identities p:a= Ag(b)p:a =_A g(b), the fiber of ϵ(a,b)\epsilon(a, b) at pp is contractible.

isInv(f,g) a:A b:B ϵ(a,b):(f(a)= Bb)(a= Ag(b)) p:a= Ag(b)isContr(fiber(ϵ(a,b),p))\mathrm{isInv}(f, g) \coloneqq \prod_{a:A} \prod_{b:B} \sum_{\epsilon(a, b):(f(a) =_B b) \to (a =_A g(b))} \prod_{p:a =_A g(b)} \mathrm{isContr}(\mathrm{fiber}(\epsilon(a, b), p))

Coherent inverse functions

Given types AA and BB and a function f:ABf:A \to B, a coherent inverse function of ff is a quasi-inverse function g:BAg:B \to A with homotopies

G: x:Bf(g(x))= BxH: x:Ag(f(x))= AxG:\prod_{x:B} f(g(x)) =_B x \qquad H:\prod_{x:A} g(f(x)) =_A x

which additionally has one of the two homotopies

K: x:Aap B(f,g(f(x)),x,H(x))= g(f(x))= AxG(f(x))L: x:BH(g(x))= f(g(x))= Bxap A(g,f(g(x)),x,G(x))K:\prod_{x:A} \mathrm{ap}_{B}(f, g(f(x)), x, H(x)) =_{g(f(x)) =_A x} G(f(x)) \qquad L:\prod_{x:B} H(g(x)) =_{f(g(x)) =_B x} \mathrm{ap}_{A}(g, f(g(x)), x, G(x))

The type of coherent inverse functions of ff is given by one of the following types

CohInv 1(f) g:BA G: x:Bf(g(x))= Bx H: x:Ag(f(x))= Ax( x:Aap B(f,g(f(x)),x,H(x))= g(f(x))= AxG(f(x)))\mathrm{CohInv}_1(f) \coloneqq \sum_{g:B \to A} \sum_{G:\prod_{x:B} f(g(x)) =_B x} \sum_{H:\prod_{x:A} g(f(x)) =_A x} \left(\prod_{x:A} \mathrm{ap}_{B}(f, g(f(x)), x, H(x)) =_{g(f(x)) =_A x} G(f(x))\right)
CohInv 2(f) g:BA G: x:Bf(g(x))= Bx H: x:Ag(f(x))= Ax( x:BH(g(x))= f(g(x))= Bxap A(g,f(g(x)),x,G(x)))\mathrm{CohInv}_2(f) \coloneqq \sum_{g:B \to A} \sum_{G:\prod_{x:B} f(g(x)) =_B x} \sum_{H:\prod_{x:A} g(f(x)) =_A x} \left(\prod_{x:B} H(g(x)) =_{f(g(x)) =_B x} \mathrm{ap}_{A}(g, f(g(x)), x, G(x))\right)

ff is called a half adjoint equivalence if it has a coherent inverse function.

Properties

Given functions f:ABf:A \to B and g:BAg:B \to A and homotopies G: x:Bf(g(x))= BxG:\prod_{x:B} f(g(x)) =_B x and H: x:Ag(f(x))= AxH:\prod_{x:A} g(f(x)) =_A x, there are elements

QInvToCohInv 1(f,g,G,H): x:Aap B(f,g(f(x)),x,H(x))= g(f(x))= AxG(f(x))\mathrm{QInvToCohInv}_1(f, g, G, H):\prod_{x:A} \mathrm{ap}_{B}(f, g(f(x)), x, H(x)) =_{g(f(x)) =_A x} G(f(x))
QInvToCohInv 2(f,g,G,H): x:BH(g(x))= f(g(x))= Bxap A(g,f(g(x)),x,G(x))\mathrm{QInvToCohInv}_2(f, g, G, H):\prod_{x:B} H(g(x)) =_{f(g(x)) =_B x} \mathrm{ap}_{A}(g, f(g(x)), x, G(x))

which satisfies the commutative squares for all elements a:Aa:A and b:Bb:B

f(g(f(g(b)))) =G(f(g(b)) f(g(b)) ap B(f,g(f(b)),b,H(b)) = f(g(f(g(b))))= Bb QInvToCohInv 2(f,g,G,H)(b) f(g(b)) =G(b) b \array{& f(g(f(g(b)))) & \overset{G(f(g(b))}= & f(g(b)) & \\ \mathrm{ap}_{B}(f, g(f(b)), b, H(b)) & \Vert & =_{f(g(f(g(b)))) =_B b} & \Vert & \mathrm{QInvToCohInv}_2(f, g, G, H)(b) \\ & f(g(b)) & \underset{G(b)}= & b & \\ }
g(f(g(f(a)))) =H(g(f(a)) g(f(a)) ap A(g,f(g(a)),a,G(a)) = g(f(g(f(a))))= Aa QInvToCohInv 1(f,g,G,H)(a) g(f(a)) =H(a) a \array{& g(f(g(f(a)))) & \overset{H(g(f(a))}= & g(f(a)) & \\ \mathrm{ap}_{A}(g, f(g(a)), a, G(a)) & \Vert & =_{g(f(g(f(a)))) =_A a} & \Vert & \mathrm{QInvToCohInv}_1(f, g, G, H)(a) \\ & g(f(a)) & \underset{H(a)}= & a & \\ }

Thus, there are functions

λg:BA.λG: x:Bf(g(x))= Bx.λH: x:Ag(f(x))= Ax.QInvToCohInv 1(f,g,G,H):QInv(f)CohInv 1(f)\lambda g:B \to A.\lambda G:\prod_{x:B} f(g(x)) =_B x.\lambda H:\prod_{x:A} g(f(x)) =_A x.\mathrm{QInvToCohInv}_1(f, g, G, H):\mathrm{QInv}(f) \to \mathrm{CohInv}_1(f)

and

λg:BA.λG: x:Bf(g(x))= Bx.λH: x:Ag(f(x))= Ax.QInvToCohInv 2(f,g,G,H):QInv(f)CohInv 2(f)\lambda g:B \to A.\lambda G:\prod_{x:B} f(g(x)) =_B x.\lambda H:\prod_{x:A} g(f(x)) =_A x.\mathrm{QInvToCohInv}_2(f, g, G, H):\mathrm{QInv}(f) \to \mathrm{CohInv}_2(f)

Every coherent inverse function is a quasi-inverse function by forgetting the additional coherence condition.

Theorem

If a function f:ABf:A \to B has a coherent inverse function, then for all elements b:Bb:B the fiber of ff at bb is contractible.

Proof

Not really related

 References

Last revised on December 31, 2023 at 21:10:41. See the history of this page for a list of all contributions to it.