# HOMOLOGY

Homology package contains basic theorems about general homology theory.

# SETS

Definition (Set).

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

Definition (Monoid).

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) 

Definition (Group).

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 

Definition (Differential Group).

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

Definition (Diff).

diff (H: group) (g h: H.1.1) : H.1.1 = (opGroup H) g ((invGroup H) h)

Definition (Conjugation). Let $G$ is a group, the conjucation of two elements of the group $x,y \in G$ is defined as $x y x^{-1}$.

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

# SUBGROUPS

Definition (Subtype).

subtypeProp (A: U): U = (P: A -> U) * (a: A) -> isProp (P a) subtype (A: U) (P: subtypeProp A): U = (x: A) * (P.1 x)

Definition (Subgroup).

subgroupProp (G: group): U = (prop: G.1.1 -> U) * (level: (x: G.1.1) -> isProp (prop x)) * (ident: prop (idGroup (G.1,G.2.1))) * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop (diff G g1 g2))

Definition (Normal Subgroup).

isNormal (G: group) (P: subgroupProp G) : U = (g1 g2: G.1.1) -> P.1 g2 -> P.1 (conjugate G g1 g2) normalSubgroupProp (G: group): U = (P: subgroupProp G) * isNormal G P subElProp (G: group) (H: subgroupProp G) : subtypeProp G.1.1 = (H.1,H.2.1) subEl (G: group) (H: subgroupProp G): U = subtype G.1.1 (subElProp G H)

# KERNEL and IMAGE

Definition (Kernel of Homomorphism).

ker_prop (G H: group) (phi: grouphom G H) : subgroupProp G = (prop,level,ident,inv,op,di) where prop (x: G.1.1): U = Path H.1.1 (phi.1 x) (idGroup H) ident: prop (idGroup G) = phi.2.2 level (x: G.1.1): isProp (prop x) = undefined inv: (x: G.1.1) -> prop x -> prop ((invGroup G) x) = undefined op: (g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2) = undefined di: (g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop (diff G g1 g2) = undefined Ker (G: abgroup) (H: group) (phi: grouphom (G.1,G.2.1) H): group = subgroup (G.1,G.2.1) (ker_prop (G.1,G.2.1) H phi)

Definition (Image of Homomorphism).

im_prop (G H: group) (phi: grouphom G H) : subgroupProp H = (prop,level,ident,inv,op,di) where prop (x: H.1.1): U = pTrunc (fiber G.1.1 H.1.1 phi.1 x) ident: prop (idGroup H) = inc ((idGroup G),<i>phi.2.2 @ -i) level (x: H.1.1): isProp (prop x) = pTruncIsProp (fiber G.1.1 H.1.1 phi.1 x) inv: (x: H.1.1) -> prop x -> prop ((invGroup H) x) = undefined op: (g1 g2: H.1.1) -> prop g1 -> prop g2 -> prop ((opGroup H) g1 g2) = undefined di: (h1 h2: H.1.1) -> prop h1 -> prop h2 -> prop (diff H h1 h2) = undefined Im (G: group) (H: abgroup) (psi: grouphom G (H.1,H.2.1)): group = subgroup (H.1,H.2.1) (im_prop G (H.1,H.2.1) psi)

Definition (Quotient).

KerImRel (G H: group) (phi: grouphom G H) (x y: H.1.1): U = pTrunc (fiber G.1.1 H.1.1 phi.1 (diff H x y)) KerImEl (G H: group) (phi: grouphom G H): U = quot H.1.1 (KerImRel G H phi)

Definition (Homology Group).

homology_group (x: ChainComplex): (n: Z) -> group

# COMPLEXES

Definition (Sequence).

mutual data Seq (A: U) (B: A -> A -> U) = seqNil (ob: A) | seqCons (ob: A) (seq: Seq A B) (hom: B ob (head A B seq)) head (A: U) (B: A -> A -> U): Seq A B -> A = split seqNil x -> x seqCons x y z -> x

Definition (Chain Complexes).

ChainComplex: U = (sequence: Seq abgroup abgrouphom) * (index: nat -> abgroup) * (augment: abgrouphom (index zero) (head abgroup abgrouphom sequence)) * ((n: nat) -> abgrouphom (index (succ n)) (index n)) CochainComplex: U = (sequence: Seq abgroup abgrouphom) * (index: nat -> abgroup) * (augment: abgrouphom (head abgroup abgrouphom sequence) (index zero)) * ((n: nat) -> abgrouphom (index n) (index (succ n)))

# AXIOMS

Definition (Homology). The map from a pair of topological spaces $A \subset X$ to an Abelian Groups, called homological groups $H_n(X,A)$ iff: i) Any map $f : (X,A) \rightarrow (Y,B)$ induces homomorphism $f_* : H_n(X,A) \rightarrow H_n(Y,B)$ such that $id_* = id : H_n(X,A) \rightarrow H_n(X,A)$, $(f \circ g)_* = f_* \circ g_*$ ii) There is unique homomorphism $\delta : H_n(X,A) \rightarrow H_{n-1}(A) = H_{n-1}(A,\varnothing)$ such that