COHOMOLOGY

Eilenberg-MacLane spaces are fundamental in unstable homotopy theory, characterized by a single non-trivial homotopy group for an abelian group and for . In Homotopy Type Theory (HoTT), they are defined as higher inductive types (HIT) and serve as classifying spaces for cohomology, with . Synthetic cohomology in HoTT leverages to define cohomology groups synthetically, enabling computational approaches in systems like Cubical Agda.

This page formalizes in HoTT, providing formation, introduction, elimination, computation, and uniqueness rules, along with theorems and applications in algebraic topology and orbifold cohomology.

Formation

(-Formation). For an abelian group and , the type is a type in , representing the Eilenberg-MacLane space with .

def K (G : AbGroup) (n : Nat) : U_{(0,0)}
(* Eilenberg-MacLane space type *)

Introduction

(-Introduction). Terms of are introduced via a higher inductive type (HIT) with a base point and loops corresponding to elements of in degree , truncated to ensure for .

HIT K (G : AbGroup) (n : Nat) :=
  | pt : K(G, n)
  | loop : G -> (pt =_{K(G, n)} pt)
  | trunc : is-n-type(K(G, n))
(* Constructors for K(G, n) *)

Elimination

(-Elimination). The eliminator maps terms of to an -type , preserving the homotopy group structure induced by .

def K_ind (G : AbGroup) (n : Nat)
          (B : U_{(0,0)}) (B_n_type : is-n-type(B))
          (b : B) (l : G -> (b =_B b))
          : K(G, n) -> B
(* Eliminator for K(G, n) *)

Computation

(-Computation). The eliminator computes on constructors as follows: the base point maps to , and loops map to paths in .

def K_comp (G : AbGroup) (n : Nat)
           (B : U_{(0,0)}) (B_n_type : is-n-type(B))
           (b : B) (l : G -> (b =_B b))
           : KInd(B, b, l, pt) ≡ b
           , KInd(B, b, l, loop(g)) ≡ l(g)
(* Computation rules *)

Uniqueness

(-Uniqueness). Any two eliminators for into an -type are homotopic, ensuring uniqueness up to homotopy.

def K_uniq (G : AbGroup) (n : Nat)
           (B : U_{(0,0)}) (B_n_type : is-n-type(B))
           (f g : Π (x : K(G, n)), B)
           (h_pt : f(pt) = g(pt))
           (h_loop : Π (g : G), f(loop(g)) = g(loop(g)))
           : f ~ g
(* Uniqueness rule *)

Theorems

(Cohomology Group). For a type , the -th cohomology group with coefficients in is the 0-truncation of the mapping space to .

def cohomology (X : U_{(0,0)}) (G : AbGroup) (n : Nat) : || X -> K(G, n) ||_0
(* Cohomology group *)

(Cohomology Ring). For , the cohomology groups form a graded ring, with cup product induced by the loop space structure of .

def cohomology_ring (X : U_{(0,0)}) (n m : Nat)
                    : H^n(X; ℤ) × H^m(X; ℤ) -> H^{n+m}(X; ℤ)
(* Cohomology ring structure *)

(Computational Cohomology). In Cubical Agda, cohomology groups for and or are computable using .

def computational_cohomology (k n : Nat) (G : {ℤ, ℤ/p}) : H^n(S^k; G)
(* Computable cohomology *)

Applications

Eilenberg-MacLane spaces and synthetic cohomology have wide applications: - : Computing cohomology groups and rings for spaces like tori and spheres, as shown in Cubical Agda implementations [2, 4, 5]. - : Defining proper orbifold cohomology using to capture group actions on manifolds [6]. - : Modeling gauge theories via cohomology classes, connecting to synthetic approaches in HoTT [1, 3].

Bibliography

[1]. Cavallo, E. (2015). Synthetic Cohomology in Homotopy Type Theory.
[2]. Ljungström, A., & Mörtberg, A. (2024). Computational Synthetic Cohomology Theory in Homotopy Type Theory.
[3]. Graham, R. (2018). Synthetic Homology in Homotopy Type Theory.
[4].Brunerie, G., Ljungström, A., & Mörtberg, A. Synthetic Cohomology Theory in Cubical Agda.
[5]. Lamiaux, T., Ljungström, A., & Mörtberg, A. (2022). Computing Cohomology Rings in Cubical Agda.
[6]. Sati, H., & Schreiber, U. Proper Orbifold Cohomology.
[7]. Domenico Fiorenza, Hisham Sati, Urs Schreiber. (2020). The character map in (twisted differential) non-abelian cohomology.