753 lines
No EOL
29 KiB
Typst
753 lines
No EOL
29 KiB
Typst
#import "./style.typ": *
|
|
#import "@preview/fletcher:0.5.4" as fletcher: diagram, node, edge
|
|
#import "@preview/prooftrees:0.1.0": *
|
|
#import "@preview/cetz:0.3.1" as cetz: canvas, draw
|
|
#import "@preview/wrap-it:0.1.0": wrap-content
|
|
|
|
#show: doc => template(
|
|
title: "Serre Spectral Sequence Thesis",
|
|
doc,
|
|
)
|
|
|
|
= Introduction
|
|
|
|
This work extends Floris van Doorn's PhD dissertation @van_doorn_formalization_2018.
|
|
In that work, the mechanization of the proof was done in Lean 2's HoTT mode.
|
|
This mode has been removed from Lean's later versions.
|
|
|
|
Cubical offers benefits such as higher inductive types.
|
|
|
|
== Computer formalization
|
|
|
|
#TODO[Need to have this section at all?]
|
|
|
|
One of the benefits of using a computationally-friendly system of proof is that we can use computer programs (known as proof assistants) to verify the correctness of our proofs.
|
|
|
|
The primary proof assistant used in this work is Agda @agda_developers_agda_2025.
|
|
Agda is a dependently typed programming language that implements homotopy type theory.
|
|
// Unlike many other popular general proof assistants, it doesn't use a tactic language to express the proofs. Instead, proofs are done by writing the proof term directly.
|
|
|
|
Despite this, Agda is still friendly to the interactive theorem proving process, with the holes feature.
|
|
Inserting a question mark in place of a proof term adds a hole, which acts as a placeholder.
|
|
Type-checking continues assuming a proof term will be placed there later.
|
|
Additionally, the context at the hole can be queried with editor extensions, and refined with functions or constructors to produce more specific expressions but with holes where the arguments would be.
|
|
This allows for a top-down interactive theorem proving experience.
|
|
|
|
== Cubical Agda
|
|
|
|
The results in this paper have been formalized using Cubical Agda @vezzosi_cubical_2021, an extension to the Agda proof assistant that implements cubical type theory.
|
|
|
|
= Martin-Löf type theory
|
|
|
|
Martin-Löf type theory @martin-lof_intuitionistic_1975
|
|
|
|
== Judgements
|
|
|
|
== Types as terms
|
|
|
|
== Types as propositions
|
|
|
|
=== Definitional vs. propositional equality <defVsProp>
|
|
|
|
Because of the computational nature of the theory, we distinguish these equalities:
|
|
|
|
- $a$ and $b$ are *definitionally* (or judgmentally) equal, denoted $defEq(a, b)$, if they reduce to exactly the same term through reduction rules.
|
|
- $a$ and $b$ are *propositionally* equal, denoted $propEq(a, b)$, if there exists any term in the #link(<identityType>)[identity type] $propEq(a, b)$ (will be introduced in a later section).
|
|
|
|
For example, given the definition for $isTyp(+, arro(NN, NN, NN))$ defined by induction on the first operand, the term $2+2$ reduces to $4$, so they are considered definitionally equal. There is a term $refl$, which is of the type $propEq(x,x)$ for any $x$. In this case, we have $refl : propEq(2+2,4)$.
|
|
|
|
On the other hand, for some arbitrary $isTyp(#[$a, b$], NN)$, the term $a+b$ and $b+a$ can never be reduced to the same expression exactly. But we know that once we substitute values for $a$ and $b$, this expression will produce the same result. We can derive an expression to reflect this equality by induction on the first operand.
|
|
|
|
== Basic types
|
|
|
|
We introduce a handful of common types that will be used later.
|
|
Each type is described with a few rules:
|
|
#TODO[Describe inference rules before this.]
|
|
|
|
- *Type former rule.* This describes how this type is derived. For simple types such as the natural numbers, this rule has no hypothesis. However, parameterized types such as List will require an input type.
|
|
- *Introduction rule.* This describes how to construct values of this type.
|
|
- *Elimination rule.* This describes ways to consume values of this type.
|
|
- *Computation rule.* This describes the value resulting from the elimination rules.
|
|
|
|
As an example, the unit type will be described fully in terms of these four rules.
|
|
The result will be in an abbreviated form, with the full rules being available in Appendix A.2 of the HoTT Book @the_univalent_foundations_program_homotopy_2013.
|
|
|
|
=== Unit type ($unitType$) <unitType>
|
|
|
|
The unit type $unitType$ is the type with only a single inhabitant, $isTyp(tt, unitType)$.
|
|
|
|
$ isTyp(ind_unitType,
|
|
product_isTyp(C, arro(unitType, typ))
|
|
arro((isTyp(c, product_isTyp(x, unitType) C(x))), (isTyp(y, unitType)) , C(y))) $
|
|
|
|
=== Boolean type ($boolType$) <boolType>
|
|
|
|
Similar to the unit type, the boolean type $boolType$ is the type with only two inhabitants, which we will call $isTyp(bTrue, boolType)$ and $isTyp(bFalse, boolType)$.
|
|
|
|
=== Empty type ($emptyType$)
|
|
|
|
The empty type $emptyType$ is the type with no inhabitants.
|
|
To be able to derive an element of this type indicates inconsistency of the logical system entirely.
|
|
|
|
The eliminator for the empty type is hence the principle of #link("https://en.wikipedia.org/wiki/Principle_of_explosion")[_ex falso quodlibet_]: given an element of the empty type, we can produce a term of any type.
|
|
|
|
$ isTyp(ind_emptyType, product_isTyp(A, typ) arro(emptyType, A)) $
|
|
|
|
A function $arro(A, emptyType)$ represents a proof of the negation of $A$, since as a consequence $A$ implies false.
|
|
We also write $negOf(A)$ as a shorthand for $arro(A, emptyType)$.
|
|
|
|
== Functions ($Pi$)
|
|
|
|
A *function* from type $A$ to type $B$ is written as $arro(A, B)$.
|
|
Functions are defined using the $lambda$ constructor, which introduces a fresh name into the binding context for the body.
|
|
|
|
As an example, $isTyp((lam(x, x + 1)), arro(NN, NN))$ is a function that increments $x$.
|
|
|
|
Functions are generalized by _dependent functions_, in which the return type may depend on the _value_ of the input.
|
|
This is primarily useful in the presence of type families, which are functions that return $typ$.
|
|
Given a type family $isTyp(P, arro(A, typ))$, we can write a dependent function $isTyp(f(x), arro((isTyp(x, A)), P(x)))$.
|
|
|
|
For example, consider the $BoolVec$ type defined above.
|
|
In particular, $BoolVec$ is indexed by the number of elements it contains.
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
line((-2, 0), (-2, 3.5), mark: (end: ">"))
|
|
content((-2, 4))[$NN$]
|
|
content((5, 4))[$typ$]
|
|
|
|
for y in (0, 1, 2, 3) {
|
|
content((-2.5, y))[$#y$]
|
|
point((-2, y))
|
|
|
|
content((4.5, y), anchor: "west")[$BoolVec\(#y)$]
|
|
circle((2, y), radius: (2, 0.4), fill: rgb(180 + y * 20, 180, 180))
|
|
|
|
// arc((-1.8, y), start: -100deg, stop: -80deg, radius: 5.0, mark: (end: ">"))
|
|
// content((-1, y + 0.15), text(size: 0.8em, $Vec$))
|
|
}
|
|
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffcc"), padding: .1))
|
|
|
|
point((2, 0))
|
|
content((2, -0.35), text(size: 0.8em)[$[]$])
|
|
|
|
let t = $sans("t")$
|
|
let f = $sans("f")$
|
|
|
|
point((1.5, 1))
|
|
point((2.5, 1))
|
|
content((1.5, 0.65), text(size: 0.8em)[$[t]$])
|
|
content((2.5, 0.65), text(size: 0.8em)[$[f]$])
|
|
|
|
point((0.75, 2))
|
|
point((1.5, 2))
|
|
point((2.25, 2))
|
|
content((3, 2))[$dots$]
|
|
content((0.75, 1.65), text(size: 0.7em)[$[t, t]$])
|
|
content((1.5, 1.65), text(size: 0.7em)[$[t, f]$])
|
|
content((2.25, 1.65), text(size: 0.7em)[$[f, t]$])
|
|
|
|
point((0.75, 3))
|
|
point((1.5, 3))
|
|
point((2.25, 3))
|
|
content((3, 3))[$dots$]
|
|
content((0.75, 2.65), text(size: 0.5em)[$[t, t, t]$])
|
|
content((1.5, 2.65), text(size: 0.5em)[$[t, t, f]$])
|
|
content((2.25, 2.65), text(size: 0.5em)[$[t, f, t]$])
|
|
}), caption: $isTyp(BoolVec, arro(NN, typ))$)
|
|
|
|
We can then write a function that, for example, maps some natural number to the vector only containing $bTrue$.
|
|
|
|
$ isTyp(sans("onlyTrue"), arro(\(n : NN\), BoolVec\(n))) $
|
|
|
|
The first parameter of the function must be named (in this case as $n$), since the output type _depends_ on the value of $n$.
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
let faded = rgb("#999")
|
|
set-style(stroke: faded)
|
|
line((-2, 0), (-2, 3.5), mark: (end: ">"))
|
|
content((-2, 4))[$NN$]
|
|
content((5, 4))[$typ$]
|
|
|
|
for y in (0, 1, 2, 3) {
|
|
content((-2.5, y))[$#y$]
|
|
point((-2, y))
|
|
|
|
content((4.5, y), anchor: "west")[$BoolVec\(#y)$]
|
|
circle((2, y), radius: (2, 0.4), fill: rgb(200 + y * 10, 200, 200))
|
|
}
|
|
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffcc"), padding: .1))
|
|
|
|
point((2, 0))
|
|
content((2, -0.35), text(size: 0.8em)[$[]$])
|
|
|
|
let t = $sans("t")$
|
|
let f = $sans("f")$
|
|
|
|
point((1.5, 1))
|
|
point((2.5, 1), paint: faded)
|
|
content((1.5, 0.65), text(size: 0.8em)[$[t]$])
|
|
content((2.5, 0.65), text(size: 0.8em)[$[f]$])
|
|
|
|
point((0.75, 2))
|
|
point((1.5, 2), paint: faded)
|
|
point((2.25, 2), paint: faded)
|
|
content((3, 2))[$dots$]
|
|
content((0.75, 1.65), text(size: 0.7em)[$[t, t]$])
|
|
content((1.5, 1.65), text(size: 0.7em)[$[t, f]$])
|
|
content((2.25, 1.65), text(size: 0.7em)[$[f, t]$])
|
|
|
|
point((0.75, 3))
|
|
point((1.5, 3), paint: faded)
|
|
point((2.25, 3), paint: faded)
|
|
content((3, 3))[$dots$]
|
|
content((0.75, 2.65), text(size: 0.5em)[$[t, t, t]$])
|
|
content((1.5, 2.65), text(size: 0.5em)[$[t, t, f]$])
|
|
content((2.25, 2.65), text(size: 0.5em)[$[t, f, t]$])
|
|
|
|
set-style(stroke: black)
|
|
arc((-1.8, 0), start: -100deg, stop: -80deg, radius: 10.5, mark: (end: ">"))
|
|
arc((-1.8, 1), start: -100deg, stop: -80deg, radius: 9.0, mark: (end: ">"))
|
|
arc((-1.8, 2), start: -100deg, stop: -80deg, radius: 7.0, mark: (end: ">"))
|
|
arc((-1.8, 3), start: -100deg, stop: -80deg, radius: 7.0, mark: (end: ">"))
|
|
// content((-1, y + 0.15), text(size: 0.8em, $Vec$))
|
|
}), caption: $isTyp(sans("onlyTrue"), arro(\(n : NN\), BoolVec\(n)))$)
|
|
|
|
== Pairs ($Sigma$)
|
|
|
|
== Universes
|
|
|
|
Universe levels will be elided in this document for brevity, however they are always present.
|
|
Many types will be universe-polymorphic, and in the formalization there will be universe levels attached to most types.
|
|
|
|
== Identity type ($propEqSym$) <identityType>
|
|
|
|
=== Path Induction
|
|
|
|
...
|
|
|
|
=== $ap$
|
|
|
|
Due to the inductive definition of paths, we get the property that functions are functorial over paths.
|
|
|
|
#definition($ap$)[
|
|
Given any function $isTyp(f, arro(A, B))$ and points $isTyp(#[$x, y$], A)$, there exists a term of type:
|
|
|
|
$ isTyp(ap, arro((propEqTy(x, y, A)), (propEqTy(f(x), f(y), B)))) $
|
|
|
|
It takes paths in $A$ and returns paths in $B$.
|
|
]
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffee"), padding: .1))
|
|
|
|
content((-2, 2.5))[$A$]
|
|
content((2, 2.5))[$B$]
|
|
|
|
circle((-2, 0), radius: (1, 2), name: "A", fill: rgb("#ffffee"))
|
|
point((-2.2, 1), name: "x")
|
|
content((rel: (-0.3, -0.2)))[$x$]
|
|
// point((-1.6, 0), name: "y")
|
|
// content((rel: (-0.3, 0)))[$y$]
|
|
point((-2, -1), name: "y")
|
|
content((rel: (-0.3, 0.2)))[$y$]
|
|
|
|
circle((2, 0), radius: (1, 2), name: "B", fill: rgb("#ffeeee"))
|
|
point((2.2, 1), name: "x")
|
|
content((rel: (0.6, -0.2)))[$f(x)$]
|
|
// point((1.6, 0), name: "y")
|
|
// content((rel: (0.6, 0)))[$f(y)$]
|
|
point((2, -1), name: "fy")
|
|
content((rel: (0.6, 0.2)))[$f(y)$]
|
|
|
|
let faded = rgb("#99999988")
|
|
arc((-2.2, 1), start: -100deg, stop: -80deg, radius: 12.5, stroke: faded, mark: (end: "stealth"))
|
|
arc((-2, -1), start: 100deg, stop: 80deg, radius: 11.5, stroke: faded, mark: (end: "stealth"))
|
|
|
|
arc((-2.2, 1), start: 12deg, stop: 0deg, radius: 9.5, mark: (end: "stealth"))
|
|
content((-1.8, 0), $p$)
|
|
arc((2.2, 1), start: 168deg, stop: 180deg, radius: 9.5, mark: (end: "stealth"))
|
|
content((1.2, 0), $ap_f\(p)$)
|
|
}), caption: [The function $ap$])
|
|
|
|
#proof[
|
|
]
|
|
|
|
A consequence of the property that all functions preserve paths is that all functions in homotopy type theory are continuous by default.
|
|
|
|
=== Transport
|
|
|
|
=== $apd$
|
|
|
|
The above definition only applies to _non-dependent_ functions, since $B$ does not depend on the choice of $A$.
|
|
We can formulate a _dependent_ version of $ap$ as follows.
|
|
For some choice $isTyp(x, A)$, we would like $f(x)$ to be of type $B(x)$.
|
|
|
|
=== Groupoid laws
|
|
|
|
The path space of any particular space forms a _groupoid_.
|
|
This means it is equipped with the following operations:
|
|
|
|
- $(-)^(-1) : arro((propEq(a, b)), (propEq(b, a)))$
|
|
- $(dot) : arro((propEq(a, b)), (propEq(b, c)), (propEq(a, c)))$
|
|
|
|
These operations respect the following laws:
|
|
|
|
- $sans("assoc") : propEq(((p dot q) dot r), (p dot (q dot r)))$
|
|
|
|
= Homotopy type theory
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffee"), padding: .1))
|
|
|
|
content((-2, 2.5))[$A$]
|
|
content((2, 2.5))[$B$]
|
|
|
|
circle((-2, 0), radius: (1, 2), name: "A", fill: rgb("#ffffee"))
|
|
point((-2, 0), name: "y")
|
|
content((rel: (-0.3, 0)))[$y$]
|
|
|
|
circle((2, 0), radius: (1, 2), name: "B", fill: rgb("#ffeeee"))
|
|
point((2, 1), name: "y1")
|
|
content((rel: (0.6, 0)))[$f(y)$]
|
|
point((2, -1), name: "y2")
|
|
content((rel: (0.6, 0)))[$g(y)$]
|
|
|
|
merge-path(fill: gradient.linear(..(rgb("#ff9999cc"), rgb("#9999ffcc")), angle: 90deg), {
|
|
bezier((-2, 0), (2, 1), (0, 0), (-1, 2))
|
|
line((2, 1), (2, -1))
|
|
bezier((2, -1), (-2, 0), (0, -1), (0, -2))
|
|
})
|
|
content((2.3, 0))[$p$]
|
|
}), caption: [Homotopy])
|
|
|
|
== Equivalences
|
|
|
|
== Univalence axiom <univalence>
|
|
|
|
One of the key observations of homotopy type theory is that the equivalence type $eqv(A, B)$ internally reflects an underlying equality between $A$ and $B$.
|
|
The *univalence axiom* realizes this idea by giving a way to "upgrade" our equivalence into a propositional equality:
|
|
|
|
#axiom("Univalence")[
|
|
$ isTyp(ua, arro((eqv(A, B)), (propEq(A, B)))) $
|
|
] <univalenceAxiom>
|
|
|
|
Furthermore, this function itself is an equivalence:
|
|
|
|
#axiom("Univalence equivalence")[
|
|
$ isTyp(uaEqv, isEquiv(ua)) $
|
|
] <univalenceEqvAxiom>
|
|
|
|
This property is not expressible with book HoTT, hence it is known as the "univalence axiom."
|
|
|
|
One consequence of this axiom is the ability to create non-trivial paths.
|
|
|
|
As an example, consider the path space $propEq(boolType, boolType)$.
|
|
The trivial path $refl$ reflects the equivalence of the identity function $isTyp(idfun, arro(boolType, boolType))$.
|
|
However, the function $isTyp(neg, arro(boolType, boolType))$ defined by $bTrue |-> bFalse$ and $bFalse |-> bTrue$ also exhibits an equivalence, and thus can be upgraded via univalence to a term $isTyp(ua(neg), propEq(boolType, boolType))$, which has the same type.
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffcc"), padding: .1))
|
|
|
|
circle((-3, 0), radius: (2, 1), fill: rgb("#ffffee"))
|
|
content((-3, 1.5))[$typ$]
|
|
point((-3, 0))
|
|
arc((-3.1, 0.15), start: 20deg, delta: 330deg, radius: 0.5, mark: (end: ">"))
|
|
arc((-2.9, 0.15), start: 160deg, delta: -330deg, radius: 0.5, mark: (end: ">"))
|
|
content((-4.0, 0), text(size: .8em, $refl$))
|
|
content((-2.0, 0), text(size: .8em, $ua(neg)$))
|
|
|
|
circle((3, 0), radius: (2, 1), fill: rgb("#ffeeee"))
|
|
content((3, 1.5))[$propEq(boolType, boolType)$]
|
|
point((2.25, 0))
|
|
point((3.75, 0))
|
|
content((2.25, -0.4), text(size: .8em, $refl$))
|
|
content((3.75, -0.4), text(size: .8em, $ua(neg)$))
|
|
}), caption: [Left: paths $refl$ and $ua(neg)$ visualized in the type of $typ$s, right: paths visualized in the path space $propEq(boolType, boolType)$])
|
|
|
|
== Pointed types
|
|
|
|
Pointed types are essentially some type equipped with a distinguished base point.
|
|
|
|
#definition("Pointed type")[
|
|
$ defEq(typ_circle.small.filled, sum_(isTyp(A, typ)) A) $
|
|
] <pointedType>
|
|
|
|
Some examples of pointed types include:
|
|
|
|
- The contractible type: $(unitType, tt)$
|
|
- Some path type: $(propEq(a, b), refl)$
|
|
|
|
Some types have fairly straightforward notions of a "nice" base point:
|
|
|
|
- For a contractible type, its center as the base point
|
|
- For path types, $refl$ is the base point
|
|
- For groups, the identity element is the base point
|
|
|
|
Of course, since pointed types are just a pair, we can choose any base point we want.
|
|
But for the definition of pointed functions below, you may find that some base points lend to more convenient definitions of the pointed functions than others.
|
|
|
|
== Higher inductive types
|
|
|
|
#[
|
|
#let diagram = figure(canvas({
|
|
import draw: *
|
|
set-style(content: (frame: "rect", stroke: none, fill: rgb("#ffffffcc"), padding: .1))
|
|
bezier((-2, 0), (2, 0), (0, 1), (0, -1), mark: (end: ">"))
|
|
point((-2, 0))
|
|
point((2, 0))
|
|
content((-2.2, 0), anchor: "east")[$a$]
|
|
content((2.2, 0), anchor: "west")[$b$]
|
|
content((0, 0))[$seg$]
|
|
}), caption: [An interval])
|
|
|
|
#wrap-content(diagram, align: right)[
|
|
Our story of higher inductive types begins with a motivating example, the interval.
|
|
This interval type consists of two points, which we will name $a$ and $b$, along with a path that connects them.
|
|
|
|
If you were given some element of this interval, it could be either $a$, $b$, _or_ some point along the path named $isTyp(seg, propEq(a, b))$.
|
|
An eliminator for this type must then handle the $seg$ case.
|
|
]
|
|
]
|
|
|
|
Remember that functions in homotopy type theory are all continuous.
|
|
This means that if there is a path $propEq(a, b)$ in the domain of a function $f$, then there must be a path $propEq(f(a), f(b))$ in the codomain.
|
|
|
|
In fact, this $ap$ function becomes part of the elimination rule for a higher inductive type.
|
|
|
|
=== Elimination and computation rules
|
|
|
|
=== Circle ($S1$) <circle>
|
|
|
|
The circle is a simple yet rich space that demonstrates a lot of interesting properties.
|
|
Analytically, the circle could be defined as the set of points $isTyp((x, y), RR times RR)$ such that:
|
|
|
|
$ x^2 + y^2 = 1 $
|
|
|
|
// #align(center, canvas({
|
|
// import draw: *
|
|
// grid((-3, -3), (3, 3), stroke: luma(90%))
|
|
// circle((0, 0), radius: 2)
|
|
// }))
|
|
|
|
In synthetic homotopy theory, we distill the circle to its only distinguishing property: that it cannot be contracted into a point, due to the hole in the middle.
|
|
We call this type $S1$, where the 1 indicates that it is a 1-dimensional sphere.
|
|
|
|
For some arbitrary choice of base point, denoted $isTyp(base, S1)$, we can imagine the circle as a path going from the base to itself.
|
|
We call this path $isTyp(loop, propEq(base, base))$.
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
circle((0, 2), radius: 2)
|
|
content((0, 4.5), $loop$)
|
|
circle((0, 0), radius: 0.05) // , stroke: (paint: red, thickness: 3pt))
|
|
content((0, 0.5), text($base$))
|
|
}), caption: [A circle])
|
|
|
|
=== Suspensions ($Sigma$)
|
|
|
|
=== Truncations
|
|
|
|
== Homotopy levels <hlevels>
|
|
|
|
#agdaCubicalLink("Cubical.Foundations.HLevels")
|
|
#footnote[
|
|
Homotopy levels are also known under a different name, homotopy $n$-types.
|
|
Although the name is the same, the numbers are offset by 2, such that sets are $0$-types, mere props are $(-1)$-types, and contractible types are $(-2)$-types.
|
|
This may introduce a lot of confusion, so for the purposes of this paper I will stick to homotopy levels since it makes more sense to begin induction on homotopy levels from 0.
|
|
]
|
|
|
|
= Cubical type theory <cubicaltt>
|
|
|
|
Cubical type theory @cohen_cubical_2016
|
|
|
|
== Cubical interval
|
|
|
|
== $sans(#[hcomp])$ and $sans(#[hfill])$
|
|
|
|
== $sans(#[Glue])$ and $sans(#[glue])$
|
|
|
|
= Algebra
|
|
|
|
== Groups
|
|
|
|
#definition("Group")[
|
|
A group ($G$, $dot$) is a type ($G$) equipped with a binary operation ($dot$) that satisfies a few axioms.
|
|
|
|
- Associativity: $arro((isTyp(a\, b\, c, G)), propEq((a dot b) dot c, a dot (b dot c)))$.
|
|
- Identity:
|
|
- There exists an element $0_G$ known as the identity element. The group $G$ may be omitted if it is clear from context.
|
|
- For any element $isTyp(a, G)$, there exist terms of type $(propEq(a dot 0, a))$ and $(propEq(0 dot a, a))$.
|
|
- Inverse:
|
|
- There exists an operation $isTyp((-)^(-1), arro(G, G))$.
|
|
- For any element $isTyp(a, G)$, there exist terms of type $(propEq(a dot a^(-1), 0_G))$ and $(propEq(a^(-1) dot a, 0_G))$.
|
|
] <group>
|
|
|
|
The mechanized definition of this can be found in #agdaCubicalLink("Cubical.Algebra.Group.Base").
|
|
|
|
#definition("Abelian group")[] <abelianGroup>
|
|
|
|
== Images and kernels
|
|
|
|
For any function $isTyp(f, arro(A, B))$, we can define the image of $f$, denoted $imOf(f)$ to be all of the elements in $B$ such that are mapped to from $A$. This differs from the _codomain_ of $f$, which is the entire set $B$ including points that cannot be mapped to.
|
|
|
|
#definition("Image")[
|
|
For types $A$ and $B$, and a function $isTyp(f, arro(A, B))$, define:
|
|
$ defEq(imOf(f), sum_(isTyp(b, B)) (sum_(isTyp(a, A)) propEq(f(a), b))) $
|
|
|
|
#TODO[This needs to be mere existence, but I need to figure out how to write that]
|
|
] <image>
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
content((0, 2.5), $A$)
|
|
circle((0, 0), radius: (1, 2))
|
|
content((5, 2.5), $B$)
|
|
circle((5, 0), radius: (1, 2))
|
|
circle((5, 0), radius: (0.75, 1.25), stroke: none, fill: luma(80%))
|
|
|
|
circle((0, 1.5), stroke: 3pt, radius: 0.05)
|
|
circle((0, 0.75), stroke: 3pt, radius: 0.05)
|
|
circle((0, 0), stroke: 3pt, radius: 0.05)
|
|
circle((0, -0.75), stroke: 3pt, radius: 0.05)
|
|
circle((0, -1.5), stroke: 3pt, radius: 0.05)
|
|
circle((5, 1.5), stroke: 3pt, radius: 0.05)
|
|
circle((5, 0.75), stroke: 3pt, radius: 0.05)
|
|
circle((5, 0), stroke: 3pt, radius: 0.05)
|
|
circle((5, -0.75), stroke: 3pt, radius: 0.05)
|
|
circle((5, -1.5), stroke: 3pt, radius: 0.05)
|
|
|
|
bezier((0, 1.5), (5, 0.75), (3, 1.5), (2, 0.75), mark: (end: ">"))
|
|
line((0, 0), (5, 0), mark: (end: ">"))
|
|
line((0, 0.75), (5, 0.75), mark: (end: ">"))
|
|
bezier((0, -0.75), (5, 0), (3, -0.75), (2, 0), mark: (end: ">"))
|
|
bezier((0, -1.5), (5, -0.75), (3, -1.5), (2, -0.75), mark: (end: ">"))
|
|
|
|
line((6.25, 0), (5.5, 0), stroke: luma(80%))
|
|
content((7, 0), text($imOf(f)$, fill: luma(50%)))
|
|
}), caption: [Image of a function])
|
|
|
|
Correspondingly, the image of a group homomorphism is defined to be the image of the corresponding function.
|
|
|
|
== Modules
|
|
|
|
== Grading
|
|
|
|
== Exactness
|
|
|
|
#definition("Exactness")[
|
|
Two functions $isTyp(f, arro(A, B))$ and $isTyp(g, arro(B, C))$ are *exact* if the image of $f$ is isomorphic to the kernel of $g$.
|
|
$ eqv(imOf(f), kerOf(g)) $
|
|
] <exactness>
|
|
|
|
= Algebraic topology
|
|
|
|
== Basic spaces
|
|
|
|
== CW complexes
|
|
|
|
== Eilenberg-MacLane spaces
|
|
|
|
Eilenberg-MacLane spaces were defined in homotopy type theory by #cite(<licata_eilenberg-maclane_2014>, form: "author") @licata_eilenberg-maclane_2014.
|
|
|
|
#agdaCubicalLink("Cubical.Homotopy.EilenbergMacLane.Base")
|
|
|
|
== Fibers
|
|
|
|
#definition("Fiber")[
|
|
Given some map between spaces $f : A -> B$, and some point $b : B$, the *fiber* of $f$ at $b$ consists of all the points in $A$ that $f$ maps to $b$.
|
|
In other words, it can be considered the set $f^(-1)(b)$.
|
|
|
|
In homotopy type theory, we define:
|
|
|
|
$ sans("fiber")_f (b) = sum_(a : A) (f(a) equiv b) $
|
|
]
|
|
|
|
A *pointed fiber* of a pointed map between #link(<pointedType>)[pointed types] has the distinguished basepoint $(a_0, f_0)$, where $a_0$ is the basepoint of $A$, and $f_0$ is the proof that $f(a_0) equiv b_0$.
|
|
|
|
== Fibration
|
|
|
|
<fibration>
|
|
A fibration is a map $p : E -> B$ that has a certain homotopy lifting property:
|
|
|
|
It turns out that in homotopy type theory, all type families are fibrations. TODO: Why?
|
|
|
|
We write $F arrow.r.hook X -> B$ to denote that $F$ is the fiber, $X$ is the total space, and $B$ is the base space.
|
|
|
|
#example[
|
|
The first projection is a fibration: $sans("pr")_1 : A times B -> A$.
|
|
The total space is $A times B$, and the base space is $A$.
|
|
The fiber in this case is $A$.
|
|
This is trivial because the total space is exactly the product of the fiber space and the base space.
|
|
]
|
|
|
|
#example("Hopf fibration")[
|
|
There exists a fibration $S^1 arrow.r.hook S^3 ->^p S^2$, where $S^n$ denotes the unit $n$-dimensional sphere given by points in $RR^(n+1)$.
|
|
This means $S^3$ can be decomposed into fibers of $S^1$ over the base space of $S^2$.
|
|
|
|
We will revisit the Hopf fibration later.
|
|
]
|
|
|
|
A Serre fibration is a map that satisfies the lifting property for all CW complexes, while a Hurewicz fibration is a map that satisfies the lifting property for _all_ spaces, making it a superset of the set of Serre fibrations.
|
|
|
|
== Homology and cohomology
|
|
|
|
Homology groups, like homotopy groups, are roughly an algebraic encoding of the holes in a topological space, such that spaces that are homotopic to each other will have the same group.
|
|
This reduces the study of spaces down to the study of more familiar algebraic structures such as groups and rings.
|
|
|
|
However, unlike calculating homotopy groups (which can be done by taking the truncation of iterated loopspaces), homology isn't a single definition; rather, it is an abstraction of different techniques to arrive at the same homology groups.
|
|
These different techniques all satisfy the basic axioms for homology, known as the Eilenberg-Steenrod axioms.
|
|
For example, simplicial homology, singular homology, and cellular homology are examples of ways to arrive at homology groups.
|
|
|
|
Taking singular homology as an example, we represent the homology groups as groups in a chain complex:
|
|
|
|
#align(center, diagram(cell-size: 10mm, $
|
|
dots.c edge(diff_3, ->) &
|
|
C_2 edge(diff_2, ->) &
|
|
C_1 edge(diff_1, ->) &
|
|
C_0 edge(diff_0, ->) &
|
|
0
|
|
$))
|
|
|
|
Cohomology is typically dualized by taking each group $C_n$ in the homological chain complex and taking $sans("Hom")(-, R)$ for some coefficient group $R$.
|
|
|
|
#align(center, diagram(cell-size: 10mm, $
|
|
dots.c edge(diff_3, <-) &
|
|
sans("Hom")(C_2, R) edge(diff_2, <-) &
|
|
sans("Hom")(C_1, R) edge(diff_1, <-) &
|
|
sans("Hom")(C_0, R) edge(diff_0, <-) &
|
|
0
|
|
$))
|
|
|
|
Like homology, cohomology also generalizes with the following axioms:
|
|
|
|
- *homotopy*
|
|
- *exactness*
|
|
- *excision*
|
|
- *additivity*
|
|
|
|
TODO: Contravariant functor definition
|
|
|
|
```
|
|
open import Cubical.Homotopy.EilenbergSteenrod
|
|
```
|
|
|
|
In later sections we will enrich our definition of cohomology to include parameterized cohomology as well as cohomology for spectra instead of just topological spaces.
|
|
|
|
== Chain complexes
|
|
|
|
#definition("Chain complex")[
|
|
A *chain complex* is a sequence of #link(<abelianGroup>)[abelian groups] $isTyp(C_n, AbGroup)$ ("chains") along with homomorphisms between consecutive groups $isTyp(d_n, hom(C_n, C_(n-1)))$ ("boundaries"), such that for any $n$, the proposition $propEq(homComp(d_(n-1), d_n), 0_(C_(n-2)))$ is inhabited.
|
|
|
|
(notation: $0_G$ is the identity element of the group $G$)
|
|
] <chainComplex>
|
|
|
|
Another way to word this is that for consecutive homomorphisms $d_n$ and $d_(n-1)$, the #link(<image>)[image] of $d_n$ is a subgroup of the kernel of $d_(n-1)$.
|
|
|
|
#definition("Exact sequence")[
|
|
An *exact sequence* is a chain complex where all consecutive homomorphisms are #link(<exactness>)[exact].
|
|
] <exactSequence>
|
|
|
|
== Long exact sequence of homotopy groups
|
|
|
|
== Spectra
|
|
|
|
Note: spectra and spectral sequences actually have nothing to do with each other.
|
|
TODO: Expand based on note: #quote(block: true, attribution: [nlab])[
|
|
Despite their name, there seemed to be nothing specifically “spectral” about spectral sequences, for any of the technical meanings of the word spectrum. Together with the concept, this term was introduced by Jean Leray and has long become standard, but was never really motivated (see p. 5 of Chow). But then, by lucky coincidence it turns out in the refined context of stable (∞,1)-category theory/stable homotopy theory that spectral sequences frequently arise by considering the homotopy groups of sequences of spectra.
|
|
]
|
|
|
|
== Spectral sequences
|
|
|
|
A spectral sequence is a series of 2-dimensional pages of abelian groups, along with differentials $d_r$ between those groups for each page $r$.
|
|
The differentials satisfy the condition that $partial^2 = 0$, making each group part of a long exact sequence.
|
|
|
|
#let stop_before(start, end, shorten, ..args) = {
|
|
import draw: *
|
|
// Extract x and y coordinates
|
|
let (x1, y1) = start
|
|
let (x2, y2) = end
|
|
let m = (y2 - y1) / (x2 - x1)
|
|
let ang = calc.atan2(x2 - x1, y2 - y1)
|
|
let sx = shorten * calc.cos(ang)
|
|
let sy = shorten * calc.sin(ang)
|
|
line((x1 + sx, y1 + sy), (x2 - sx, y2 - sy), ..args)
|
|
}
|
|
|
|
#figure(canvas({
|
|
import draw: *
|
|
set-style(stroke: 0.4pt)
|
|
grid((0, 0), (6.5, 4.5), step: 1, stroke: gray + 0.2pt)
|
|
line((-0.5, 0), (6.5, 0), mark: (end: "stealth"))
|
|
line((0, -0.5), (0, 4.5), mark: (end: "stealth"))
|
|
for x in (1, 2, 3, 4, 5, 6) {
|
|
for y in (1, 2, 3, 4) {
|
|
circle((x, y), fill: black, radius: 0.08)
|
|
if x < 5 {
|
|
stop_before((x, y), (x+2, y - 1), 0.15,
|
|
mark: (end: "straight"),
|
|
stroke: (paint: rgb("#ff9999"), thickness: 0.6pt)
|
|
)
|
|
}
|
|
}
|
|
}
|
|
}), caption: [Page $E_2$ of a spectral sequence])
|
|
|
|
A spectral sequence is a series of 2-dimensional pages of abelian groups, along with differentials (group homomorphisms) between those groups.
|
|
A group is denoted $E^(p,q)_r$, where $r$ gives the page of the spectral sequence, and $p, q : ZZ$ give the coordinates of the group in the page $r$.
|
|
In particular, for all $p, q < 0$, the groups are defined to be the zero group.
|
|
|
|
=== Convergence
|
|
|
|
After turning the page of a spectral sequence, the differentials go up and over by a different amount.
|
|
For some sufficiently large $r$, all of the nonzero groups in the first quadrant of the spectral sequence will only have differentials from and to groups outside the first quadrant.
|
|
We say that the differentials vanish beyond this point.
|
|
This page is also known as $E^(p,q)_infinity$.
|
|
|
|
Then, we can compute $H^n (X)$ (where $X$ is the total space) by reading off the diagonal of $E_infinity$ such that $p + q = n$.
|
|
|
|
#notation("Convergence")[
|
|
$ E^(p,q)_2 :equiv C^(p,q) arrow.r.double D^(p+q) $
|
|
|
|
means there exists a spectral sequence $E$ such that:
|
|
|
|
- $E^(p,q)_2 :equiv C^(p,q)$
|
|
- $E$ converges to $E_infinity$
|
|
- $D^(p+q)$ is built from $E^(p,q)_infinity$
|
|
]
|
|
|
|
TODO: Caveat about extension problems
|
|
|
|
= The Serre spectral sequence
|
|
|
|
There is a Serre spectral sequence for cohomology, and one for homology. We will first focus on the cohomology one.
|
|
|
|
#definition("Cohomological Serre spectral sequence")[
|
|
Given #link(<fibration>)[fibration] $F arrow.r.hook X -> B$, such that $B$ is path-connected, we define a spectral sequence by giving its initial (2nd) page:
|
|
|
|
$ E^(p,q)_2 :equiv H^p (B; H^q (F; ZZ)) $
|
|
|
|
TODO: Note about the choice of coefficient $ZZ$
|
|
] <serreSSCohom>
|
|
|
|
#theorem[
|
|
The spectral sequence defined in @serreSSCohom converges:
|
|
|
|
$ E^(p,q)_2 :equiv H^p (B; H^q (F; ZZ)) arrow.r.double H^(p+q) (E; ZZ) $
|
|
]
|
|
|
|
== Applications
|
|
|
|
= Conclusion
|
|
|
|
|
|
- #TODO[References @agda_developers_agda_2025 should probably have more info]
|
|
- #TODO[References @martin-lof_intuitionistic_1975 is this correct?] |