HOMOLOGY

$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapup#1{\Big\uparrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$

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

$$ \begin{array}{ccc} \phi (g_1 \cdot g_2 \cdot g_1^{-1}) & \mapright{phiUnfold} & \phi(g_1) \cdot \phi(g_2) \cdot (\phi (g_1))^{-1} \\ \mapup{} & & \mapup{} \\ \phi (g_1 \cdot g_2) \cdot \phi(g_1)^{-1} & \mapright{} & \phi(g_1) \cdot \phi(g_2) \cdot \phi (g_1)^{-1} \\ \end{array} $$

$$ \begin{array}{ccc} \phi(g_1) \cdot \phi(g_2) \cdot (\phi(g_1))^{-1} & \mapright{conjOne} & 1 \\ \mapup{} & & \mapup{} \\ \phi(g_1) \cdot 1 \cdot (\phi(g_1)^{-1}) & \mapright{} & \phi(g_1) \cdot \phi (g_1)^{-1} \\ \end{array} $$

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