Definitions for Cohomology of Local Cochains

QAlgorithms.Papers.Independent.Intakethird100.P07.BasedLoops

For any group $G$ equipped with a topology, this defines the type of based loops to consist of continuous paths $\gamma:[0,1]\to G$ satisfying both $\gamma(0)=1$ and $\gamma(1)=1$.

QAlgorithms.Papers.Independent.Intakethird100.P07.BasedPaths

For any type $G$ equipped with a topology and a group structure, $\mathrm{BasedPaths}(G)$ is the type of continuous functions $\gamma:[0,1]\to G$ satisfying $\gamma(0)=1_G$, where the interval has its usual subspace topology and $1_G$ is the group identity. There is no restriction on $\gamma(1)$, and continuity of the group operations is not assumed.

QAlgorithms.Papers.Independent.Intakethird100.P07.IsAddLoopContraction

For any type $V$ equipped with a topology and an additive group structure, and any function $\phi:V\times[0,1]\to V$, the predicate $\mathrm{IsAddLoopContraction}(\phi)$ means that $\phi$ is continuous for the product topology, that $\phi(x,0)=0_V$ and $\phi(x,1)=x$ for every $x\in V$, and that $\phi(x+y,t)=\phi(x,t)+\phi(y,t)$ for every $t\in[0,1]$ and every $x,y\in V$. Here $0_V$ is the additive identity, and $[0,1]$ has its topology inherited from $\mathbb R$. Neither commutativity nor compatibility between the topology and the additive group operations is assumed separately.

QAlgorithms.Papers.Independent.Intakethird100.P07.IsKAddLoopContraction

For any type $V$ in universe $u$, equipped with a topology and an additive group structure, and any function $\phi:V\times[0,1]\to V$, this defines the proposition that $\phi$ is continuous when its domain has the compactly generated refinement of the usual product topology, and that

$$\phi(x,0)=0,\qquad \phi(x,1)=x,\qquad \phi(x+y,t)=\phi(x,t)+\phi(y,t)$$

for every $x,y\in V$ and every real $t\in[0,1]$, including both endpoints. The domain refinement declares a subset open exactly when its inverse image is open under every continuous map from a compact Hausdorff space in universe $u$ into the original product $V\times[0,1]$. The topology on $V$ is unchanged, and no compatibility between its topology and group operations is assumed separately in this definition.

QAlgorithms.Papers.Independent.Intakethird100.P07.IsKOmega

For a topological space $X$ whose underlying type lies in universe $u$, the property $\mathrm{IsKOmega}(X)$ means that there exist an at most countable index type $I$ in universe $u$, compact Hausdorff spaces $K_i$ in universe $u$ for every $i\in I$, and continuous maps $f_i:K_i\to X$, such that every $x\in X$ equals $f_i(y)$ for some $i\in I$ and $y\in K_i$, and, for every subset $A\subseteq X$, $A$ is open if and only if $f_i^{-1}(A)$ is open in $K_i$ for every $i\in I$. The index type and the spaces $K_i$ may be empty; an empty index type satisfies these conditions exactly when $X$ is empty.

QAlgorithms.Papers.Independent.Intakethird100.P07.IsLoopContraction

For any type $G$ equipped with a topology and a group structure, and any function $\phi:G\times[0,1]\to G$, the predicate $\mathrm{IsLoopContraction}(\phi)$ means that $\phi$ is continuous for the product topology, that $\phi(g,0)=1_G$ and $\phi(g,1)=g$ for every $g\in G$, and that $\phi(gh,t)=\phi(g,t)\phi(h,t)$ for every $t\in[0,1]$ and every $g,h\in G$. Here $1_G$ is the group identity, and the interval has its topology inherited from $\mathbb R$. No compatibility between the given topology and the group operations is assumed separately.

QAlgorithms.Papers.Independent.Intakethird100.P07.KSpace

For every type $X$ in universe $u$, this defines $K(X)$ to be the same underlying type $X$. This declaration has no topology assumption and itself specifies no topology.

QAlgorithms.Papers.Independent.Intakethird100.P07.LoopContractible

For any type $G$ equipped with a topology and a group structure, $\mathrm{LoopContractible}(G)$ means that there exists a continuous function $\phi:G\times[0,1]\to G$, with the product topology on its domain and the usual subspace topology on $[0,1]$, such that $\phi(g,0)=1_G$ and $\phi(g,1)=g$ for every $g\in G$, and $\phi(gh,t)=\phi(g,t)\phi(h,t)$ for every $t\in[0,1]$ and every $g,h\in G$. Here $1_G$ is the group identity; continuity of the group operations is not a separate assumption.

