Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized

Proposition 2.4.7

Let

\[ M \colon \mathrm{ProFin}^{\mathrm{op}}\longrightarrow \mathrm{Ab} \]

be a functor, i.e. a presheaf of abelian groups on $\mathrm{ProFin}$. Assume that $M$ preserves finite products, and that for any surjective map $f: T\to S$, the complex

\[ 0\longrightarrow M(S)\longrightarrow M(T)\longrightarrow M(T\times _S T)\longrightarrow M(T\times _S T\times _S T)\longrightarrow \ldots \]

is exact.

Then $M$ is a condensed abelian group, and for all profinite sets $S$ and $i{\gt}0$, one has $H^i(S,M)=0$ for $i{\gt}0$.

LaTeX Lean

Proposition 2.1.4

Consider an inverse system $(X_i)_i$ of compact-Hausdorffly-filtered-pseudonormed abelian groups where all transition maps $X_i\to X_j$ send $X_{i,\leq c}$ to $X_{j,\leq c}$. Then

\[ X_{\leq c} := \varprojlim _i X_{i,\leq c} \]

is compact Hausdorff, and

\[ X=\varinjlim _c X_{\leq c} \]

is naturally a compact-Hausdorffly-filtered pseudonormed abelian group which is the limit of $(X_i)_i$ in the strict category structure.

LaTeX Lean

Definition 1.2.3

A pseudo-normed group $M$ is CH-filtered if each of the sets $M_c$ is endowed with a topological space structure making it a compact Hausdorff space, such that following maps are all continuous:

the inclusion $M_{c_1} \to M_{c_2}$ (for $c_1 \le c_2$);
the negation $M_c \to M_c$;
the addition $M_{c_1} \times M_{c_2} \to M_{c_1 + c_2}$.

The pseudo-normed group $M$ is profinitely filtered if moreover the filtration sets $M_c$ are totally disconnected, making them profinite sets.

LaTeX

Lean

comphaus_filtered_pseudo_normed_group
profinitely_filtered_pseudo_normed_group

Proposition 2.4.5

Consider an exact sequence of abelian groups

\[ X'\overset {f}{\longrightarrow } X\overset {g}{\longrightarrow } X'' \]

such that all of $X'$, $X$ and $X''$ carry the structure of compact-Hausdorffly-filtered-pseudonormed abelian groups. Assume that $f(X'_{\leq c})\subset X_{\leq c}$ and $g(X_{\leq c})\subset X''_{\leq c}$. If the sequence is strongly exact with respect to $r$, then the sequence

\[ \underline{X'}\longrightarrow \underline{X}\longrightarrow \underline{X''} \]

of condensed abelian groups is exact.

LaTeX

Definition 1.2.5

A morphism of CH-filtered pseudo-normed groups $M \to N$ is a group homomorphism $f \colon M \to N$ that is

bounded: there is a constant $C$ such that $x \in M_c$ implies $f(x) \in N_{Cc}$;
continuous: for one (or equivalently all) constants $C$ as above, the induced map $M_c \to N_{Cc}$ is a morphism of profinite sets, i.e. continuous.

The reason the two definitions of continuity are equivalent is that a continuous injection from a compact space to a Hausdorff space must be a topological embedding.

A morphism $f \colon M \to N$ is strict if $x \in M_c$ implies $f(x) \in N_c$ (in other words, if we can take $C = 1$ in the boundedness condition above).

LaTeX Lean

Definition 1.2.6

Let $r'$ be a positive real number. A CH-filtered pseudo-normed group $M$ has an $r'$-action of $T^{-1}$ if it comes endowed with a distinguished morphism of CH-filtered pseudo-normed groups $T^{-1} \colon M \to M$ that is bounded by $r'^{-1}$: if $x \in M_c$ then $T^{-1}x \in M_{c/r'}$.

A morphism of CH-filtered pseudo-normed groups with $r'$-action of $T^{-1}$ is a morphism $f \colon M \to N$ of CH-filtered pseudo-normed groups that commutes with the action of $T^{-1}$.

LaTeX

Lean

comphaus_filtered_pseudo_normed_group_with_Tinv
comphaus_filtered_pseudo_normed_group_with_Tinv_hom

Definition 2.4.4

There is a natural functor

\begin{align*} \text{CHPNG} & \longrightarrow \operatorname{Cond}(\operatorname{Ab}) \\ M & \longmapsto \underline{M} \end{align*}

where $\underline{M}(S)$ is defined to be collection of functions $f \colon S \to M$ that factor as continuous through $M_c$, for some $c$. In symbols:

\[ M(S) = \{ f \colon S \to M \mid \exists c, f(S) \subset M_c \text{ and $f \colon S \to M_c$ is continuous}\} . \]

LaTeX Lean

Lemma 2.4.13

Let $0 {\lt} r {\lt} r' {\lt} 1$ be real numbers. Let $S$ be a profinite set, and let $V$ be an $r$-normed $\mathbb Z[T^{\pm 1}]$-module. Then $\operatorname{Ext}_{\mathrm{Mod}^{\mathrm{cond}}_{\mathbb Z[T^{-1}]}}^i(\mathcal L_{r'}(S), V) = 0$ for all $i {\gt} 0$. In other words,

