HOMOLOGY

Homology package contains basic theorems about general homology theory.

SETS

Definition (Proposition, Set). Type $A : \mathcal{U}$ is a proposition if all elements of $A$ are equal. Type $A : \mathcal{U}$ is a set if all paths between elements of $A$ are equal. $$isProp(A) ≔ \prod_{x, y : A} x = y$$ $$isSet(A) ≔ \prod_{x, y : A} \prod_{p, q : x = y} p = q$$

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). Monoid is a set $M$ equipped with binary associative operation $(x, y \mapsto x \cdot y) : M \rightarrow M \rightarrow M$ called multiplication and identity element $1$ satisfying $x \cdot 1 = 1 \cdot x = x$.

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). Group is a monoid with inversion $(x \mapsto x^{-1})$ satisfying $x^{-1} \cdot x = x \cdot x^{-1} = 1$.

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 (Division). $$x \backslash y ≔ x^{-1} \cdot y$$ $$x / y ≔ x \cdot y^{-1}$$

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)

Definition (Conjugation). Let $G$ be a group, the conjugation 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 = rdiv G ((opGroup G) g1 g2) g1

SUBGROUPS

Definition (Predicate). Type family $P : A \rightarrow \mathcal{U}$ is a predicate iff $P(x)$ is a mere proposition for all $x : A$. $$\forall (x : A), isProp(P(x))$$

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

Definition (Subtype). Let $P : A \rightarrow \mathcal{U}$ be a predicate. Then: $$\{ x \in A \mid P(x) \} ≔ \sum_{x : A} P(x)$$

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

Definition (Subgroup). Predicate $\phi : G \rightarrow \mathcal{U}$ is a subgroup iff 1) $1 \in \phi$ 2) $\forall (x : G), x \in \phi \implies x^{-1} \in \phi$ and 3) $\forall (x, y : G), x \in \phi \land y \in \phi \implies (x \cdot y) \in \phi$

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))

Definition (Normal Subgroup). Subgroup $\phi$ is normal iff for every $g \in \phi$ it contains conjugate of $g$.

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

Definition (Kernel of Homomorphism). $$\mathrm{Ker}(\phi) ≔ \{ x \in G \mid f(x) = 1 \}$$

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

Definition (Image of Homomorphism). $$\mathrm{Im}(\phi) ≔ \left\{ y \in H \middle| \left( \left\| \sum_{x : G} f(x) = y \right\| \right) \right\}$$

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)

Theorem (Kernel of Homomorphism is subgroup).

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

Theorem (Image of Homomorphism is subgroup).

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

Definition (Set-Quotient). Assume some type $A : \mathcal{U}$ and relation $R : A \rightarrow A \rightarrow \mathcal{U}$ on it. We define $\| A/R \|_0$ as following Higher Inductive Type: $$\| A/R \|_0 ≔ \begin{cases} f : A \rightarrow A/R \\ p : \prod_{a, b : A} \prod_{r : R(a, b)} f(a) = f(b) \\ q : \prod_{a, b : \| A/R \|_0} \prod_{p, q : a = b} p = q \end{cases}$$

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 ]

Definition (Factor Group). Let $G$ be a group and $\phi$ his normal subgroup. We define: $$\begin{cases} R : G \rightarrow G \rightarrow \mathcal{U} \\ R ≔ (x, y) \mapsto (x / y) \in \phi \end{cases}$$ $$G/\phi ≔ \| G/R \|_0$$ We can also define $G\backslash\phi$ by relation $(x, y) \mapsto (x \backslash y) \in \phi$. If $\phi$ is normal subgroup then $G/\phi \simeq G\backslash\phi$. This statement is proven in Lean.

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)

Theorem (Factor group of dihedral group $D_3$). As an test of factor group $G/\phi$ correctness we prove that $D_3/A_3 \cong Z_2$, where $A_3 = \{ R_0, R_1, R_2 \} \subset D_3$ and $Z_2 ≅ \mathbb{Z}/2\mathbb{Z}$, i. e. smallest nontrivial group.

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

Definition (Trivial homomorphism). Trivial homomorphism $0$ between two groups (or monoids) $G$ and $H$ maps every element of $G$ to identity element of $H$: $x \mapsto 1_H$

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))

Definition (Chain complex). Chain complex consists of: 1) Sequence of abelian groups $K_n$. 2) Homomorphisms between these groups $\delta_n : K_{n + 1} \rightarrow K_n$. 3) Requirement: the composition of two consecutive homomorphisms is trivial: $\delta_n \circ \delta_{n + 1} = 0$ $$\ldots \xrightarrow{\delta_{n+2}} K_{n+1} \xrightarrow{\delta_n} K_n \xrightarrow{\delta_{n - 1}} \ldots \xrightarrow{\delta_1} K_1 \xrightarrow{\delta_0} K_0$$

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)))

Definition (Cycles). $Z_n(X) ≔ \mathrm{Ker}(\delta_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)

Definition (Boundaries). $B_n(X) ≔ \mathrm{Im}(\delta_{n + 1})$

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))

Definition (Homology Group). $H_n(X) ≔ Z_n(X) / B_n(X)$

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

Theorem (First Group Isomorphism Theorem). Let $G$ and $H$ be groups, and let $\phi : G \rightarrow H$ be a homomorphism. Then: 1) The kernel of $\phi$ is normal subgroup of G. 2) The image of $\phi$ is a subgroup of $H$. 3) The image of $\phi$ is isomorphic to the quotient group $G/ker(\phi)$.

By composition of $phiUnfold$ and $conjOne$ we obtain a path $\phi (g_1 \cdot g_2 \cdot g_1^{-1}) = 1$. Therefore, $\phi$ contains every conjugation of $g_2$

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