Homology package contains basic theorems about general homology theory.


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)


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

(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


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


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

(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