\[ \operatorname{Ext}_{\mathbb Z}^i(\mathcal L_{r'}(S), V) \xrightarrow {[T⁻¹]_L - [T⁻¹]_V} \operatorname{Ext}_{\mathbb Z}^i(\mathcal L_{r'}(S), V) \]

is a bijection for all $i {\gt} 0$ and a surjection for $i = 0$.

LaTeX Lean

Lemma 2.4.10

Let $0 {\lt} r {\lt} r' {\lt} 1$ be real numbers. Let $S$ be a profinite set, and let $V$ be a $r$-normed (Banach?) $\mathbb Z[T^{\pm 1}]$-module. Then $\operatorname{Ext}_{\mathrm{Mod}^{\mathrm{cond}}_{\mathbb Z[T^{-1}]}}^i(\overline{\mathcal L}_{r'}(S), V) = 0$ for all $i \ge 0$. In other words,

\[ \operatorname{Ext}_{\mathbb Z}^i(\overline{\mathcal L}_{r'}(S), V) \xrightarrow {[T⁻¹]_L - [T⁻¹]_V} \operatorname{Ext}_{\mathbb Z}^i(\overline{\mathcal L}_{r'}(S), V) \]

is a bijection for all $i$.

LaTeX Lean

Lemma 2.4.11

Assume that in each degree $i$, the map

\[ (T^{-1})_V - (T^{-1})_{\mathcal M}: \mathrm{Ext}^i(Q'(\overline{\mathcal M}_{r'}(S))_{\leq c},V)\longrightarrow \mathrm{Ext}^i(Q'(\overline{\mathcal M}_{r'}(S))_{\leq r' c},V) \]

is a pro-isomorphism in $c$ (i.e., pro-systems of kernels, and of cokernels, are pro-zero). Then

\[ (T^{-1})_V - (T^{-1})_{\mathcal M}: \mathrm{Ext}^i(Q'(\overline{\mathcal M}_{r'}(S)),V)\longrightarrow \mathrm{Ext}^i(Q'(\overline{\mathcal M}_{r'}(S)),V). \]

is an isomorphism.

LaTeX

Lean

QprimeFP.short_exact
Lbar.useful_commsq_bicartesian

Theorem 1.7.1

Let $\mathsf{BD}= (n,f,h)$ be a Breen–Deligne package, and let $\kappa = (\kappa _0, \kappa _1, \kappa _2, \dots )$ be a sequence of constants in $\mathbb R_{\ge 0}$ that is $\mathsf{BD}$-suitable. Fix radii $1{\gt}r'{\gt}r{\gt}0$. For any $m$ there is some $k$ and $c_0$ such that for all profinite sets $S$ and all $r$-normed $\mathbb Z[T^{\pm 1}]$-modules $V$, the system of complexes

