# HOMOLOGY

Homology package contains basic theorems about general homology theory.

# SETS

**Definition** (Proposition, Set).
Type

```
n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where
rec (A: U) (a b: A) : (k: N) -> U
= split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n }
isProp (A: U): U = n_grpd A Z
isSet (A: U): U = n_grpd A (S Z)
```

# GROUPS

```
isMonoid (M: SET): U
= (op: M.1 -> M.1 -> M.1)
* (assoc: isAssociative M.1 op)
* (id: M.1)
* (hasIdentity M.1 op id)
ismonoidhom (a b: monoid) (f: a.1.1 -> b.1.1): U
= (_: preservesOp a.1.1 b.1.1 (opGroup a) (opGroup b) f)
* (preservesId a.1.1 b.1.1 (idGroup a) (idGroup b) f)
monoidhom (a b: monoid): U
= (f: a.1.1 -> b.1.1)
* (ismonoidhom a b f)
```

```
isGroup (G: SET): U
= (m: isMonoid G)
* (inv: G.1 -> G.1)
* (hasInverse G.1 m.1 m.2.2.1 inv)
opGroup (g: group): g.1.1 -> g.1.1 -> g.1.1
idGroup (g: group): g.1.1
invGroup (g: group): g.1.1 -> g.1.1
```

```
isDifferentialGroup (G: SET): U
= (g: isGroup G)
* (comm: isCommutative G.1 g.1.1)
* (boundary: G.1 -> G.1)
* ((x: G.1) -> Path G.1 (boundary (boundary x)) g.1.2.2.1)
dgroup: U = (X: SET) * isDifferentialGroup X
dgrouphom (a b: dgroup): U = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1)
unitDGroup: dgroup
```

```
ldiv (H: group) (g h: H.1.1) : H.1.1
= (opGroup H) ((invGroup H) g) h
rdiv (H: group) (g h: H.1.1) : H.1.1
= (opGroup H) g ((invGroup H) h)
```

```
conjugate (G: group) (g1 g2: G.1.1): G.1.1
= rdiv G ((opGroup G) g1 g2) g1
```

# SUBGROUPS

```
subtypeProp (A: U): U
= (P : A -> U)
* (a : A) -> isProp (P a)
```

```
subtype (A : U) (P : subtypeProp A): U
= (x : A) -- prop
* (P.1 x) -- level
```

```
subgroupProp (G: group): U
= (prop: G.1.1 -> U)
* (level: (x: G.1.1) -> isProp (prop x))
* (ident: prop (idGroup G))
* (inv: (g: G.1.1) -> prop g -> prop ((invGroup G) g))
* ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))
```

```
isNormal (G: group) (P: subgroupProp G) : U
= (X: group)
* (g1 g2: G.1.1) -> P.1 g2 -> P.1 (conjugate G g1 g2)
normalSubgroupProp (G: group): U
= (P: subgroupProp G)
* isNormal G P
```

# KERNEL and IMAGE

```
isGroupKer (G H: group) (f: G.1.1 -> H.1.1) (x: G.1.1): U
= Path H.1.1 (f x) (idGroup H)
```

```
isGroupIm (G H: group) (f: G.1.1 -> H.1.1) (g: H.1.1): U
= propTrunc (fiber G.1.1 H.1.1 f g)
```

```
kerProp (G H: group) (phi: grouphom G H)
: subgroupProp G
```

```
imProp (G H: group) (phi: grouphom G H)
: subgroupProp H
```

```
data setQuot (A: U) (R: A -> A -> U)
= quotient (a: A)
| identification (a b: A) (r: R a b)
<i>[ (i=0) -> quotient a, (i=1) -> quotient b ]
| trunc (a b : setQuot A R) (p q : Path (setQuot A R) a b)
<i j> [ (i = 0) -> p @ j , (i = 1) -> q @ j ,
(j = 0) -> a , (j = 1) -> b ]
```

```
factorProp (G : group) (P : normalSubgroupProp G) : G.1.1 -> G.1.1 -> U
= \(x y : G.1.1) -> P.1.1 (rdiv G x y)
factor (G : group) (P : normalSubgroupProp G) : U
= setQuot G.1.1 (factorProp G P)
```

`def D₃.iso : Z₂ ≅ D₃\A₃`

```
trivmonoidhom (a b : monoid) : monoidhom a b
= (\(x : a.1.1) -> idMonoid b,
\(x y : a.1.1) -> <i> (hasIdMonoid b).1 (idMonoid b) @ -i,
<_> idMonoid b)
trivabgrouphom (a b : abgroup) : abgrouphom a b
= trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))
```

```
chainComplex : U
= (K : nat -> abgroup)
* (hom : (n : nat) -> abgrouphom (K (succ n)) (K n))
* ((n : nat) -> Path (abgrouphom (K (succ2 n)) (K n))
(abgrouphomcomp (K (succ2 n)) (K (succ n)) (K n) (hom (succ n)) (hom n))
(trivabgrouphom (K (succ2 n)) (K n)))
```

```
propZ (C : chainComplex) (n : nat) : subgroupProp (K' C (succ n))
= kerProp (K' C (succ n)) (K' C n) (hom C n)
Z (C : chainComplex) (n : nat) : group = subgroup (K' C (succ n)) (propZ C n)
```

```
B (C : chainComplex) (n : nat) : normalSubgroupProp (Z C n)
= abelianSubgroupIsNormal (abelianSubgroupIsAbelian (K C (succ n)) (propZ C n))
(subgroupSubgroup (K' C (succ n))
(imProp (K' C (succ (succ n))) (K' C (succ n)) (hom C (succ n))) (propZ C n))
```

`H (C : chainComplex) (n : nat) : group = factorGroup (Z C n) (B C n)`

By composition of

```
kernelIsNormalSubgroup (G H : group) (phi : grouphom G H)
: normalSubgroupProp G
```