QAlgorithms.Papers.Independent.Intakethird100.P07.UnitTime

$\mathrm{UnitTime}$ denotes the closed real interval $[0,1]=\{t\in\mathbb R\mid 0\le t\le1\}$, including both endpoints.

QAlgorithms.Papers.Independent.Intakethird100.P07.basedLoopsTopology

For any group $G$ equipped with a topology, this equips the set of continuous paths $\gamma:[0,1]\to G$ satisfying $\gamma(0)=\gamma(1)=1$ with the subspace topology inherited from the space of continuous paths satisfying $\gamma(0)=1$; that latter space itself has the subspace topology inherited from the compact-open topology on all continuous maps $[0,1]\to G$.

QAlgorithms.Papers.Independent.Intakethird100.P07.basedPathEndpoint

For any group $G$ equipped with a topology and any continuous path $\gamma:[0,1]\to G$ satisfying $\gamma(0)=1$, this defines the endpoint of $\gamma$ to be the element $\gamma(1)\in G$.

QAlgorithms.Papers.Independent.Intakethird100.P07.basedPathMul

For any type $G$ equipped with a topology and a group structure whose multiplication and inversion are continuous, and any continuous paths $\gamma,\eta:[0,1]\to G$ satisfying $\gamma(0)=\eta(0)=1_G$, $\mathrm{basedPathMul}(\gamma,\eta)$ is the continuous path $t\mapsto\gamma(t)\eta(t)$ for every $t\in[0,1]$. Its value at $0$ is $1_G$, so it belongs to the same space of paths starting at the identity; no condition is imposed on either input path’s value at $1$.

QAlgorithms.Papers.Independent.Intakethird100.P07.basedPathOne

For any type $G$ equipped with a topology and a group structure, $\mathrm{basedPathOne}$ is the constant continuous path $\gamma:[0,1]\to G$ given by $\gamma(t)=1_G$ for every $t\in[0,1]$. In particular, $\gamma(0)=1_G$, so it is an element of the space of continuous paths starting at the group identity. No continuity of the group operations is assumed.

QAlgorithms.Papers.Independent.Intakethird100.P07.basedPathsTopology

For any type $G$ equipped with a topology and a group structure, this instance equips the set of continuous functions $\gamma:[0,1]\to G$ satisfying $\gamma(0)=1_G$ with the subspace topology inherited from the space $C([0,1],G)$ of continuous maps, which carries the compact-open topology. Here $[0,1]$ has its usual subspace topology, $1_G$ is the group identity, and no continuity of the group operations is assumed.

QAlgorithms.Papers.Independent.Intakethird100.P07.kCoreflector

This defines a functor from the category of topological spaces in universe $u$, with continuous maps as morphisms, to the category of spaces in universe $u$ that are compactly generated with respect to compact Hausdorff spaces in universe $u$. It sends each space $X$ to the same underlying set with topology $kX$, where $A\subseteq X$ is open exactly when every originally continuous map $g:S\to X$ from such a compact Hausdorff space has open inverse image $g^{-1}(A)$. It sends each continuous map $f:X\to Y$ to the same underlying function regarded as a continuous map $kX\to kY$, and these assignments preserve identity maps and composition.

QAlgorithms.Papers.Independent.Intakethird100.P07.kMap

For any topological spaces $X$ and $Y$ whose underlying types lie in universe $u$, and any continuous map $f:X\to Y$, this defines a continuous map $kX\to kY$ whose underlying function is $x\mapsto f(x)$. For either space $Z=X,Y$, the space $kZ$ has the underlying set of $Z$, and $A\subseteq Z$ is open in $kZ$ exactly when $g^{-1}(A)$ is open for every compact Hausdorff space $S$ in universe $u$ and every continuous map $g:S\to Z$ using the original topology of $Z$.

QAlgorithms.Papers.Independent.Intakethird100.P07.kProbe

Let $X$ be a topological space in universe $u$, let $S$ be any compact Hausdorff space in universe $u$, and let $f:S\to X$ be continuous. Equip the underlying set $X$ with the topology in which a subset $A$ is open exactly when $g^{-1}(A)$ is open for every continuous map $g:T\to X$ from any compact Hausdorff space $T$ in universe $u$, where continuity of $g$ is measured using the original topology on $X$. This defines a continuous map from $S$ into that newly topologized space $K(X)$ whose value at every $a\in S$ is exactly $f(a)$.