\[ C^{\mathsf{BD}}_{\kappa }(\overline{\mathcal L}_{r'}(S))_c^\bullet \colon \widehat{V}(\overline{\mathcal L}_{r'}(S)_{\leq c})^{T^{-1}} \longrightarrow \widehat{V}(\overline{\mathcal L}_{r'}(S)_{\leq \kappa _1c}^2)^{T^{-1}} \longrightarrow \ldots \]

is $\leq k$-exact in degrees $\leq m$ for $c\geq c_0$.

LaTeX Lean

Lemma 2.4.6

Let $S = \varprojlim S_i$ be a profinite set. Then $\mathbb Z[S]$ is naturally a profinitely filtered pseudo-normed group, via $\mathbb Z[S]_{\le c} = \varprojlim \mathbb Z[S_i]_{\le c}$, where $\mathbb Z[S_i]_{\le c}$ is the set $\{ \sum _{s \in S_i} n_s[s] \mid \sum _s |n_s| \le c\} $.

There is a natural isomorphism between the free condensed abelian group $\mathbb Z[S]$ and the colimit $\varinjlim _c \mathbb Z[S]_{\le c}$ of condensed sets.

LaTeX Lean

Proposition 2.3.1

For any $i\geq 0$, the functor $A\mapsto H_i(Q'(A))$ has the following properties:

It is additive, i.e.

\[ H_i(Q'(A\oplus B))\cong H_i(Q'(A))\oplus H_i(Q'(B)). \]
It commutes with filtered colimits, i.e. for a filtered inductive system $A_i$,

\[ \varinjlim _i H_i(Q'(A))\cong H_i(Q'(\varinjlim _i A_i)). \]

In particular, for torsion-free abelian groups $A$, there is a functorial isomorphism

\[ H_i(Q'(A))\cong H_i(Q'(\mathbb Z))\otimes A. \]

LaTeX

Lean

breen_deligne.package.eval_additive
breen_deligne.data.eval_functor_preserves_filtered_colimits

Definition 2.2.3

Let $0 {\lt} r' {\lt} 1$ be a real number, and let $S$ be a profinite set with a presentation $S=\varprojlim S_i$, where all $S_i$ are finite. For all $c{\gt}0$, let $\mathcal L_{r'}(S)_{\leq c}$ denote the projective limit

\[ \mathcal L_{r'}(S)_{\leq c}=\varprojlim \mathcal L_{r'}(S_i)_{\leq c}, \]

endowed with the projective limit topology, and set

\[ \mathcal L_{r'}(S)=\varinjlim _{c {\gt} 0}\mathcal L_{r'}(S)_{\leq c}. \]

LaTeX Lean

Definition 2.2.2

Let $0 {\lt} r' {\lt} 1$ be a real number, and let $S$ be a finite set. Then $\mathcal L_{r'}(S)$ denotes the group

\[ \mathcal L_{r'}(S)=\{ \sum _{s\in S,n\in \mathbb {Z}}a_{n,s}T^n[s] \mid a_{n,s}\in \mathbb {Z}, \sum _{n\in \mathbb {Z}, s\in S}\lvert a_{n,s}\rvert r^n {\lt} + \infty \} . \]

LaTeX Lean

Proposition 2.4.12

Let $0 {\lt} r {\lt} 1$ be a real number, and let $S$ be a profinite set. Decomposing $\mathbb Z((T))_r$ into positive and nonpositive coefficients yields a direct sum decomposition

\[ \mathbb Z((T))_r = T\mathbb Z[[T]]_r \oplus \mathbb Z[T^{-1}]. \]

This extends to a decomposition of spaces of measures

\[ \mathcal L_r(S) = \mathcal L(S,T\mathbb Z((T))_r) = \mathcal L(S,T\mathbb Z[[T]]_r) \oplus \mathcal L(S,\mathbb Z[T^{-1}]) \]

where $\mathcal M(S,\mathbb Z[T^{-1}]) = \mathbb Z[T^{-1}][S]$ is the free condensed $\mathbb Z[T^{-1}]$-module on $S$. Letting $\overline{\mathcal L}_r(S)= \mathcal L(S,T\mathbb Z[[T]]_r)$, we get a short exact sequence of condensed $\mathbb Z[T^{-1}]$-modules

\[ 0 \longrightarrow \mathbb Z[T^{-1}][S] \longrightarrow \mathcal L_r(S) \longrightarrow \overline{\mathcal L}_r(S) \longrightarrow 0. \]

LaTeX Lean

Lemma 2.4.14

Let $0 {\lt} p' {\lt} 1$ be a real number, let $S$ be a profinite set, and let $r'$ denote $(\tfrac 12)^{p'}$. There is a short exact sequence of condensed $\mathbb Z[T^{-1}]$-modules

\[ 0 \longrightarrow \mathcal L_{r'}(S) \longrightarrow \mathcal L_{r'}(S) \longrightarrow \mathcal M_{p'}(S) \longrightarrow 0 \]

where the first map is multiplication by $2T - 1$, and the second is evaluation at $T = \tfrac 12$.

LaTeX Lean

Theorem 2.4.15Clausen–Scholze

Let $0 {\lt} p' {\lt} p \le 1$ be real numbers, let $S$ be a profinite set, and let $V$ be a $p$-Banach space. Let $\mathcal M_{p'}(S)$ be the space of real $p'$-measures on $S$. Then

\[ \operatorname{Ext}^i_{\operatorname{Cond}(\operatorname{Ab})}(\mathcal M_{p'}(S),V) = 0 \]

for $i \ge 1$.

LaTeX Lean

Proposition 2.4.8

Let $(M,\| \cdot \| )$ be a complete normed group, regarded as a topological group. Then the corresponding condensed abelian group $\underline{M}$ sends any profinite set $S$ to the completion of normed group of locally constant maps $S\to M$ (with the supremum norm).

LaTeX Lean

Proposition 2.4.9

Let $(M,\| \cdot \| )$ be a complete normed group, regarded as a topological group. Then for any profinite set $S$, one has $H^i(S,\underline{M})=0$ for $i{\gt}0$.

LaTeX Lean

Definition 1.2.1

Let $r {\gt} 0$ be a real number. An $r$-normed $\mathbb Z[T^{\pm 1}]$-module is a semi-normed group $V$ endowed with an automorphism $T \colon V \to V$ such that for all $v \in V$ we have $\| T(v)\| = r\| v\| $.

LaTeX Lean

Definition 2.1.1

A $p$-Banach space $V$ is a complete topological $\mathbb R$-vector space whose topology is induced by a $p$-norm; that is, a norm satisfying $\| rv\| = |r|^p\| v\| $.

LaTeX Lean

Lemma 2.1.2

A $p$-Banach $V$ is (up to non-canonical choice) an $r$-Banach $\mathbb Z[T^{\pm 1}]$-module, where $r=2^{-p}$. (See Definition 1.2.1 for the definition of $r$-normed $\mathbb Z[T^{\pm 1}]$-modules.)

LaTeX Lean

Definition 2.1.3

We will consider the following categories:

$\text{CHPNG}$ the category of CH-filtered pseudo-normed groups with bounded morphisms.
$\text{CHPNG}_1$ the category of exhaustive CH-filtered pseudo-normed groups with strict morphisms.
$\text{ProfinPNG}$ the category of profinitely filtered pseudo-normed groups with bounded morphisms.
$\text{ProfinPNG}_1$ the category of exhaustive profinitely filtered pseudo-normed groups with strict morphisms.
$\text{ProfinPNGTinv}_1^{r'}$ the category of exhaustive profinitely filtered pseudo-normed groups with $r'$-action of $T^{-1}$ and strict morphisms.

LaTeX

Lean

CompHausFiltPseuNormGrp.large_category
CompHausFiltPseuNormGrp₁.category_theory.large_category
ProFiltPseuNormGrp.large_category
ProFiltPseuNormGrp₁.category_theory.large_category
ProFiltPseuNormGrpWithTinv₁.category_theory.large_category

Definition 1.2.2

A pseudo-normed group is an abelian group $(M,+)$, together with an increasing filtration $M_c \subseteq M$ of subsets $M_c$ indexed by $\mathbb R_{\ge 0}$, such that each $M_c$ contains $0$, is closed under negation, and $M_{c_1} + M_{c_2} \subseteq M_{c_1 + c_2}$. An example would be $M=\mathbb {R}$ or $M=\mathbb {Q}_p$ with $M_c :=\{ x\, :\, |x|\leq c\} $.

A pseudo-normed group $M$ is exhaustive if $\varinjlim _c M_c = M$.

LaTeX Lean

Corollary 2.3.2

For torsion-free condensed abelian groups $A$, there is a natural isomorphism

\[ H_i(Q'(A))\cong H_i(Q'(\mathbb Z))\otimes A \]

of condensed abelian groups.

LaTeX Lean

Proposition 2.3.3

Let $M$ and $N$ be condensed abelian groups with endomorphisms $f_M$, $f_N$. Assume that $M$ is torsion-free (over $\mathbb Z$). Then

\[ \mathrm{Ext}^i_{\mathbb Z[f]}(M,N)=0 \]

for all $i\geq 0$ if and only if

\[ \mathrm{Ext}^i_{\mathbb Z[f]}(Q'(M),N)=0 \]

for all $i\geq 0$. More precisely, the first vanishes for $0\leq i\leq j$ if and only if the second vanishes for $0\leq i\leq j$.

LaTeX Lean

Definition 2.2.1

Let $0 {\lt} p' {\lt} 1$ be a real number, and let $S$ be a finite set. Then $\mathcal M_{p'}(S)$ denotes the real vector space

\[ \mathcal M_{p'}(S) = \left\{ \sum _{s\in S}a_{s}[s] \text{ such that } a_{s}\in \mathbb {R}\right\} \]

endowed with the $\ell ^{p'}$-norm $\Vert \sum _{s\in S}a_s[s]\Vert _{\ell ^{p'}}=\sum _{s\in S}\lvert a_s\rvert ^{p'}$.

For every finite set $S$, the space $\mathcal M_{p'}(S)$ can be written as the colimit (or simply the union, in this case)

\[ \mathcal M_{p'}(S) = \varinjlim _{c{\gt}0}\mathcal M_{p'}(S)_{\leq c} \]

where $\mathcal M_{p'}(S)_{\leq c} = \left\{ F \in \mathcal M_{p'}(S) \text{ such that } \Vert F \Vert _{\ell ^{p'}}\leq c\right\} $. Now, given a profinite set $S=\varprojlim S_i$, where all $S_i$’s are finite sets, and a positive real number $c{\gt}0$, define $\mathcal M_{p'}(S)_{\leq c}$ as

\[ \mathcal M_{p'}(S)_{\leq c}=\varprojlim \mathcal M_{p'}(S_i)_{\leq c} \]

endowed with the projective limit topology. Finally, set $\mathcal M_{p'}(S)=\varinjlim _{c}\mathcal M_{p'}(S)_{\leq c}$.

LaTeX Lean

Definition 2.4.2

Consider an exact sequence of abelian groups

\[ X'\overset {f}{\longrightarrow } X\overset {g}{\longrightarrow } X'' \]

such that all of $X'$, $X$ and $X''$ carry the structure of compact-Hausdorffly-filtered-pseudonormed abelian groups. Assume that the maps are strict, i.e., $f(X'_{\leq c})\subset X_{\leq c}$ and $g(X_{\leq c})\subset X''_{\leq c}$. Let $r \colon \mathbb {R}_{\ge 0} \to \mathbb {R}_{\ge 0}$ be a function satisfying $c \le r(c)$ for all $c$. We say that the sequence is strongly exact with respect to $r$ if $\mathrm{ker}(g)\cap X_{\leq c}\subset f(X'_{\leq r(c)})$.

LaTeX

Proposition 2.4.3

Consider an inverse system

\[ (X_i'\overset {f}{\longrightarrow } X_i\overset {g}{\longrightarrow } X_i'')_i \]

of exact sequences that are strongly exact with respect to $r$ (independent of $i$). Moreover, assume that the transition maps $X'_i\to X'_j$, $X_i\to X_j$ and $X''_i\to X''_j$ are strict, and let $X'$, $X$ and $X''$ be their limits. Then

\[ X'\overset {f}{\longrightarrow } X\overset {g}{\longrightarrow } X'' \]

is strongly exact with respect to $r$.

LaTeX

Definition 2.2.4

Fix $0{\lt}\xi {\lt}1$, and let $\vartheta _{\xi }\colon \mathbb {Z}(\! (T)\! )_r\rightarrow \mathbb {R}$ be the evaluation map

\[ \sum a_nT^n\longmapsto \sum a_n\xi ^n. \]

LaTeX Lean

Lemma 2.2.7

Fix a finite set $S$, real numbers $0{\lt}\xi ,p'{\lt}1$ and set $r'=(\xi )^{p'}$. The map $\vartheta _\xi $ of Definition 2.2.4 is continuous when endowing $\mathcal L_{r'}(S)$ with the topology defined in Definition 2.2.2 and $\mathcal M_{p'}(S)$ with the topology defined in Definition 2.2.1

LaTeX Lean

Theorem 2.2.8

Let $0{\lt}p'{\lt}1$ be a real number, let $S$ be a finite set, and let $r'$ denote $\left(\frac{1}{2}\right)^{p'}$. The sequence

\[ 0\longrightarrow \mathcal L_{r'}(S)\longrightarrow \mathcal L_{r'}(S)\overset {\theta _S}{\longrightarrow } \mathcal M_{p'}(S)\longrightarrow 0, \]

where the first map is multiplication by $2T-1$, is exact. In particular, the kernel of $\theta _S$ is principal, generated by $2T-1$.

LaTeX Lean

Lemma 2.2.6

The map $\vartheta _{\xi }$ is surjective.

LaTeX Lean

Definition 2.2.5

For all $x \in \mathbb {R}$ and $n\in \mathbb {N}$, set

\[ Y_\xi (x, n)= \begin{cases} x& \text{ if } n = 0 \\ Y_\xi (x,n-1) - \left\lfloor \frac{Y_\xi (x,n-1)}{\xi ^{n-1}} \right\rfloor \xi ^{n-1} & \text{ if } n \ge 1 \end{cases} \]

where $\lfloor \ast \rfloor $ denotes the floor of $\ast $, namely the greatest integer that is less or equal than $\ast $.

LaTeX