HOMOLOGY

Homology package contains basic theorems about general homology theory.

SETS

Definition (Proposition, Set). Type is a proposition if all elements of are equal. Type is a set if all paths between elements of are equal. $≔$ $≔$

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

(Monoid). Monoid is a set equipped with binary associative operation called multiplication and identity element satisfying .

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)

(Group). Group is a monoid with inversion satisfying .

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

(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

(Division). $≔$ $≔$

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)

(Conjugation). Let be a group, the conjugation of two elements of the group is defined as .

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

SUBGROUPS

(Predicate). Type family is a predicate iff is a mere proposition for all .

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

(Subtype). Let be a predicate. Then: $≔$

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

(Subgroup). Predicate is a subgroup iff 1) 2) and 3)

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

(Normal Subgroup). Subgroup is normal iff for every it contains conjugate of .

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

(Kernel of Homomorphism). $≔$

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

(Image of Homomorphism). $≔$

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)

(Kernel of Homomorphism is subgroup).

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

(Image of Homomorphism is subgroup).

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

(Set-Quotient). Assume some type and relation on it. We define as following Higher Inductive Type: $≔$

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 ]

(Factor Group). Let be a group and his normal subgroup. We define: $≔$ $≔$ We can also define by relation . If is normal subgroup then . 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)

(Factor group of dihedral group ). As an test of factor group correctness we prove that , where and , i. e. smallest nontrivial group.

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

(Trivial homomorphism). Trivial homomorphism between two groups (or monoids) and maps every element of to identity element of :

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

(Chain complex). Chain complex consists of: 1) Sequence of abelian groups . 2) Homomorphisms between these groups . 3) Requirement: the composition of two consecutive homomorphisms is trivial:

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

(Cycles). $≔$

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)

(Boundaries). $≔$

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

(Homology Group). $≔$

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

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

By composition of and we obtain a path . Therefore, contains every conjugation of

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