nLab weakly constant function

Redirected from "steady function".
Weakly constant function

Weakly constant function

Idea

By a weakly constant function one means a function which is equipped with a certain sort of “witness of constancy”.

However, in higher category theory and homotopy theory, it is debatable whether or not this witness really exhibits “constancy”, hence the use of a different word. (The term “steady function” was suggested by Andrej Bauer but did not catch on.)

Definition

In homotopy type theory, a function

f:AB f\colon A\to B

is weakly constant if we have a term of type of the dependent product over the identification types of all the values of ff on all pairs of arguments:

(x,y:A)(fx=fy). \prod_{(x,y:A)} (f x = f y) \,.

By regarding homotopy type theory as the internal logic of an (∞,1)-topos, we obtain a definition that makes sense in any \infty -category with binary products: a morphism f:ABf:A\to B is weakly constant if the two composites A×AAfBA\times A \rightrightarrows A \xrightarrow{f} B are equivalent.

Relationship to constancy

If ff is constant in the sense that it factors through the terminal object (i.e. we have f=λx.bf = \lambda x. b for some b:Bb:B), then ff is obviously weakly constant. The converse holds if we know that the domain AA is inhabited, for if a 0:Aa_0:A, then fa=fa 0f a = f a_0 for all a:Aa:A. However, the identity function of the empty type is weakly constant, yet not equal to λx.b\lambda x.b for any b:b:\varnothing (since no such bb exists).

More generally, if ff factors through the propositional truncation A{\|A\|}, then it is weakly constant, since any two elements of A{\|A\|} are equal (i.e. it is an h-proposition). In fact, this is true if ff factors through any h-proposition (in which case it in fact also factors through A{\|A\|}, by the universal property of the latter).

The converse to this last implication does hold for some specific f:ABf:A\to B, such as:

  • If BB is an h-set. For then ff factors through the 0-truncation A 0{\|A\|_0}, and the set-coequalizer of the two projections A 0×A 0A 0{\|A\|_0} \times {\|A\|_0} \to {\|A\|_0} is the propositional truncation.

  • If AA has split support. For then we have a composite AAfB{\|A\|} \to A \xrightarrow{f} B, whose restriction to AA is equal to ff by weak constancy.

  • If A=P+QA=P+Q, with PP and QQ h-propositions. For then A{\|A\|} is the join P*QP*Q of PP and QQ, i.e. the pushout of the two projections PP×QQP \leftarrow P\times Q \to Q. The universal property of this pushout says exactly that any weakly constant map P+QBP+Q\to B factors through P*Q=P+QP*Q = \Vert P+Q\Vert.

  • If A=BA=B (see below).

However, it can fail in general, even when AA is merely inhabited (i.e. A=1{\|A\|}= 1). For instance, let A=P+Q+RA=P+Q+R for h-propositions PP, QQ, and RR, and let BB be the triple pushout of PP, QQ, and RR under P×QP\times Q, P×RP\times R, and Q×RQ\times R. Then there is a steady map f:ABf:A\to B, but there exist models in which A=1{\|A\|} = 1 but BB has no global element. The most straightforward such model is presheaves on the poset of proper subsets of {a,b,c}\{a,b,c\}, with P={a,b}P=\{a,b\}, Q={b,c}Q=\{b,c\}, and R={a,c}R=\{a,c\}. In this model, we have B(S)=1B(S) = 1 for all nonempty proper subsets SS, while B()=S 1B(\emptyset) = S^1, and BB has no global sections.

See this discussion.

In general, being weakly constant may be regarded as an “incoherent approximation” to constancy in the sense of factoring through an h-proposition. Indeed for a set AA, its propositional truncation is the set-coequalizer of A×AAA\times A\rightrightarrows A. However, in general such a construction requires the realization of a whole simplicial diagram (the simplicial kernel of the map A1A\to 1).

Weakly constant endomaps

While an arbitrary weakly constant function is not very coherent, a weakly constant endofunction f:AAf:A\to A has some extra degree of “coherence”, as witnessed by the following results of (KECA).

Lemma

If f:AAf:A\to A is weakly constant, then the type Fix(f) x:A(fx=x)Fix(f) \coloneqq \sum_{x:A} (f x = x) is an h-proposition, and equivalent to A{\|A\|}.

Proof

Suppose H: (x,y:A)(fx=fy)H: \prod_{(x,y:A)} (f x = f y), and let (a,p),(b,q):Fix(f)(a,p),(b,q):Fix(f); we want to show (a,p)=(b,q)(a,p)=(b,q). Let r:a=br:a=b be the concatenated path

ap 1faH a,a 1faH a,bfbqb. a \xrightarrow{p^{-1}} f a \xrightarrow{H_{a,a}^{-1}} f a \xrightarrow{H_{a,b}} f b \xrightarrow{q} b.

It will suffice to show that pr=ap f(r)qp \bullet r = ap_f(r) \bullet q, where ap fap_f denotes the action of ff on paths. However, the dependent action of HH on paths implies that H x,yap f(s)=H x,yH_{x,y} \bullet ap_f(s) = H_{x,y'} for any x:Ax:A and any s:y=ys:y=y', and in particular ap f(r)=H a,a 1H a,bap_f(r) = H_{a,a}^{-1} \bullet H_{a,b}. From this pr=ap f(r)qp \bullet r = ap_f(r) \bullet q is immediate. Thus, Fix(f)Fix(f) is an h-proposition.

Now we have a map g:AFix(f)g:A\to Fix(f) defined by g(x)(fx,H fx,x)g(x) \coloneqq (f x, H_{f x,x}), so by the universal property of A{\|A\|}, we have AFix(f){\|A\|} \to Fix(f). On the other hand, we have the first projection pr 1:Fix(f)Apr_1:Fix(f) \to A, and hence Fix(f)AFix(f) \to {\|A\|}. Thus, these two h-propositions are equal.

Theorem

A type AA has split support if and only if it admits a weakly constant endomap f:AAf:A\to A.

Proof

Given AA{\|A\|} \to A, the composite AAAA\to {\|A\|} \to \A is weakly constant. Conversely, if ff is steady, Fix(f)=AFix(f) = {\|A\|} by the lemma, so pr 1:Fix(f)Apr_1:Fix(f) \to A splits the support of AA.

Note that pr 1g=fpr_1 \circ g = f, so that if we start with a weakly constant endomap of AA, deduce a splitting of the support of AA, and then reconstruct a weakly constant endomap, we obtain the same map. However, the proof of steadiness is generally different from the one we began with, so this “logical equivalence” is not an equivalence of types.

Corollary

A type AA is an h-set if and only if every identity type x= Ayx=_A y admits a weakly constant endomap.

Proof

We know that AA is an h-set just when all x= Ayx=_A y have split support.

References

Last revised on December 9, 2023 at 02:56:47. See the history of this page for a list of all contributions to it.