migration to Lean architect

Stream: Infinity-Cosmos

[Emily Riehl]

A quick heads up: we're planning to migrate the infinity cosmos repository to the new Lean architect system developed by @Pietro Monticone and @Hanwen Zhu. They have a draft PR now. I'll alert everyone here once it's merged.

[Emily Riehl]

Note I just merged @Arnoud van der Leer's coherent iso PR so that this will be included before the migration.

[Thomas Zhu]

Thanks Emily for the heads up! By the way I think you linked the wrong @Hanwen Zhu, I developed LeanArchitect :)

[Emily Riehl]

As of today the infinity-cosmos repository is now using LeanArchitect, developed by @Thomas Zhu and @Pietro Monticone. Their system makes it possible to automatically generate the blueprint (or parts of the blueprint) using tags directly in the Lean code.

[Emily Riehl]

For example, in our content.tex file, the LaTeX source for the blueprint we have:

Before introducing an axiomatic framework that allows us to develop $\infty$-cat\-e\-gory theory in general, we first consider one model in particular: \emph{quasi-cat\-e\-go\-ries}, which were introduced in 1973 by Boardman and Vogt \cite{BoardmanVogt:1973hi} in their study of homotopy coherent diagrams. Ordinary 1-categories give examples of quasi-categories via the construction of Definition \ref{defn:nerve}. Joyal first undertook the task of extending 1-category theory to quasi-category theory in \cite{Joyal:2002qk} and \cite{Joyal:2008tq} and in several unpublished draft book manuscripts. The majority of the results in this section are due to him.

\inputleannode{defn:simplex-category}

The maps in the simplex category include in particular:

\inputleannode{defn:face-map}

\inputleannode{defn:degeneracy-map}

The commands inputleannode refer to text that can be found in the Lean code.

[Emily Riehl]

In the ForMathlib folder of our repo, we have a file with contents:

import Architect
import Mathlib.AlgebraicTopology.SimplexCategory.Basic

open CategoryTheory SimplexCategory

namespace SimplexCategory

attribute [blueprint
  "defn:simplex-category"
  (title := "the simplex category")
  (statement := /--
  Let $\Del$ denote the \textbf{simplex category} of finite nonempty ordinals $[n] = \{0 <1 <\cdots
  < n\}$ and order-preserving maps.
  -/)]
  smallCategory

attribute [blueprint
  "defn:face-map"
  (title := "elementary face maps")
  (statement := /--
  The \textbf{elementary~face~operators} are the maps
  \begin{center}
  \begin{tikzcd}[row sep=tiny, column sep=small]
     {[n-1]} \arrow[r, tail, "{\face^i}"] & {[n]}  & {0 \leq i \leq n}
  \end{tikzcd}
  \end{center}
  whose images omit the element $i \in [n]$.
  -/)]
  δ

attribute [blueprint
  "defn:degeneracy-map"
  (title := "elementary degeneracy maps")
  (statement := /--
    The \textbf{elementary~degeneracy~operators} are the maps
  \begin{center}
  \begin{tikzcd}[row sep=tiny, column sep=small]
   {[n+1]} \arrow[r, two heads, "{\degen^i}"] & {[n]} & {0 \leq i \leq n }
  \end{tikzcd}
  \end{center}
  whose images  double up on the element $i \in [n]$.
  -/)]
  σ

attribute [blueprint
  "prop:simplex-cat-factorization"
  (statement := /--
  Every morphism in $\Del$ factors uniquely as an epimorphism followed by a monomorphism; these
  epimorphisms, the \textbf{degeneracy operators}, decompose as composites of elementary degeneracy
  operators, while the monomorphisms, the \textbf{face operators}, decompose as composites of
  elementary face operators.
  -/)
  (proof := /--
  The image factorizations have been formalized but the canonical decompositions into elementary
  face and degeneracy operators remain to be done.
  -/)
  (latexEnv := "proposition")]
  SimplexCategory.instHasStrongEpiImages

def δ_zero_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) :
    δ 0 ≫ mkOfLe i j h = (mk 0).const (mk n) j := by
  ext x; fin_cases x; simp [δ, mkOfLe, const]

def δ_one_mkOfLe {n : ℕ} (i j : Fin (n + 1)) (h : i ≤ j) :
    δ 1 ≫ mkOfLe i j h = (mk 0).const (mk n) i := by
  ext x; fin_cases x; simp [δ, mkOfLe, const]

end SimplexCategory

[Emily Riehl]

This provides LaTeX text --- including a tikzcd diagram !! --- as well as Lean references, e.g., to SimplexCategory.smallCategory.

[Emily Riehl]

Contributors to this project will know that the blueprint has been woefully misaligned with the current formalization status and targets. I'm hoping this integration will make it easier in the future to automatically extend the blueprint while, e.g., formalizing statements of theorems with sorries or contributing new definitions in support of proving one of the existing targets.