QAlgorithms.Papers.Independent.Intakethird100.P07.kProductCone

For any index type $I$ in universe $u$ and any family $(Y_i)_{i\in I}$ of spaces in universe $u$ compactly generated with respect to compact Hausdorff spaces in universe $u$, this defines a cone over the family in the category of such spaces. Its vertex is $k\bigl(\prod_{i\in I}Y_i\bigr)$, where the product first has its usual product topology and a subset of the product is then declared open exactly when its inverse image is open under every continuous map from a compact Hausdorff space in universe $u$ into that original product. Its leg to $Y_i$, for each $i\in I$, is the continuous coordinate projection $x\mapsto x_i$. The definition also applies when $I$ is empty, in which case the underlying product is a singleton and there are no legs.

QAlgorithms.Papers.Independent.Intakethird100.P07.kSpaceGenerated

For every type $X$ in universe $u$, equipped with any topology, the same underlying set equipped with its compactly generated topology, denoted $kX$, is compactly generated with respect to compact Hausdorff spaces in universe $u$. Here the topology on $kX$ is defined by declaring $A\subseteq X$ open exactly when $g^{-1}(A)$ is open for every compact Hausdorff space $S$ in universe $u$ and every continuous map $g:S\to X$, where continuity into $X$ uses its original topology. The asserted compact generation means that openness in $kX$ is likewise detected by continuous maps from such spaces into $kX$. No separation or nonemptiness assumption is imposed on $X$.

QAlgorithms.Papers.Independent.Intakethird100.P07.kSpaceTopology

For every topological space $X$ whose underlying type lies in universe $u$, this equips the same underlying set $K(X)=X$ with the finest topology for which every map $f:S\to X$ continuous for the original topology, with $S$ a compact Hausdorff space in universe $u$, remains continuous as a map into $K(X)$. Equivalently, a subset $A\subseteq K(X)$ is open exactly when $f^{-1}(A)$ is open in $S$ for every such $S$ and $f$.

QAlgorithms.Papers.Independent.Intakethird100.P07.kToOriginal

For any topological spaces $X$ and $Y$ whose underlying types lie in universe $u$, and any continuous map $f:X\to Y$, this defines a continuous map $kX\to Y$ with the same underlying function $x\mapsto f(x)$. Here $kX$ has the same underlying set as $X$, with $A\subseteq X$ open precisely when $g^{-1}(A)$ is open for every compact Hausdorff space $S$ in universe $u$ and every originally continuous map $g:S\to X$; $Y$ retains its given topology.

QAlgorithms.Papers.Independent.Intakethird100.P07.pathRescale

Let $G$ be a group equipped with a topology, let $\gamma:[0,1]\to G$ be a continuous path satisfying $\gamma(0)=1$, and let $s\in[0,1]$. This defines a new continuous path based at $1$ by $\gamma_s(t)=\gamma(st)$ for every $t\in[0,1]$. In particular, the definition includes $s=0$, which gives the constant path at $1$, and $s=1$, which gives $\gamma$.

QAlgorithms.Papers.Independent.Intakethird100.P07.scalarHomotopy

For any type $V$ equipped with a specified scalar multiplication operation $\mathbb R\times V\to V$, and any pair $p=(x,t)\in V\times[0,1]$, $\mathrm{scalarHomotopy}(p)$ is defined to be $t\mathbin{\bullet}x$, using the underlying real number of $t$. The scalar multiplication operation is not required here to satisfy any module or action axioms, so this definition alone imposes no particular values at $t=0$ or $t=1$.

QAlgorithms.Papers.Independent.Intakethird100.P07.scaledTime

For any real numbers $s,t\in[0,1]$, this defines their scaled time to be the product $st$, regarded as an element of $[0,1]$; the accompanying bounds establish $0\le st\le1$. Both endpoints of the interval are included.

QAlgorithms.Papers.Independent.Intakethird100.P07.timeOne

$\mathrm{timeOne}$ is the element of $\mathrm{UnitTime}=[0,1]\subseteq\mathbb R$ whose underlying real number is $1$.

QAlgorithms.Papers.Independent.Intakethird100.P07.timeZero

$\mathrm{timeZero}$ is the element of $\mathrm{UnitTime}=[0,1]\subseteq\mathbb R$ whose underlying real number is $0$.