(*****************************************************************************) (* Homology Groups *) (*****************************************************************************) Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop. Require Import finfun tuple ssralg matrix mxalgebra zmodp vector rank. Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. (***************************************************************************** Definition of homology groups: Let V1, V2 and V3 be vector spaces over a field K and f: V1 -> V2, g: V2 -> V3 be linear maps such that gf = 0 then the homology group of (f,g), denoted by H_(f,g) is the quotient ker(g)/im(f). *****************************************************************************) Section HomologyDefinition. Variable (K : fieldType) (V1 V2 V3 : vectType K) (f : linearApp V1 V2) (g :linearApp V2 V3). Definition Homology := ((lker g) :\: (limg f))%VS. Section HomologyDefinitionProperties. Lemma img_f_subset_ker_g: (g \o f = \0)%VS -> ((limg f) <= (lker g))%VS. Proof. by move => nilpotency; rewrite -lkerE limgE -limg_comp nilpotency lim0g. Qed. End HomologyDefinitionProperties. Section HomologyDimension. Definition dimHomology := vdim V2 - \dim (limg g) - \dim (limg f). Lemma addn_equal_subn: forall (m n p : nat), m+n= p -> m = p - n. Proof. move=> m n p H. have H1: m+n - n = p -n. by rewrite H. by rewrite -H1 addnK. Qed. Lemma dim_lker_limg_homology: \dim ((lker g) :\: (limg f)) = \dim (lker g) - \dim ((lker g) :&: (limg f)). Proof. have H: \dim ((lker g) :\: (limg f)) + \dim ((lker g) :&: (limg f))= \dim (lker g). by rewrite addnC dimv_cap_compl. by apply addn_equal_subn. Qed. Lemma dim_ker_intersection_im: (g \o f = \0)%VS -> \dim ((lker g) :&: (limg f)) = \dim (limg f). Proof. by move => nilpotency; move : (img_f_subset_ker_g nilpotency); rewrite capvKr; move/eqP => ->. Qed. Lemma dim_ker : \dim (lker g) = vdim V2 - \dim (limg g). Proof. have : \dim ((fullv V2) :&: lker g) + \dim (g @: (fullv V2)) = \dim (fullv V2). by rewrite limg_ker_dim. have H1 : \dim (fullv V2 :&: lker g) = \dim (lker g). by move : (subvf (lker g)); rewrite capvKr; move/eqP => ->. have H2 : \dim (g @: fullv V2) = \dim (limg g). by rewrite limgE. by rewrite H1 H2 dimvf => H; apply addn_equal_subn. Qed. Lemma dimHomologyE: (g \o f = \0)%VS -> dimHomology = \dim Homology. Proof. move => nilpotency. by rewrite /Homology dim_lker_limg_homology dim_ker dim_ker_intersection_im /dimHomology. Qed. End HomologyDimension. End HomologyDefinition. Section HomologyRank. Variable (K : fieldType) (v1 v2 v3:nat). Definition V1 := (matrixVectType K 1 v1). Definition V2 := (matrixVectType K 1 v2). Definition V3 := (matrixVectType K 1 v3). Variable (mxf: 'M[K]_(vdim V1,vdim V2)) (mxg : 'M[K]_(vdim V2,vdim V3)). Definition dimHomologyrank := v2 - \rank mxg - \rank mxf. Lemma vdimV2: vdim V2 = v2. Proof. by rewrite /V2 /vdim /= mul1n. Qed. Lemma cancelmx_of_lapp : forall (V W : vectType K) (mx: 'M[K]_(vdim V,vdim W)), mx_of_lapp (LinearApp mx) = mx. Proof. by move => mx; rewrite /mx_of_lapp. Qed. Lemma dimHomologyrank_dimHomology: dimHomologyrank = (dimHomology (LinearApp mxf) (LinearApp mxg)). Proof. by rewrite /dimHomology vdimV2 /limg !cancelmx_of_lapp /dimv !mx2vsK /dimHomologyrank. Qed. Lemma dimHomologyrankE: (mulmx mxf mxg) = 0%R -> dimHomologyrank = \dim (Homology (LinearApp mxf) (LinearApp mxg)). Proof. move => nilpotency_mx; rewrite -dimHomologyE. by rewrite /dimHomology vdimV2 /limg !cancelmx_of_lapp /dimv !mx2vsK /dimHomologyrank. by rewrite /comp_lapp !cancelmx_of_lapp nilpotency_mx. Qed. End HomologyRank. Section Ex_Homology. Variable (K : fieldType) (v1 v2 v3:nat). Hypothesis v1_0 : v1 > 0. Hypothesis v2_0 : v2 > 0. Hypothesis v3_0 : v3 > 0. Definition W1 := (matrixVectType K 1 v1). Definition W2 := (matrixVectType K 1 v2). Definition W3 := (matrixVectType K 1 v3). Variable (ex_mxf: Matrix K) (ex_mxg : Matrix K). Hypothesis Mokf: Mok ex_mxf v1 v2. Hypothesis Mokg: Mok ex_mxg v2 v3. Definition ex_dimHomology := v2 - (ex_Rank v2 ex_mxg) - (ex_Rank v1 ex_mxf). Lemma vdimW2: vdim W2 = v2. Proof. by rewrite /W2 /vdim /= mul1n. Qed. Lemma vdimW1: vdim W1 = v1. Proof. by rewrite /W1 /vdim /= mul1n. Qed. Lemma vdimW3: vdim W3 = v3. Proof. by rewrite /W3 /vdim /= mul1n. Qed. Lemma Sv1: exists x, 1+x = v1. Proof. by exists (v1-1); rewrite addnC subnK. Qed. Lemma Sv2: exists x, 1+x = v2. Proof. by exists (v2-1); rewrite addnC subnK. Qed. Lemma Sv3: exists x, 1+x = v3. Proof. by exists (v3-1); rewrite addnC subnK. Qed. Lemma ex_dimHomology_dimHomologyrank: ex_dimHomology = (dimHomologyrank (Matrix2mat (vdim W1) (vdim W2) ex_mxf) (Matrix2mat (vdim W2) (vdim W3) ex_mxg)). Proof. rewrite /dimHomologyrank -!rankRank !vdimW1 !vdimW2 !vdimW3. move : Sv1 => [x1 H1]; move : Sv2 => [x2 H2]; move : Sv3 => [x3 H3]. rewrite -H1 -H2 -H3 -!ex_Rank_ok !m2m_ok2; last first. by rewrite H2 H3. by rewrite H1 H2. by rewrite /ex_dimHomology -H2 -H1. Qed. Local Open Scope ring_scope. Fixpoint exnullmx (m n:nat) : Matrix K := if m is (S p) then let zp := (zeroes K p) in if n is (S q) then let zq := (zeroes K q) in cM 0 zq zp (exnullmx p q) else (eM K) (* m is 0 *) else (eM K). (* n is 0 *) Lemma Matrix2mat_zero : forall m n, Matrix2mat m n (exnullmx m n) = (0:'M[K]_(m,n)). Proof. elim => [| m hm]; elim => [ | n hi] //=. rewrite seq2rV_zeroes seq2cV_zeroes hm //=. have -> : 0%:M = 0 :> 'M[K]_1 by apply/matrixP => i j; rewrite !mxE GRing.mul0rn. by rewrite /block_mx !row_mx0 col_mx0. Qed. Lemma exnullmx_ok : forall m n, Mok (exnullmx m n) m n. Proof. elim => [ | m hi] [ | n] //=. by rewrite !size_nseq (hi n) !eqxx. Qed. Lemma ex_dimHomologyE: (mult ex_mxf ex_mxg) = (exnullmx (vdim W1) (vdim W3)) -> ex_dimHomology = \dim (Homology (LinearApp (Matrix2mat (vdim W1) (vdim W2) ex_mxf)) (LinearApp (Matrix2mat (vdim W2) (vdim W3) ex_mxg))). Proof. move => nilpotency_mx; rewrite ex_dimHomology_dimHomologyrank dimHomologyrankE //=. move : nilpotency_mx. rewrite -{1}(m2m_ok2 Mokf) -{1}(m2m_ok2 Mokg) !vdimW1 !vdimW2 !vdimW3. move : Sv1 => [x1 H1]; move : Sv2 => [x2 H2]; move : Sv3 => [x3 H3]. rewrite -H1 -H2 -H3 -multE. move => H. have H4 : (Matrix2mat (1 + x1) (1 + x2) ex_mxf *m Matrix2mat (1 + x2) (1 + x3) ex_mxg) = (Matrix2mat (1 + x1) (1 + x3) (exnullmx (1 + x1) (1 + x3))). by rewrite -H m2m_ok. by rewrite H4 Matrix2mat_zero. Qed. End Ex_Homology. (* Some examples *) Definition F2 := Fp_fieldType 2. Notation "n %:F2" := (n%R : 'F_2) (at level 2, left associativity, format "n %:F2"). (* The first example comes from a filled triangle *) Definition d0_ex1 := (@eM F2). Definition d1_ex1 := cM 1%:F2 [:: 1%:F2 ; 0%:F2] [:: 1%:F2 ; 0%:F2] (cM 0%:F2 [:: 1%:F2] [:: 1%:F2] (cM 1%:F2 [::] [::] (@eM _ ))). Definition d2_ex1 := cM 1%:F2 [::] [:: 1%:F2 ; 1%:F2] (@eM _ ). Definition H0_ex1 := (ex_dimHomology 0 3 d0_ex1 d1_ex1). Definition H1_ex1 := (ex_dimHomology 3 3 d1_ex1 d2_ex1). Eval vm_compute in H0_ex1. (* 1 connected component *) Eval vm_compute in H1_ex1. (* 0 holes *) (* The second example comes from a triangle attached to an empty triangle *) Definition d0_ex2 := (@eM F2). Definition d1_ex2 := cM 1%:F2 [:: 1%:F2 ; 0%:F2; 0%:F2; 0%:F2] [:: 1%:F2 ; 0%:F2; 0%:F2] (cM 0%:F2 [:: 1%:F2; 1%:F2; 0%:F2] [:: 1%:F2; 0%:F2] (cM 1%:F2 [:: 0%:F2; 1%:F2] [:: 0%:F2] (cM 1%:F2 [:: 1%:F2] [::] (@eM _ )))). Definition d2_ex2 := cM 1%:F2 [::] [:: 1%:F2 ; 1%:F2; 0%:F2; 0%:F2] (@eM _ ). Definition H0_ex2 := (ex_dimHomology 0 4 d0_ex2 d1_ex2). Definition H1_ex2 := (ex_dimHomology 4 5 d1_ex2 d2_ex2). Eval vm_compute in H0_ex2. (* 1 connected component *) Eval vm_compute in H1_ex2. (* 1 hole *) (* This example comes from an empty triangle *) Definition d0_ex3 := (@eM F2). Definition d1_ex3 := cM 1%:F2 [:: 1%:F2 ; 0%:F2] [:: 1%:F2 ; 0%:F2] (cM 0%:F2 [:: 1%:F2] [:: 1%:F2] (cM 1%:F2 [::] [::] (@eM _ ))). Definition d2_ex3 := (@eM F2). Definition H0_ex3 := (ex_dimHomology 0 3 d0_ex3 d1_ex3). Definition H1_ex3 := (ex_dimHomology 3 3 d1_ex3 d2_ex3). Eval vm_compute in H0_ex3. (* 1 connected component *) Eval vm_compute in H1_ex3. (* 1 hole *)