(* We want to prove that the product of two consecutive incidence matrices *) (* of a simplicial complex is equal to the null matrix. *) Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype. Require Import finfun bigop finset ssralg perm zmodp matrix. Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Lemma cardsD: forall (T:finType) (A B:{set T}), B \subset A -> #|A:\:B| = #|A| - #|B|. Proof. move=> T A B H. by rewrite -(cardsID B A) (setIidPr H) -{2}(addn0 #|B|) subn_add2l subn0. Qed. Section simplicial_complexes. (* V is the vertex set *) Variable V : finType. (* A simplex over V is a finite subset of V *) Definition simplex := {set V}. Definition face_op (S : simplex) (x : V) := S :\ x. Definition boundary (S : simplex) := (face_op S) @: S. Lemma face_op_inj: forall (S : simplex), {in S, injective (face_op S)}. Proof. move=> S x Hx y HB. have Hbx: #|S :\: (face_op S x)| == 1. rewrite cardsD ; last exact: subD1set. by rewrite (cardsD1 x) -(add0n #|_ :\ _|) Hx subn_add2r. case/cards1P:Hbx => t Ht. have Hx2: x \in (S :\: (face_op S x)). by rewrite /face_op !inE eqxx Hx. case Hy: (y \in S) ; last first. rewrite /face_op in HB. move:(ltnSn #|S :\ x|) ; move:(cardsD1 y S). rewrite (cardsD1 x) HB Hx Hy add1n add0n => Habs. by rewrite -{1}Habs ltnn. have Hy2: y \in (S :\: (face_op S y)). by rewrite /face_op !inE eqxx Hy. by rewrite -HB Ht !in_set1 in Hx2 Hy2 ; rewrite (eqP Hx2) (eqP Hy2). Qed. Lemma face_op_inj2: forall (S : simplex), {in S &, injective (face_op S)}. Proof. by move=> S x y Hx _ ; exact: (face_op_inj Hx). Qed. Lemma boundaryP: forall (S : simplex) (B : simplex), reflect (B \subset S /\ #|S| = #|B|.+1) (B \in boundary S). Proof. move=> S B ; apply:introP => H. case/imsetP: H => x Hx HB. split ; first by rewrite HB ; exact:subD1set. by rewrite (cardsD1 x) Hx add1n HB. case=> H_sub H_card. have: B \in boundary S ; last by rewrite (negbTE H). apply/imsetP ; case:(pickP [pred x \in (S :\: B)]) => [x Hx | H0]. rewrite !inE in Hx ; case/andP:Hx => Hx1 Hx2. exists x => // ; apply/setP ; apply:subset_cardP. by apply/eqP ; rewrite -eqSS -H_card (cardsD1 x) Hx2 add1n. apply/subsetP => y Hy ; rewrite !inE (subsetP H_sub _ Hy) andbT. case Heq: (y == x) => // ; by rewrite -(eqP Heq) Hy in Hx1. by move:(cardsD H_sub) ; rewrite H_card subSnn (eq_card H0) card0. Qed. (* Simplicial complex definifition *) Definition simplicial_complex (c : {set simplex}) := forall x, x \in c -> forall y : simplex, y \subset x -> y \in c. Definition powerset (x : simplex) : {set simplex} := setT ::&: x. Lemma powersetE : forall (x : simplex) (y : simplex), y \in powerset x -> y \subset x. Proof. rewrite /powerset. rewrite /ssetI; move => x y. rewrite [y \in _]inE. by move/andP => [_]. Qed. Lemma in_powerset : forall (x y : simplex), y \subset x -> y \in powerset x. Proof. move => x y xy; rewrite inE. rewrite xy andbT. by []. Qed. (* utiliser bigcup_sup *) Definition create_sc (s : {set simplex}) : {set simplex} := \bigcup_(sp \in s) powerset sp. Lemma create_sc_correct : forall s, simplicial_complex (create_sc s). move => s x xc y yx. rewrite /create_sc. apply/bigcupP. move: xc. rewrite /create_sc. move/bigcupP => [si sis xsi]. exists si; first by []. apply: in_powerset. apply: subset_trans yx _. by apply: powersetE. Qed. Definition facet (c : {set simplex}) (x : simplex) := [set y : simplex | (x \subset y) && (y \in c)] == [set x]. Definition facets (c : {set simplex}) := [set x : simplex | facet c x] : {set simplex}. (* Definition of the incidence matrix of two enumerated finite sets of *) (* simplices *) Section incidence_matrix. Open Local Scope ring_scope. (* Top and Left are two enumerated finite sets of simplices *) Variables Left Top:{set simplex}. (* x0 is the trivial simplex *) Definition x0 := set0 : simplex. (* We are going to work with coefficients in the ring Z2 *) (* From the incidence function we can define the incidence matrix *) Definition incidenceMatrix := \matrix_(i < #|Left|, j < #|Top|) if enum_val i \in boundary (enum_val j) then 1 else 0:'F_2. End incidence_matrix. Section nth_incidence_mx. (* We are going to define the incidence matrix of the set of simplices c *) (* in dimension n using the above definition *) Variable c: {set simplex}. Variable n:nat. (* The Top set is the set of n-simplices of c and the Left set is the *) (* set of (n-1)-simplices of c *) Definition n_1_simplices := [set x \in c | #|x|==n] : {set simplex}. Definition n_simplices := [set x \in c | #|x|==n.+1] : {set simplex}. (* Using the incidenceMatrix function we define the incidence matrix of *) (* the set of simplices c in dimension n *) Definition incidence_mx_n := incidenceMatrix n_1_simplices n_simplices. End nth_incidence_mx. End simplicial_complexes. (* Statement of the theorem *) Open Local Scope ring_scope. Lemma incidence_matrices_sc_product: forall (V:finType) (n:nat) (sc: {set (simplex V)}), simplicial_complex sc -> (incidence_mx_n sc n) *m (incidence_mx_n sc (n.+1)) = 0. Proof. move => V n sc gsc ; apply/matrixP => i j ; rewrite !mxE. pose P := pickP [pred x \in (n_simplices sc n)]. case: P => [x0|H] ; [rewrite inE|] ; last first. rewrite big1 // => k _ ; move:(eq_card H) ; rewrite card0=> Heq. by case:(cast_ord Heq k). move=> Hx0 ; rewrite (reindex_onto (enum_rank_in Hx0) enum_val) ; last first. by move=> x _ ; exact:enum_valK_in. rewrite (bigID (mem (boundary (enum_val j)))) Monoid.mulmC big1 /= ; last first. move=> X ; case/andP ; rewrite !mxE ; move/eqP => -> H. by rewrite (negbTE H) GRing.mulr0. pose F X := if enum_val i \in boundary X then 1 else 0:'F_2. rewrite (eq_big (mem (boundary (enum_val j))) F) /F; last first. move=> X; rewrite !mxE ; case/andP. by move/eqP => -> -> ; rewrite GRing.mulr1. have HB: {subset boundary (enum_val j) <= (n_simplices sc n)} => [x Hx|X]. rewrite inE ; case/boundaryP: Hx => Hx_sub Hx_card. move: (enum_valP j) ; rewrite inE ; case/andP => Hj. by rewrite (gsc (enum_val j) Hj _ Hx_sub) Hx_card eqSS => ->. rewrite !inE /= ; case H: (X \in _) ; last exact: andbF. by move/eqP:(enum_rankK_in Hx0 (HB _ H)) => ->. rewrite big_imset ; last exact:face_op_inj2. rewrite (bigID (mem (enum_val i))) big1 ; last first. move=> x ; case/andP=> _ H ; case:ifPn=> //=. by case/imsetP=> y _ Heq; rewrite Heq !inE eqxx andbF in H. move:(enum_valP i) (enum_valP j); rewrite !inE. case/andP => _ ; move/eqP=> Hi ; case/andP => _ ; move/eqP=> Hj. case Hij: (enum_val i \subset enum_val j) ; last first. rewrite big1 => [|x] ; first exact:val_inj. case/andP => _ _ ; case:ifPn => //= ; case/boundaryP => H _. by rewrite (subset_trans H (subD1set _ _)) in Hij. rewrite (eq_bigr (fun _ => 1)) ; last first. move=> x ; case/andP => H1 H2. suff: (enum_val i \in boundary (face_op (enum_val j) x)) => [->|] //. apply/boundaryP ; split ; [apply/subsetP=> y Hy; rewrite !inE|apply/eqP]. by rewrite ((subsetP Hij) y Hy); move:Hy H2; case:(y==x)/eqP => //= -> ->. by move:(cardsD1 x (enum_val j)) ; rewrite H1 Hi Hj addnC addn1 -eqSS => <-. rewrite big_const (@eq_card _ _ [pred x \in (enum_val j :\: enum_val i)]). rewrite (cardsD Hij) Hi Hj -(addn1 n) -!addnS -{2}(addn0 n) (subn_add2l n 2 0). exact:val_inj. by move=> x; rewrite !inE andbC. Qed. Lemma incidence_matrices_sc_product_facets: forall (V:finType) (n:nat) (ss: {set (simplex V)}), n >= 1 -> mulmx (incidence_mx_n (create_sc (facets ss)) n) (incidence_mx_n (create_sc (facets ss)) (n.+1)) = 0%R. Proof. move => V n ss n0. rewrite incidence_matrices_sc_product => //. apply: create_sc_correct. Qed.