(***** we define H^1 in an intuitionistic type-theory setting; we show the first stage of the long exact sequence, saying that H^1 being trivial gives surjectivity of a map on a space of sections ***) (**** Carlos Simpson CNRS, Universit\'e de Nice-Sophia Antipolis carlos@math.unice.fr *******************************************) Implicit Arguments On. Implicits exT [1]. Implicits ex [1]. Definition mark := [X:Type; x:X]x. Theorem plug : (a,b: Type; h:a-> b; u,v : a)(u == v) -> (h u) == (h v). Intros. Rewrite H. Trivial. Save. Inductive JMeqT [A: Type; a:A] : (B: Type; b:B) Prop := JMeqT_refl : (JMeqT a a). Infix 9 "-=-" JMeqT. Axiom JMeqT_eqT : (A:Type; a,b: A)(a -=- b) -> (a == b). Theorem eqT_JMeqT : (A:Type; a,b: A)(a == b) -> (a -=- b). Intros. Rewrite H. EApply JMeqT_refl. Save. Parameter eqT_rect : (A,B:Type) (A == B) -> A -> B. Axiom eqT_rect_JMeqT : (A,B: Type; hyp : A == B; a:A)((eqT_rect hyp a) -=- a). Axiom proof_irrelevance : (P : Prop; p,q: P)(p == q). Axiom extensionality : (x:Type; f:x-> Type; u,v: (y:x)(f y)) ((y:x)(u y) == (v y)) -> u == v. Definition type_of := [T:Type; t:T]T. Theorem eqT_utility : (X:Type; P : (a,b:X; hyp: a == b)Prop) (a,b:X; hyp : a == b) (P a a (refl_eqT ? a)) -> (P a b hyp). Intros. Generalize hyp. NewInduction hyp. Intros. Assert (refl_eqT X a)==hyp. EApply proof_irrelevance. Rewrite <- H0. Assumption. Save. Inductive nonempty [T:Type]:Prop := nonempty_intro : T -> (nonempty T). Record has_one_element [T:Type]:Prop := { one_nonempty : (nonempty T); one_unique : (a,b:T)a == b }. Inductive ONE : Type := pt : ONE. Theorem ONE_has_one_element : (has_one_element ONE). EApply Build_has_one_element. EApply nonempty_intro. Exact pt. Intros. NewInduction a; NewInduction b. Trivial. Save. Record virtual [X:Type]:Type := { carrier : Type; virt_touch :> carrier -> X; virt_nonempty : (nonempty carrier); virt_equal : (v,w:carrier)(virt_touch v) == (virt_touch w) }. Definition virtualize : (X:Type)X -> (virtual X). Intros. EApply (!Build_virtual X ONE [u:ONE]X0). EApply (nonempty_intro pt). Intros. Trivial. Defined. Record description [X:Type]:Type := { the_description :> (virtual X) -> X; description_eq : (v:(virtual X); x:(carrier v))(the_description v) == (v x) }. Definition use_description : (X:Type; de: (description X); Y:Type; t: Y -> X; ne : (nonempty Y); e : (y,z:Y)(t y) == (t z))X. Intros. LetTac V:=(!Build_virtual X Y t ne e). Exact (de V). Defined. Theorem use_description_eq: (X:Type; de: (description X); Y:Type; t: Y -> X; ne : (nonempty Y); e : (y,z:Y)(t y) == (t z); y:Y) (use_description de ne e) == (t y). Intros. Unfold use_description. LetTac V:=(Build_virtual ne e). LetTac K:=(!description_eq X de V y). Rewrite K. Trivial. Save. (********** quotients ***********) Definition TypeQ := Type. Parameter quotient : (r,x:Type; p1,p2: r->x)Type. Definition quotient_fix_universe : (r,x:TypeQ; p1,p2: r->x)TypeQ := quotient. (*Implicits quotient [1 2].*) Parameter quotient_map : (r,x:Type; p1,p2: r->x)x->(quotient p1 p2). (*Implicits quotient_map [1 2].*) Axiom quotient_eq: (r,x:Type; p1,p2: r->x) (w:r)(quotient_map p1 p2 (p1 w)) == (quotient_map p1 p2 (p2 w)). Parameter quotient_fact : (r,x:Type; p1,p2: r->x) (y:Type; g:x-> y; hyp : ((w:r)(g (p1 w)) == (g (p2 w))))(quotient p1 p2)-> y. (*Implicits quotient_fact [1 2].*) Parameter quotient_recT : (r,x:Type; p1,p2: r->x) (g:x-> Type; hyp : ((w:r)(g (p1 w)) == (g (p2 w))))(quotient p1 p2)-> Type. Parameter quotient_rect : (r,x: Type; p1,p2 : r -> x) (g:x->Type; hyp : (w:r)((g (p1 w)) == (g (p2 w))); s: (a:x)(g a); hyp1 : (w:r)((s (p1 w)) -=- (s (p2 w))) ) (q:(quotient p1 p2))(quotient_recT hyp q). Axiom quotient_fact_comp : (r,x:Type; p1,p2: r->x) (y:Type; g:x->y; hyp : ((w:r)(g (p1 w)) == (g (p2 w))); a:x) (quotient_fact hyp (quotient_map p1 p2 a)) == (g a). Implicits exT [1]. Axiom quotient_surj: (r,x:Type; p1,p2: r->x) (b:(quotient p1 p2))(exT [a:x]((quotient_map p1 p2 a) == b)). (**** we might have to repeat the above for other universe levels *****) Inductive R_gen_by [r,x: Type; p1,p2: r->x]: x->x-> Prop := R_gen_by_i1 : (w:r)(R_gen_by p1 p2 (p1 w) (p2 w)) | R_gen_by_i2 : (w:r)(R_gen_by p1 p2 (p2 w) (p1 w)) | R_gen_by_refl : (a:x)(R_gen_by p1 p2 a a) | R_gen_by_trans : (a,b,c: x)(R_gen_by p1 p2 a b) -> (R_gen_by p1 p2 b c) -> (R_gen_by p1 p2 a c). Record is_equivalence_relation [x:Type; R : x -> x -> Prop]: Prop :={ reln_refl : (a:x)(R a a); reln_symm : (a,b: x)(R a b) -> (R b a); reln_trans : (a,b,c: x)(R a b) -> (R b c) -> (R a c) }. Theorem R_gen_by_er : (r,x:Type; p1,p2 : r-> x) (is_equivalence_relation (R_gen_by p1 p2)). Intros. EApply (!Build_is_equivalence_relation x (R_gen_by p1 p2)). Intros. EApply R_gen_by_refl. Intros. NewInduction H. EApply R_gen_by_i2. EApply R_gen_by_i1. EApply R_gen_by_refl. EApply R_gen_by_trans with b. Assumption. Assumption. Intros. EApply R_gen_by_trans with b. Assumption. Assumption. Defined. Theorem R_gen_by_minimal : (r,x:Type; p1,p2: r -> x; R: x -> x -> Prop; eR : (is_equivalence_relation R); hyp : (w:r)(R (p1 w) (p2 w)); a,b: x)(R_gen_by p1 p2 a b) -> (R a b). Intros. NewInduction H. EApply hyp. EApply reln_symm. Exact eR. EApply hyp. EApply reln_refl. EApply eR. EApply reln_trans with x b. Assumption. Assumption. Assumption. Save. Axiom quotient_inj : (r,x: Type; p1,p2: r->x; a,b:x) ((quotient_map p1 p2 a) == (quotient_map p1 p2 b))-> (R_gen_by p1 p2 a b). Theorem quotient_R_eq : (r,x:Type; p1,p2: r->x; a,b:x) (R_gen_by p1 p2 a b) -> (quotient_map p1 p2 a) == (quotient_map p1 p2 b). Intros. NewInduction H. EApply quotient_eq. Symmetry. EApply quotient_eq. Trivial. Transitivity (quotient_map p1 p2 b). Assumption. Assumption. Save. (******* groups *************) Record group : Type := { the_group :> Type; op : the_group -> the_group -> the_group; id : the_group; inv : the_group -> the_group; left_id : (x:the_group)(op id x) == x; right_id : (x:the_group)(op x id) == x; assoc : (x,y,z:the_group)(op (op x y) z) == (op x (op y z)); left_inv: (x:the_group)(op (inv x) x) == id; right_inv : (x:the_group)(op x (inv x)) == id }. Theorem id_left_char : (G:group; x,y:G)(op x y) == y -> x == (id G). Intros. LetTac h:=(inv y). Assert (op y h)==(id G). Unfold h. EApply right_inv. Rewrite <- H0. Rewrite <- H. Transitivity (op x (op y h)). Rewrite H0. Symmetry. EApply right_id. Symmetry. EApply assoc. Save. Theorem id_right_char : (G:group; x,y:G)(op x y) == x -> y == (id G). Intros. LetTac z:=(inv x). Assert (id G)==(op z x). Unfold z. Symmetry. EApply left_inv. Rewrite H0. Rewrite <- H. Transitivity (op (op z x) y). Rewrite <- H0. Symmetry. EApply left_id. EApply assoc. Save. Theorem inv_left_char : (G:group; x,y:G)(op x y) == (id G) -> x == (inv y). Intros. Assert (op (id G) (inv y))==(inv y). EApply left_id. Rewrite <- H0. Rewrite <- H. Transitivity (op x (op y (inv y))). Assert (op y (inv y))==(id G). EApply right_inv. Rewrite H1. Symmetry. EApply right_id. Symmetry. EApply assoc. Save. Theorem inv_right_char : (G:group; x,y:G)(op x y) == (id G) -> y == (inv x). Intros. Transitivity (inv (inv y)). EApply inv_left_char. EApply right_inv. Assert (inv y)==x. Symmetry. EApply inv_left_char. Assumption. Rewrite H0. Trivial. Save. Hint Rewrite [assoc] in assoc_right. Hint Rewrite <- [assoc] in assoc_left. Theorem unop_left : (G:group; x,y,z: G)y == z -> (op x y) == (op x z). Intros. Rewrite H. Trivial. Save. Theorem unop_right : (G:group; x,y,z: G)y == z -> (op y x) == (op z x). Intros. Rewrite H. Trivial. Save. Theorem multiply_left : (G:group; x,y,z:G)(op x y) == (op x z) -> y == z. Intros. Assert (op (inv x) x)==(id G). EApply left_inv. Assert y==(op (inv x) (op x y)). AutoRewrite [ assoc_left ]. Rewrite H0. Symmetry. EApply left_id. Assert z==(op (inv x) (op x z)). AutoRewrite [ assoc_left ]. Rewrite H0. Symmetry. EApply left_id. Rewrite H1. Rewrite H2. EApply unop_left. Assumption. Save. Theorem multiply_right : (G:group; x,y,z:G)(op y x) == (op z x) -> y == z. Intros. Assert (op x (inv x))==(id G). EApply right_inv. Assert y==(op (op y x) (inv x)). AutoRewrite [ assoc_right ]. Rewrite H0. Symmetry. EApply right_id. Assert z==(op (op z x) (inv x)). AutoRewrite [ assoc_right ]. Rewrite H0. Symmetry. EApply right_id. Rewrite H1. Rewrite H2. EApply unop_right. Assumption. Save. Theorem switch : (G:group; x,y: G)(op x y) == (id G) -> (op y x) == (id G). Intros. EApply multiply_right with (inv x). Rewrite left_id. AutoRewrite [ assoc_right ]. Rewrite right_inv. Rewrite right_id. EApply multiply_left with x. Rewrite right_inv. Assumption. Save. Theorem inv_op : (G:group; x,y: G)(inv (op x y)) == (op (inv y) (inv x)). Intros. Symmetry. EApply inv_left_char. AutoRewrite [ assoc_left ]. EApply switch. AutoRewrite [ assoc_right ]. Rewrite left_inv. Rewrite right_id. Apply right_inv. Save. Hint Rewrite [inv_op] in inv_in. Theorem inv_inv : (G:group; x:G)(inv (inv x)) == x. Intros. Symmetry. EApply inv_left_char. EApply right_inv. Save. Record gmap [A,B:group]:Type := { the_gmap :>A -> B; gmap_op : (x,y:A)(op (the_gmap x) (the_gmap y)) == (the_gmap (op x y)) }. Hint Rewrite <- [gmap_op] in gmap_in. Theorem gmap_extens : (A,B: group; f,g:(gmap A B)) ((x:A)(f x) == (g x)) -> f == g. Intros. Assert (the_gmap f)==(the_gmap g). EApply (!extensionality A [x:A]B). Assumption. NewInduction f. NewInduction g. Assert the_gmap0==the_gmap1. Assumption. NewInduction H1. Assert gmap_op0==gmap_op1. EApply proof_irrelevance. Rewrite H1. Trivial. Save. Theorem gmap_id : (A,B:group; f:(gmap A B))(f (id A)) == (id B). Intros. EApply id_left_char with (f (id A)). Transitivity (f (op (id A) (id A))). EApply gmap_op. LetTac x:=(op (id A) (id A)). Assert x==(id A). Unfold x. EApply left_id. Rewrite H. Trivial. Save. Theorem gmap_inv : (A,B:group; f:(gmap A B); x:A)(f (inv x)) == (inv (f x)). Intros. EApply inv_left_char. Transitivity (f (op (inv x) x)). EApply gmap_op. Assert (op (inv x) x)==(id A). EApply left_inv. Rewrite H. EApply gmap_id. Save. Definition gmap_comp : (A,B,C:group)(gmap B C) -> (gmap A B) -> (gmap A C). Intros A B C f g. EApply (!Build_gmap A C [x:A](f (g x))). Intros. Transitivity (f (op (g x) (g y))). EApply gmap_op. Assert (op (g x) (g y))==(g (op x y)). EApply gmap_op. Rewrite H. Trivial. Defined. Theorem gmap_comp_eq : (A,B,C:group; f: (gmap B C); g: (gmap A B); x:A) (gmap_comp f g x) == (f (g x)). Intros. Trivial. Save. Section onecohomology_def. Variable G : group. Record onecocycle : Type := { substrate : Type; cdiff :> substrate -> substrate -> G; substrate_nonempty : (nonempty substrate); cocycle_rule : (x,y,z:substrate)(op (cdiff y z) (cdiff x y)) == (cdiff x z) }. Record onecoboundary [alpha, beta : onecocycle] : Type := { bdiff :> (substrate alpha) -> (substrate beta) -> G; cobound_left : (x,y: (substrate alpha); z : (substrate beta)) (op (bdiff y z) (alpha x y)) == (bdiff x z); cobound_right : (x: (substrate alpha); y,z: (substrate beta)) (op (beta y z) (bdiff x y))== (bdiff x z) }. Lemma onecocycle_extens : (alpha, beta : onecocycle) (substrate alpha) == (substrate beta) -> ((x,y: (substrate alpha); x', y' : (substrate beta))(x -=- x') -> (y -=- y') -> (alpha x y) == (beta x' y')) -> alpha == beta. Intros. NewInduction alpha. NewInduction beta. Assert substrate0==substrate1. Exact H. NewInduction H1. LetTac alpha:=(Build_onecocycle substrate_nonempty0 cocycle_rule0). LetTac beta:=(Build_onecocycle substrate_nonempty1 cocycle_rule1). Assert cdiff0==cdiff1. EApply (!extensionality substrate0 [x:substrate0](type_of (cdiff0 x))). Intros. EApply (!extensionality substrate0 [z:substrate0](type_of (cdiff0 y z))). Intros. Change (alpha y y0)==(beta y y0) . EApply H0. EApply JMeqT_refl. EApply JMeqT_refl. NewInduction H1. Assert cocycle_rule0==cocycle_rule1. EApply proof_irrelevance. Assert substrate_nonempty0 == substrate_nonempty1. EApply proof_irrelevance. NewInduction H1. NewInduction H2. Trivial. Save. Lemma onecoboundary_extens : (alpha, beta : onecocycle; f,g: (onecoboundary alpha beta)) ((x: (substrate alpha); y: (substrate beta))(f x y) == (g x y)) -> f == g. Intros. NewInduction f. NewInduction g. Assert bdiff0==bdiff1. EApply (!extensionality (substrate alpha) [y:(substrate alpha)](type_of (bdiff0 y))). Intros. EApply (!extensionality (substrate beta) [z:(substrate beta)](type_of (bdiff0 y z))). Intros. EApply H. NewInduction H0. Assert cobound_left0==cobound_left1. EApply proof_irrelevance. Assert cobound_right0==cobound_right1. EApply proof_irrelevance. Rewrite H0. Rewrite H1. Trivial. Save. Section onecob_descrip. Variables alpha, beta : onecocycle. Variable de : (description G). Variable v : (virtual (onecoboundary alpha beta)). Section onecob_descripA. Variable x : (substrate alpha). Variable y : (substrate beta). Definition virt_bdiff : (virtual G). Apply (!Build_virtual G (carrier v) [c:(carrier v)](v c x y)). Apply virt_nonempty. Intros. Assert (v v0) == (v w). Apply virt_equal. Rewrite H. Trivial. Defined. Remark rmk1 : (c: (carrier v); d: (carrier virt_bdiff)) (virt_bdiff d) == (v c x y). Change (c,d: (carrier v))(virt_bdiff d) == (v c x y). Intros. Assert (virt_bdiff d) == (virt_bdiff c). EApply virt_equal. Rewrite H. Trivial. Save. Definition real_bdiff : G. Exact (de virt_bdiff). Defined. Remark rmk2 : (c: (carrier v))real_bdiff == (v c x y). Intros. Transitivity (virt_bdiff c). Unfold real_bdiff. EApply description_eq. EApply rmk1. Save. End onecob_descripA. Definition onecob_the_descrip : (onecoboundary alpha beta). EApply (!Build_onecoboundary alpha beta real_bdiff). Intros. Assert (nonempty (carrier v)). EApply virt_nonempty. NewInduction H. Assert (real_bdiff y z) == (v X y z). EApply onecob_descripA.rmk2. Assert (real_bdiff x z) == (v X x z). EApply onecob_descripA.rmk2. Rewrite H. Rewrite H0. EApply cobound_left. Intros. Assert (nonempty (carrier v)). EApply virt_nonempty. NewInduction H. Assert (real_bdiff x z) == (v X x z). EApply onecob_descripA.rmk2. Assert (real_bdiff x y) == (v X x y). EApply onecob_descripA.rmk2. Rewrite H. Rewrite H0. EApply cobound_right. Defined. Remark rmk3: (c:(carrier v))onecob_the_descrip == (v c). Intros. EApply onecoboundary_extens. Intros. Change (real_bdiff x y) == (v c x y). EApply onecob_descripA.rmk2. Save. End onecob_descrip. Definition onecoboundary_description : (alpha, beta : onecocycle) (description G) -> (description (onecoboundary alpha beta)). Intros. EApply (!Build_description (onecoboundary alpha beta) (!onecob_the_descrip alpha beta X)). Intros. EApply onecob_descrip.rmk3. Defined. Definition onecoboundary_cocycle : (alpha, beta, gamma : onecocycle) (onecoboundary beta gamma) -> (onecoboundary alpha beta) -> (onecoboundary alpha gamma) -> Prop. Intros alpha beta gamma f g h. Exact (x:(substrate alpha); y: (substrate beta); z: (substrate gamma)) (op (f y z) (g x y)) == (h x z). Defined. Record onecoboundary_trans [alpha, beta, gamma : onecocycle; f: (onecoboundary beta gamma); g: (onecoboundary alpha beta)] : Type := { onecob_trans : (onecoboundary alpha gamma); onecob_trans_cocycle : (onecoboundary_cocycle f g onecob_trans) }. Theorem onecoboundary_trans_exists : (alpha, beta, gamma : onecocycle; f:(onecoboundary beta gamma); g: (onecoboundary alpha beta)) (ExT [h: (onecoboundary alpha gamma)](onecoboundary_cocycle f g h)). Intros. Assert (nonempty (substrate beta)). EApply substrate_nonempty. NewInduction H. LetTac B:=[x:(substrate alpha); z:(substrate gamma)](op (f X z) (g x X)). Assert B_left : (u,v:(substrate alpha); w:(substrate gamma)) (op (B v w) (alpha u v))==(B u w). Intros. Unfold B. Transitivity (op (f X w) (op (g v X) (alpha u v))). EApply assoc. Assert (op (g v X) (alpha u v))==(g u X). EApply cobound_left. Rewrite H. Trivial. Assert B_right : (u:(substrate alpha); v,w:(substrate gamma)) (op (gamma v w) (B u v))==(B u w). Intros. Unfold B. Transitivity (op (op (gamma v w) (f X v)) (g u X)). Symmetry. EApply assoc. Assert (op (gamma v w) (f X v))==(f X w). EApply cobound_right. Rewrite H. Trivial. LetTac Bb:=(!Build_onecoboundary alpha gamma B B_left B_right). EApply exT_intro with Bb. Unfold onecoboundary_cocycle. Intros. Unfold Bb. Transitivity (op (f X z) (g x X)). Assert (f y z)==(op (f X z) (beta y X)). Symmetry. EApply cobound_left. Rewrite H. Assert (g x y)==(op (beta X y) (g x X)). Symmetry. EApply cobound_right. Rewrite H0. Transitivity (op (f X z) (op (beta y X) (op (beta X y) (g x X)))). EApply assoc. Assert (op (beta y X) (op (beta X y) (g x X)))==(g x X). Transitivity (op (op (beta y X) (beta X y)) (g x X)). Symmetry. EApply assoc. Assert (op (beta y X) (beta X y))==(beta X X). EApply cocycle_rule. Rewrite H1. EApply cobound_right. Rewrite H1. Trivial. Trivial. Save. Theorem onecoboundary_trans_unique: (alpha, beta, gamma : onecocycle; f:(onecoboundary beta gamma); g: (onecoboundary alpha beta); h,h': (onecoboundary alpha gamma)) (onecoboundary_cocycle f g h) -> (onecoboundary_cocycle f g h') -> h == h'. Intros. EApply onecoboundary_extens. Intros. Assert (nonempty (substrate beta)). EApply substrate_nonempty. NewInduction H1. Transitivity (op (f X y) (g x X)). Symmetry. EApply H. EApply H0. Save. Definition onecoboundary_symm : (alpha, beta : onecocycle; f: (onecoboundary alpha beta)) (onecoboundary beta alpha). Intros. EApply (!Build_onecoboundary beta alpha [x:(substrate beta); y:(substrate alpha)](inv (f y x))). Intros. EApply inv_right_char. Transitivity (op (op (f z x) (inv (f z y))) (beta x y)). Symmetry. EApply assoc. Assert (op (f z x) (inv (f z y)))==(beta y x). Transitivity (op (beta y x) (op (f z y) (inv (f z y)))). Assert (op (f z y) (inv (f z y)))==(id ?). EApply right_inv. Transitivity (op (op (beta y x) (f z y)) (inv (f z y))). Assert (f z x)==(op (beta y x) (f z y)). Symmetry. EApply cobound_right. Rewrite H0. Trivial. EApply assoc. Assert (op (f z y) (inv (f z y)))==(id G). EApply right_inv. Rewrite H. EApply right_id. Rewrite H. Transitivity (beta x x). EApply cocycle_rule. EApply id_left_char with (beta x x). EApply cocycle_rule. Intros. EApply inv_left_char. Transitivity (op (alpha y z) (op (inv (f y x)) (f z x))). EApply assoc. Assert (op (inv (f y x)) (f z x))==(alpha z y). Transitivity (op (inv (f y x)) (op (f y x) (alpha z y))). Assert (f z x)==(op (f y x) (alpha z y)). Symmetry. EApply cobound_left. Rewrite H. Trivial. Transitivity (op (op (inv (f y x)) (f y x)) (alpha z y)). Symmetry. EApply assoc. Assert (op (inv (f y x)) (f y x))==(id G). EApply left_inv. Rewrite H. EApply left_id. Rewrite H. Transitivity (alpha z z). EApply cocycle_rule. EApply id_left_char with (alpha z z). EApply cocycle_rule. Defined. Theorem onecoboundary_trans_one_elt : (alpha, beta, gamma : (onecocycle); f: (onecoboundary beta gamma); g: (onecoboundary alpha beta))(has_one_element (onecoboundary_trans f g)). Intros. EApply Build_has_one_element. LetTac K:=(onecoboundary_trans_exists f g). NewInduction K. EApply nonempty_intro. EApply (Build_onecoboundary_trans 4!f 5!g 6!x). Assumption. Intros. NewInduction a. NewInduction b. Assert onecob_trans0==onecob_trans1. EApply onecoboundary_trans_unique with beta f g. Assumption. Assumption. NewInduction H. Assert onecob_trans_cocycle0==onecob_trans_cocycle1. EApply proof_irrelevance. Rewrite H. Trivial. Save. Section onecoboundary_trans_touch_def. Variables alpha, beta, gamma : (onecocycle). Variable f: (onecoboundary beta gamma). Variable g: (onecoboundary alpha beta). Variable de : (description G). Local V : (virtual (onecoboundary alpha gamma)). EApply (!Build_virtual (onecoboundary alpha gamma) (onecoboundary_trans f g) [u : (onecoboundary_trans f g)](onecob_trans u)). EApply one_nonempty. EApply onecoboundary_trans_one_elt. Intros. Assert v==w. EApply one_unique. EApply onecoboundary_trans_one_elt. Rewrite H. Trivial. Defined. Remark rmk1: (c:(carrier V); h : (onecoboundary_trans f g)) (V c) == (onecob_trans h). Intros. Change (onecob_trans c)==(onecob_trans h) . Assert h==c. EApply one_unique. EApply onecoboundary_trans_one_elt. Rewrite H. Trivial. Save. Local h : (onecoboundary alpha gamma). Assert (description (onecoboundary alpha gamma)). EApply onecoboundary_description. Assumption. Exact (X V). Defined. Definition onecoboundary_trans_touch : (onecoboundary_trans f g). EApply (!Build_onecoboundary_trans alpha beta gamma f g h). Assert (nonempty (onecoboundary_trans f g)). EApply one_nonempty. EApply onecoboundary_trans_one_elt. NewInduction H. Assert (c:(carrier V))(V c)==h. Unfold h. Intros. Symmetry. EApply description_eq. Assert (V X)==h. EApply H. Assert (V X)==(onecob_trans X). EApply rmk1. Rewrite <- H0. Rewrite H1. EApply onecob_trans_cocycle. Defined. End onecoboundary_trans_touch_def. Definition onecoboundary_refl : (alpha : onecocycle) (onecoboundary alpha alpha). Intros. EApply (!Build_onecoboundary alpha alpha [x,y:(substrate alpha)](alpha x y)). Intros. EApply cocycle_rule. Intros. EApply cocycle_rule. Defined. End onecohomology_def. Section onecohomology_functoriality. Variables F,G: group. Variable f : (gmap F G). Definition onecocycle_funct : (onecocycle F) -> (onecocycle G). Intro a. NewInduction a. EApply (!Build_onecocycle G substrate0 [x,y:substrate0](f (cdiff0 x y))). Assumption. Intros. Transitivity (f (op (cdiff0 y z) (cdiff0 x y))). EApply gmap_op. Rewrite cocycle_rule0. Trivial. Defined. Definition onecoboundary_funct : (alpha, beta : (onecocycle F)) (onecoboundary alpha beta) -> (onecoboundary (onecocycle_funct alpha) (onecocycle_funct beta)). Intros. LetTac a:= alpha. LetTac b := beta. LetTac A:=(onecocycle_funct a). LetTac B:=(onecocycle_funct b). NewInduction alpha. NewInduction beta. NewInduction X. EApply (!Build_onecoboundary G A B [x:(substrate A); y:(substrate B)](f (bdiff0 x y))). Intros. Assert (A x y)==(f (a x y)). Trivial. Rewrite H. Transitivity (f (op (bdiff0 y z) (a x y))). EApply gmap_op. Assert (op (bdiff0 y z) (a x y))==(bdiff0 x z). EApply cobound_left0. Rewrite H0. Trivial. Intros. Assert (B y z)==(f (b y z)). Trivial. Rewrite H. Transitivity (f (op (b y z) (bdiff0 x y))). EApply gmap_op. Rewrite cobound_right0. Trivial. Defined. End onecohomology_functoriality. Section change_substrate_def. Variable G: group. Variable alpha : (onecocycle G). Variable U: Type. Variable s: U -> (substrate alpha). Hypothesis ne : (nonempty U). Definition change_substrate : (onecocycle G). EApply (!Build_onecocycle G U [x,y:U](alpha (s x) (s y))). Assumption. Intros. EApply cocycle_rule. Defined. Theorem change_substrate_eq : (x,y:U)(change_substrate x y) == (alpha (s x) (s y)). Intros. Trivial. Save. Definition change_substrate_cob : (onecoboundary alpha change_substrate). EApply (!Build_onecoboundary G alpha change_substrate [x:(substrate alpha); y: U](alpha x (s y))). Intros. EApply cocycle_rule. Intros. Rewrite change_substrate_eq. EApply cocycle_rule. Defined. End change_substrate_def. Section onecohomology_X_def. Variable X : Type. Section h1_X_G. Variable G : X -> group. Definition c1 := (x:X)(onecocycle (G x)). Record b1 : Type := { b1_a : c1; b1_b : c1; b1_bound : (x:X)(onecoboundary (b1_a x) (b1_b x)) }. Definition h1 := (quotient b1_a b1_b). Definition h1_fix_universe := (!Build_group h1). Definition h1_class : c1 -> h1. Intros. Unfold h1. EApply quotient_map. Assumption. Defined. Theorem h1_class_surj : (u:h1)(exT [a : c1](h1_class a) == u). Unfold h1. Unfold h1_class. Intro. EApply quotient_surj. Save. Theorem h1_class_inj1: (a,b: c1)(h1_class a) == (h1_class b) -> (R_gen_by b1_a b1_b a b). Unfold h1. Unfold h1_class. Intros. EApply quotient_inj. Assumption. Save. (*** now we refine the statement of h1_class_inj using the hypothesis de *****) Variable de : (x:X)(description (G x)). Definition b1R := [a,b: c1](nonempty (x:X)(onecoboundary (a x) (b x))). Theorem b1R_er : (is_equivalence_relation b1R). EApply Build_is_equivalence_relation. Intros. Unfold b1R. EApply nonempty_intro. Intros. EApply onecoboundary_refl. Intros a b. Unfold b1R. Intro. NewInduction H. EApply nonempty_intro. Intros. EApply onecoboundary_symm. Exact (X0 x). Intros. Unfold b1R. Unfold b1R in H. Unfold b1R in H0. NewInduction H. NewInduction H0. LetTac U:=[x:X](onecoboundary_trans (X1 x) (X0 x)). Assert (nonempty (x:X)(U x)). EApply nonempty_intro. Intro. Unfold U. EApply onecoboundary_trans_touch. EApply de. NewInduction H. EApply nonempty_intro. Intros. LetTac T:=(X2 x). Exact (onecob_trans T). Save. Theorem b1_b1R : (a,b: c1)(R_gen_by b1_a b1_b a b) -> (b1R a b). Intros. EApply R_gen_by_minimal with b1 c1 b1_a b1_b. EApply b1R_er. Intros. NewInduction w. Change (b1R b1_a0 b1_b0) . Unfold b1R. EApply nonempty_intro. Assumption. Assumption. Save. Theorem b1R_b1 : (a,b: c1)(b1R a b) -> (R_gen_by b1_a b1_b a b). Intros. Unfold b1R in H. NewInduction H. LetTac U:=(Build_b1 X0). Exact (R_gen_by_i1 b1_a b1_b U). Save. Theorem h1_class_inj2: (a,b: c1)(h1_class a) == (h1_class b) -> (b1R a b). Intros. EApply b1_b1R. EApply h1_class_inj1. Assumption. Save. Theorem h1_class_inj : (a,b: c1)(h1_class a) == (h1_class b) -> (nonempty (x:X)(onecoboundary (a x) (b x))). Exact h1_class_inj2. Save. Theorem h1_class_eq : (a,b: c1)(nonempty (x:X) (onecoboundary (a x) (b x))) -> (h1_class a) == (h1_class b). Unfold h1. Unfold h1_class. Intros. EApply quotient_R_eq. EApply b1R_b1. Exact H. Save. Definition h1_fact : (Y : Type; f: c1 -> Y)((a,b: c1; u : (x:X)(onecoboundary (a x) (b x)))(f a) == (f b)) -> h1 -> Y. Intros. EApply quotient_fact with b1 c1 b1_a b1_b f. Intros. NewInduction w. Change (f b1_a0)==(f b1_b0) . EApply H. Assumption. Exact X0. Defined. Theorem h1_fact_eq : (Y : Type; f: c1 -> Y; hyp : (a,b: c1; u : (x:X)(onecoboundary (a x) (b x)))(f a) == (f b); u: c1)(h1_fact hyp (h1_class u)) == (f u). Intros. Unfold h1. Unfold h1_fact. Unfold h1_class. EApply quotient_fact_comp. Save. End h1_X_G. Section h1_funct_def. Variables F,G: X -> group. Variable f: (x:X)(gmap (F x) (G x)). Definition c1_funct : (c1 F) -> (c1 G). Intros. Unfold c1. Intros. EApply onecocycle_funct with (F x). EApply f. EApply X0. Defined. Definition h1_funct : (h1 F) -> (h1 G). Intro u. EApply h1_fact with F [a:(c1 F)](h1_class (c1_funct a)). Intros. EApply h1_class_eq. EApply nonempty_intro. Intros. Unfold c1_funct. EApply onecoboundary_funct. EApply u0. Assumption. Defined. End h1_funct_def. End onecohomology_X_def. Definition TypeL := Type. Definition typeL_type_of_substrates := [G:group; U:TypeL] (!Build_onecocycle G U). Section exact_sequence_properties. Variables A,B,C: group. Variable f: (gmap A B). Variable g : (gmap B C). Hypothesis surj : (c:C)(exT [b:B](g b) == c). Hypothesis inj : (a1, a2 : A)(f a1) == (f a2) -> a1 == a2. Hypothesis comp : (a:A)(g (f a)) == (id C). Variable exact : (b:B; hyp : (g b) == (id C))A. Hypothesis exact_eq : (b:B; hyp : (g b) == (id C))(f (exact hyp)) == b. Definition exact_diff : (c:C; b,b': B; hyp : (g b) ==c; hyp' : (g b') == c)A. Intros. EApply exact with (op b' (inv b)). Transitivity (op (g b') (g (inv b))). Symmetry. EApply gmap_op. Rewrite hyp'. Assert (g (inv b))==(inv (g b)). EApply inv_left_char. Transitivity (g (op (inv b) b)). EApply gmap_op. Assert (op (inv b) b)==(id B). EApply left_inv. Rewrite H. EApply gmap_id. Rewrite H. Rewrite hyp. EApply right_inv. Defined. Theorem exact_diff_eq : (c:C; b,b': B; hyp : (g b) ==c; hyp' : (g b') == c) (f (exact_diff hyp hyp')) == (op b' (inv b)). Intros. Unfold exact_diff. EApply exact_eq. Save. (*** by the way we show that with (description A) we can get exact ****) Section exact_from_description_def. Variable de : (description A). Hypothesis exact_ext : (b:B)((g b) == (id C)) -> (exT [a:A](f a) == b). Variable b:B. Hypothesis hyp : (g b) == (id C). Remark rmk1 : (exT [a:A](f a) == b). Exact (exact_ext hyp). Save. Record efd_carrier : Type := { the_efd :> A; efd_eq : (f the_efd) == b }. Remark rmk2 : (has_one_element efd_carrier). EApply Build_has_one_element. LetTac K:=rmk1. NewInduction K. EApply nonempty_intro. Exact (Build_efd_carrier H). Intros. NewInduction a. NewInduction b0. Assert the_efd0==the_efd1. EApply inj. Rewrite efd_eq0. Symmetry. Assumption. NewInduction H. Assert efd_eq0==efd_eq1. EApply proof_irrelevance. Rewrite H. Trivial. Save. Local V : (virtual A). EApply (!Build_virtual A efd_carrier the_efd). EApply one_nonempty. EApply rmk2. Intros. Assert v==w. EApply one_unique. EApply rmk2. Rewrite H. Trivial. Defined. Definition exact_from_description : A. Exact (de V). Defined. Theorem exact_from_description_eq : (f exact_from_description) == b. Assert (nonempty (carrier V)). EApply one_nonempty. Exact rmk2. NewInduction H. Assert exact_from_description==(V X). Unfold exact_from_description. EApply description_eq. Rewrite H. Change (f X)==b . EApply efd_eq. Save. End exact_from_description_def. Record connecter [c:C; alpha : (onecocycle A)] : Type := { connecter_diff:> (b:B; hyp : (g b) == c; x : (substrate alpha))A; connecter_left : (b,b':B; hyp : (g b) == c; hyp' : (g b') == c; x:(substrate alpha)) (op (connecter_diff b' hyp' x) (exact_diff hyp hyp')) == (connecter_diff b hyp x); connecter_right : (b:B;hyp : (g b) == c; x,y:(substrate alpha)) (op (alpha x y) (connecter_diff b hyp x)) == (connecter_diff b hyp y) }. Theorem connecter_both : (c:C; alpha :(onecocycle A); d: (connecter c alpha); b,b' : B; hyp : (g b) == c; hyp' : (g b') == c; x,x' : (substrate alpha)) (op (op (alpha x x') (d b hyp x)) (exact_diff hyp' hyp)) == (d b' hyp' x'). Intros. Transitivity (op (alpha x x') (d b' hyp' x)). AutoRewrite [ assoc_right ]. EApply unop_left. EApply connecter_left. EApply connecter_right. Save. Theorem connecter_extens: (c:C; alpha: (onecocycle A); e,e': (connecter c alpha)) ((b:B; hyp : (g b) == c; x:(substrate alpha))(e b hyp x) == (e' b hyp x)) -> e == e'. Intros. NewInduction e. NewInduction e'. Assert (b:B; hyp:((g b)==c); x:(substrate alpha)) (connecter_diff0 b hyp x)==(connecter_diff1 b hyp x). Exact H. Assert connecter_diff0==connecter_diff1. EApply (!extensionality B [b:B](type_of (connecter_diff0 b))). Intros. EApply (!extensionality (g y)==c [u:((g y)==c)](type_of (connecter_diff0 y u))). Intros. EApply (!extensionality (substrate alpha) [x:(substrate alpha)](type_of (connecter_diff0 y y0 x))). Intros. EApply H0. NewInduction H1. Assert connecter_left0==connecter_left1. EApply proof_irrelevance. Assert connecter_right0==connecter_right1. EApply proof_irrelevance. Rewrite H1. Rewrite H2. Trivial. Save. Section connecter_description_def. Variable c:C. Variable alpha: (onecocycle A). Variable de : (description A). Variable V : (virtual (connecter c alpha)). Local Z := (carrier V). Section cdescripA. Variable b:B. Hypothesis hyp : (g b) == c. Variable x: (substrate alpha). Local virt_cdiff : (virtual A). EApply (!Build_virtual A Z [z:Z](V z b hyp x)). Unfold Z. EApply virt_nonempty. Intros. Assert (V v)==(V w). Apply virt_equal. Rewrite H. Trivial. Defined. Remark rmk1 : (z:Z)(virt_cdiff z) == (V z b hyp x). Intros. Trivial. Save. Definition real_cdiff : A. Exact (de virt_cdiff). Defined. Remark rmk2 : (z:Z)real_cdiff == (V z b hyp x). Intros. Rewrite <- rmk1. Unfold real_cdiff. EApply description_eq. Save. End cdescripA. Definition connecter_the_descrip : (connecter c alpha). EApply (!Build_connecter c alpha real_cdiff). Intros. Assert (nonempty Z). Unfold Z. EApply virt_nonempty. NewInduction H. Assert (real_cdiff hyp' x)==(V X b' hyp' x). EApply cdescripA.rmk2. Assert (real_cdiff hyp x)==(V X b hyp x). EApply cdescripA.rmk2. Rewrite H. Rewrite H0. EApply connecter_left. Intros. Assert (nonempty Z). Unfold Z. EApply virt_nonempty. NewInduction H. Assert (real_cdiff hyp x)==(V X b hyp x). EApply cdescripA.rmk2. Assert (real_cdiff hyp y)==(V X b hyp y). EApply cdescripA.rmk2. Rewrite H. Rewrite H0. EApply connecter_right. Defined. Remark rmk3: (z:Z)connecter_the_descrip == (V z). Intros. EApply connecter_extens. Intros. Change (real_cdiff hyp x)==(V z b hyp x). EApply cdescripA.rmk2. Save. End connecter_description_def. Definition connecter_description : (c:C; alpha : (onecocycle A); de : (description A)) (description (connecter c alpha)). Intros. EApply (!Build_description (connecter c alpha) (!connecter_the_descrip c alpha de)). Intros. EApply connecter_description_def.rmk3. Defined. Definition connecter_cocycle :=[c:C; alpha,beta : (onecocycle A); d: (connecter c alpha); e : (connecter c beta); m : (onecoboundary alpha beta)] (b:B; hyp : (g b) == c; x: (substrate alpha); y: (substrate beta)) (op (m x y) (d b hyp x)) == (e b hyp y). Section connecter_coboundary_def. Variable c:C. Variables alpha,beta : (onecocycle A). Variable d : (connecter c alpha). Variable e : (connecter c beta). Theorem connecter_coboundary_exists : (exT [m: (onecoboundary alpha beta)] (connecter_cocycle d e m)). NewInduction (surj c). LetTac U := [y:(substrate alpha); z: (substrate beta)] (op (e x H z) (inv (d x H y))). Assert U_left : (u,v:(substrate alpha); w:(substrate beta)) (op (U v w) (alpha u v))==(U u w). Intros. Unfold U. Transitivity (op (e x H w) (op (inv (d x H v)) (alpha u v))). EApply assoc. Assert (op (inv (d x H v)) (alpha u v))==(inv (d x H u)). EApply inv_left_char. Transitivity (op (inv (d x H v)) (op (alpha u v) (d x H u))). EApply assoc. Assert (op (alpha u v) (d x H u))==(d x H v). EApply connecter_right. Rewrite H0. EApply left_inv. Rewrite H0. Trivial. Assert U_right : (u:(substrate alpha); v,w:(substrate beta)) (op (beta v w) (U u v))==(U u w). Intros. Unfold U. Transitivity (op (op (beta v w) (e x H v)) (inv (d x H u))). Symmetry. EApply assoc. Assert (op (beta v w) (e x H v))==(e x H w). EApply connecter_right. Rewrite H0. Trivial. LetTac M:=(!Build_onecoboundary A alpha beta U U_left U_right). EApply exT_intro with M. Unfold connecter_cocycle. Intros. Change (op (U x0 y) (d b hyp x0))==(e b hyp y) . Unfold U. Assert (e x H y)==(op (e b hyp y) (exact_diff H hyp)). Symmetry. EApply connecter_left. Assert (d b hyp x0)==(op (d x H x0) (exact_diff hyp H)). Symmetry. EApply connecter_left. Rewrite H0. Transitivity (op (e b hyp y) (op (op (exact_diff H hyp) (inv (d x H x0))) (d b hyp x0))). AutoRewrite [ assoc_left ]. Trivial. Transitivity (op (e b hyp y) (id ?)). EApply unop_left. EApply switch. EApply multiply_right with (d x H x0). Rewrite left_id. AutoRewrite [ assoc_right ]. Rewrite left_inv. AutoRewrite [ assoc_left ]. Rewrite right_id. EApply connecter_left. EApply right_id. Save. Theorem connecter_coboundary_unique : (m,m' : (onecoboundary alpha beta)) (connecter_cocycle d e m) -> (connecter_cocycle d e m') -> m == m'. Intros. EApply onecoboundary_extens. Intros. Unfold connecter_cocycle in H. Unfold connecter_cocycle in H0. NewInduction (surj c). LetTac K:=(H x0 H1 x y). LetTac K0:=(H0 x0 H1 x y). EApply multiply_right with (d x0 H1 x). Rewrite K. Rewrite K0. Trivial. Save. Record ccob_carrier : Type := { the_ccob :> (onecoboundary alpha beta); ccob_cocycle : (connecter_cocycle d e the_ccob) }. Theorem ccob_one_elt : (has_one_element ccob_carrier). EApply Build_has_one_element. LetTac E := connecter_coboundary_exists. NewInduction E. EApply nonempty_intro. EApply (!Build_ccob_carrier x H). Intros. NewInduction a. NewInduction b. Assert the_ccob0==the_ccob1. EApply connecter_coboundary_unique. Assumption. Assumption. NewInduction H. Assert ccob_cocycle0==ccob_cocycle1. EApply proof_irrelevance. Rewrite H. Trivial. Save. Local V : (virtual (onecoboundary alpha beta)). EApply (!Build_virtual (onecoboundary alpha beta) ccob_carrier the_ccob). EApply one_nonempty. EApply ccob_one_elt. Intros. NewInduction v. NewInduction w. Assert the_ccob0==the_ccob1. EApply connecter_coboundary_unique. Assumption. Assumption. NewInduction H. Assert ccob_cocycle0==ccob_cocycle1. EApply proof_irrelevance. Rewrite H. Trivial. Defined. Remark rmk1 : (c:(carrier V))(connecter_cocycle d e (V c)). Intros. Assert (V c0)==(the_ccob c0). Trivial. Rewrite H. EApply ccob_cocycle. Save. Definition ccob_touch : (description A)->(onecoboundary alpha beta). Intro de. Assert (description (onecoboundary alpha beta)). EApply onecoboundary_description. Assumption. EApply (the_description X). Exact V. Defined. Remark rmk2 : (c:(carrier V); de : (description A))(ccob_touch de) == (V c). Intros. Unfold ccob_touch. EApply description_eq. Save. Theorem ccob_touch_cocycle : (de : (description A)) (connecter_cocycle d e (ccob_touch de)). Intros. Assert (nonempty (carrier V)). EApply virt_nonempty. NewInduction H. Assert (ccob_touch de)==(V X). EApply rmk2. Rewrite H. EApply rmk1. Save. End connecter_coboundary_def. Section connecter_connecter_def. Variable c:C. Variables alpha, beta: (onecocycle A). Variable d: (connecter c alpha). Variable m : (onecoboundary alpha beta). Theorem connecter_connecter_exists : (exT [e: (connecter c beta)] (connecter_cocycle d e m)). NewInduction (surj c). Assert (nonempty (substrate alpha)). EApply substrate_nonempty. NewInduction H0. LetTac U:=[b:B; hyp:((g b)==c); u:(substrate beta)](op (m X u) (d b hyp X)). Assert U_left : (b1,b2:B; hyp1 : (g b1) == c; hyp2 : (g b2) == c; u:(substrate beta)) (op (U b2 hyp2 u) (exact_diff hyp1 hyp2)) == (U b1 hyp1 u). Intros. Unfold U. Transitivity (op (m X u) (op (d b0 hyp2 X) (exact_diff hyp1 hyp2))). EApply assoc. EApply unop_left. EApply connecter_left. Assert U_right : (b:B;hyp : (g b) == c; u,v:(substrate beta)) (op (beta u v) (U b hyp u)) == (U b hyp v). Intros. Unfold U. Transitivity (op (op (beta u v) (m X u)) (d b hyp X)). Symmetry. EApply assoc. EApply unop_right. EApply cobound_right. LetTac W:=(!Build_connecter c beta U U_left U_right). EApply exT_intro with W. Unfold connecter_cocycle. Intros. Unfold W. Symmetry. Transitivity (U b hyp y). Trivial. Unfold U. Assert (m x0 y)==(op (m X y) (alpha x0 X)). Symmetry. EApply cobound_left. Rewrite H0. Symmetry. Transitivity (op (m X y) (op (alpha x0 X) (d b hyp x0))). EApply assoc. EApply unop_left. EApply connecter_right. Save. Theorem connecter_connecter_unique : (e,e' : (connecter c beta)) (connecter_cocycle d e m) -> (connecter_cocycle d e' m) -> e == e'. Intros. EApply connecter_extens. Intros. Assert (nonempty (substrate alpha)). EApply substrate_nonempty. NewInduction H1. Transitivity (op (m X x) (d b hyp X)). Symmetry. EApply H. EApply H0. Save. Record ccon_carrier : Type := { the_ccon :> (connecter c beta); ccon_cocycle : (connecter_cocycle d the_ccon m) }. Theorem ccon_one_elt: (has_one_element ccon_carrier). EApply Build_has_one_element. LetTac K:=connecter_connecter_exists. NewInduction K. EApply nonempty_intro. EApply (!Build_ccon_carrier x). Assumption. Intros. NewInduction a. NewInduction b. Assert the_ccon0==the_ccon1. EApply connecter_connecter_unique. Assumption. Assumption. NewInduction H. Assert ccon_cocycle0==ccon_cocycle1. EApply proof_irrelevance. Rewrite H. Trivial. Save. Local V : (virtual (connecter c beta)). EApply (!Build_virtual (connecter c beta) ccon_carrier the_ccon). EApply one_nonempty. EApply ccon_one_elt. Intros. Assert v==w. EApply one_unique. EApply ccon_one_elt. Rewrite H. Trivial. Defined. Variable de : (description A). Definition ccon_touch : (connecter c beta). Assert (description (connecter c beta)). EApply connecter_description. Assumption. EApply (the_description X). Exact V. Defined. Remark rmk1 : (z:(carrier V))ccon_touch == (V z). Intros. Unfold ccon_touch. EApply description_eq. Save. Theorem ccon_touch_cocycle : (connecter_cocycle d ccon_touch m). Assert (nonempty (carrier V)). EApply virt_nonempty. NewInduction H. Assert ccon_touch==(V X). EApply rmk1. Rewrite H. Assert (V X)==(the_ccon X). Trivial. Rewrite H0. EApply ccon_cocycle. Save. End connecter_connecter_def. Section connectee_def. Variable c:C. Variable U : TypeL. Hypothesis ne : (nonempty U). Variable s: U -> B. Variable hyp : (u:U)(g (s u)) == c. Definition connectee_diff : U -> U -> A. Intros x y. Assert (g (s x))==c. Apply hyp. Assert (g (s y))==c. Apply hyp. Exact (exact_diff H H0). Defined. Remark rmk1 : (x,y: U)(f (connectee_diff x y)) == (op (s y) (inv (s x))). Intros. Unfold connectee_diff. EApply exact_diff_eq. Save. Definition connectee : (onecocycle A). EApply (!Build_onecocycle A U connectee_diff). Assumption. Intros. EApply inj. Transitivity (op (f (connectee_diff y z)) (f (connectee_diff x y))). Symmetry. EApply gmap_op. Rewrite rmk1. Rewrite rmk1. Rewrite rmk1. AutoRewrite [ assoc_right ]. EApply unop_left. AutoRewrite [ assoc_left ]. Rewrite left_inv. EApply left_id. Defined. Definition connectee_connecter_diff : (b:B; hyp : (g b) == c; x:U) A. Intros. Assert (g (s x))==c. Apply hyp. Exact (exact_diff hyp0 H). Defined. Remark rmk2: (b:B; hyp : (g b) == c; x:U) (f (connectee_connecter_diff hyp x)) == (op (s x) (inv b)). Intros. Unfold connectee_connecter_diff. EApply exact_diff_eq. Save. Definition connectee_connecter : (connecter c connectee). EApply (!Build_connecter c connectee connectee_connecter_diff). Intros. EApply inj. Rewrite <- gmap_op. Rewrite rmk2. Rewrite rmk2. Rewrite exact_diff_eq. AutoRewrite [ assoc_left ]. EApply unop_right. AutoRewrite [ assoc_right ]. Rewrite left_inv. EApply right_id. Intros. EApply inj. Rewrite <- gmap_op. Rewrite rmk2. Rewrite rmk2. Rewrite rmk1. AutoRewrite [ assoc_left ]. EApply unop_right. AutoRewrite [ assoc_right ]. Rewrite left_inv. EApply right_id. Defined. End connectee_def. Section connecter_two_section. Variables c1, c2 : C. Variable alpha : (onecocycle A). Variable d1: (connecter c1 alpha). Variable d2 : (connecter c2 alpha). Variable deb : (description B). (*** try to get back an element b : B with (op b c1) == c2 ***) Record connecter_two_carrier : Type := { ctc_b1 : B; ctc_b2 : B; ctc_sub : (substrate alpha); ctc_hyp1 : (g ctc_b1) == c1; ctc_hyp2 : (g ctc_b2) == c2 }. Local ctc_b1_corr := [w:connecter_two_carrier] (op (f (d1 (ctc_b1 w) (ctc_hyp1 w) (ctc_sub w))) (ctc_b1 w)). Local ctc_b2_corr := [w:connecter_two_carrier] (op (f (d2 (ctc_b2 w) (ctc_hyp2 w) (ctc_sub w))) (ctc_b2 w)). Remark rmk1 : (w:connecter_two_carrier)(g (ctc_b1_corr w)) == c1. Intros. Unfold ctc_b1_corr. Rewrite <- gmap_op. Rewrite comp. Rewrite left_id. EApply ctc_hyp1. Save. Remark rmk2 : (w:connecter_two_carrier)(g (ctc_b2_corr w)) == c2. Intros. Unfold ctc_b2_corr. Rewrite <- gmap_op. Rewrite comp. Rewrite left_id. EApply ctc_hyp2. Save. Definition ctc_virt_touch :connecter_two_carrier -> B := [w:connecter_two_carrier](op (inv (ctc_b1_corr w)) (ctc_b2_corr w) ). Remark rmk3 : (w:connecter_two_carrier)(op c1 (g (ctc_virt_touch w))) == c2. Intros. Unfold ctc_virt_touch. Rewrite <- gmap_op. Rewrite gmap_inv. Rewrite rmk1. Rewrite rmk2. AutoRewrite [ assoc_left ]. Rewrite right_inv. Apply left_id. Save. Remark rmk4 : (w,w' : connecter_two_carrier) (op (f (exact_diff (ctc_hyp2 w') (ctc_hyp2 w))) (ctc_b2 w')) == (ctc_b2 w). Intros. Rewrite exact_diff_eq. AutoRewrite [ assoc_right ]. Rewrite left_inv. EApply right_id. Save. Remark rmk5 : (w,w' : connecter_two_carrier) (op (inv (ctc_b1 w')) (inv (f (exact_diff (ctc_hyp1 w') (ctc_hyp1 w))) )) == (inv (ctc_b1 w)). Intros. Rewrite exact_diff_eq. Rewrite inv_op. Rewrite inv_inv. AutoRewrite [ assoc_left ]. Rewrite left_inv. Apply left_id. Save. Theorem ctc_virt_unique : (w,w' : connecter_two_carrier) (ctc_virt_touch w) == (ctc_virt_touch w'). Intros. Unfold ctc_virt_touch. Unfold ctc_b1_corr. Unfold ctc_b2_corr. LetTac K1:=(connecter_both d1 (ctc_hyp1 w) (ctc_hyp1 w') (ctc_sub w) (ctc_sub w')). LetTac K2:=(connecter_both d2 (ctc_hyp2 w) (ctc_hyp2 w') (ctc_sub w) (ctc_sub w')). Rewrite <- K1. Rewrite <- K2. AutoRewrite [ gmap_in ]. AutoRewrite [ inv_in ]. AutoRewrite [ assoc_left ]. Rewrite rmk5. AutoRewrite [ assoc_right ]. EApply unop_left. EApply unop_left. Rewrite rmk4. AutoRewrite [ assoc_left ]. EApply unop_right. Rewrite left_inv. Rewrite left_id. Trivial. Save. Remark rmk6 : (nonempty connecter_two_carrier). Assert (nonempty (substrate alpha)). EApply substrate_nonempty. Assert (exT [u1:B](g u1)==c1). EApply surj. Assert (exT [u2:B](g u2)==c2). EApply surj. NewInduction H. NewInduction H0. NewInduction H1. EApply nonempty_intro. EApply Build_connecter_two_carrier with x x0. Assumption. Assumption. Assumption. Save. Definition connecter_two_virtual : (virtual B). EApply (!Build_virtual B connecter_two_carrier ctc_virt_touch). EApply rmk6. Intros. EApply ctc_virt_unique. Defined. Remark rmk7 : (u: (carrier connecter_two_virtual)) (op c1 (g (connecter_two_virtual u))) == c2. Intros. EApply rmk3. Save. Definition connecter_two : B. Exact (deb connecter_two_virtual). Defined. Theorem connecter_two_property : (op c1 (g connecter_two)) == c2. Assert (nonempty (carrier connecter_two_virtual)). EApply virt_nonempty. NewInduction H. Assert connecter_two == (connecter_two_virtual X). Unfold connecter_two. EApply description_eq. Rewrite H. EApply rmk7. Save. End connecter_two_section. Section connecter_three_section. Variables c1, c2 : C. Variables alpha, beta : (onecocycle A). Variable d1: (connecter c1 alpha). Variable d2 : (connecter c2 beta). Variable m : (onecoboundary alpha beta). Variable dea : (description A). Variable deb : (description B). Definition c3_new_d1 : (connecter c1 beta). EApply ccon_touch with alpha. Assumption. Assumption. Assumption. Defined. Definition connecter_three : B. EApply connecter_two with c1 c2 beta. EApply c3_new_d1. Assumption. Assumption. Defined. Theorem connecter_three_property : (op c1 (g connecter_three)) == c2. Unfold connecter_three. EApply connecter_two_property. Save. End connecter_three_section. End exact_sequence_properties. Record small_cover_replacement [X:Type; Y:X -> Type] : Type := { scr_upsilon : X -> TypeL; scr_phi : (x:X)(scr_upsilon x) -> (Y x); scr_nonempty : (x:X)(nonempty (scr_upsilon x)) }. Section long_exact_sequence_section. Variable X : Type. Variable scr : (Y: X -> Type; hyp : (x:X)(nonempty (Y x))) (small_cover_replacement Y). Variables A,B,C: X -> group. Variable f : (x:X)(gmap (A x) (B x)). Variable g : (x:X)(gmap (B x) (C x)). Variable de : (x:X)(description (A x)). Variable deb : (x:X)(description (B x)). Hypothesis inj : (x:X; a1,a2 : (A x))(f x a1) == (f x a2) -> a1 == a2. Hypothesis surj : (x:X; c:(C x))(exT [b:(B x)](g x b) == c). Hypothesis comp : (x:X; a: (A x))(g x (f x a)) == (id (C x)). Hypothesis exact : (x:X; b:(B x))(g x b) == (id (C x)) -> (exT [a:(A x)](f x a) == b). Record les_f_inv_im [x:X; b:(B x)]: Type := { lfii : (A x); lfii_eq : (f x lfii) == b }. Record les_g_inv_im [x:X; c : (C x)] : Type := { lgii : (B x); lgii_eq : (g x lgii) == c }. Definition exact_virtual_section : (x:X; b:(B x); hyp : (g x b) == (id (C x))) (virtual (A x)). Intros. EApply (!Build_virtual (A x) (les_f_inv_im b) (!lfii x b)). LetTac K:=(exact hyp). NewInduction K. EApply nonempty_intro. Exact (Build_les_f_inv_im H). Intros. EApply inj. Rewrite lfii_eq. Rewrite lfii_eq. Trivial. Defined. Definition exact_section : (x:X; b:(B x); hyp : (g x b) == (id (C x))) (A x). Intros. Exact (de x (exact_virtual_section hyp)). Defined. Theorem exact_section_eq : (x:X; b:(B x); hyp : (g x b) == (id (C x))) (f x (exact_section hyp)) == b. Intros. LetTac V:=(exact_virtual_section hyp). Assert (nonempty (carrier V)). EApply virt_nonempty. NewInduction H. Assert (exact_section hyp)==(V X0). Unfold exact_section. EApply description_eq. Rewrite H. Assert (V X0)==(!lfii x b X0). Trivial. Rewrite H0. EApply lfii_eq. Save. Section connecting_map_def. Variable c: (x:X)(C x). Local connecting_scr : (small_cover_replacement [x:X](les_g_inv_im (c x))). EApply scr. Intros. LetTac K:=(surj (c x)). NewInduction K. EApply nonempty_intro. Exact (Build_les_g_inv_im H). Defined. Definition connecting_substrate : X -> TypeL. Exact (scr_upsilon connecting_scr). Defined. Definition connecting_substrate_map : (x:X)(connecting_substrate x) -> (B x). Intros. EApply lgii with (c x). EApply (!scr_phi X [x:X](les_g_inv_im (c x)) connecting_scr). Exact X0. Defined. Theorem connecting_substrate_eq : (x:X; u:(connecting_substrate x)) (g x (connecting_substrate_map u))== (c x). Intros. Unfold connecting_substrate_map. EApply lgii_eq. Save. Theorem connecting_substrate_ne : (x:X)(nonempty (connecting_substrate x)). Intros. Unfold connecting_substrate. EApply scr_nonempty. Save. Definition les_connectee : (x:X)(onecocycle (A x)). Intro x. Exact (!connectee (A x) (B x) (C x) (f x) (g x) (!inj x) (!exact_section x) (!exact_section_eq x) (c x) (!connecting_substrate x) (!connecting_substrate_ne x) (!connecting_substrate_map x) (!connecting_substrate_eq x)). Defined. Definition les_connecter : (x:X)(connecter (!exact_section x) (c x) (les_connectee x)). Intro x. Unfold les_connectee. EApply connectee_connecter. Defined. Definition les_delta : (h1 A). Exact (h1_class les_connectee). Defined. End connecting_map_def. Section if_delta_same. Variables c1, c2: (x:X)(C x). Hypothesis hyp : (les_delta c1) == (les_delta c2). Theorem delta_same_onecoboundary_nonempty : (nonempty (x:X) (onecoboundary (les_connectee c1 x) (les_connectee c2 x))). EApply h1_class_inj. Exact de. Exact hyp. Save. Section delta_sameA. Variable u : (x:X)(onecoboundary (les_connectee c1 x) (les_connectee c2 x)). Definition les_lift : (x:X)(B x). Intro x. Apply connecter_three with A:=(A x) B:=(B x) C:=(C x) f:=(f x) g:=(g x) exact:=(!exact_section x) c1:=(c1 x) c2:=(c2 x) alpha:=(les_connectee c1 x) beta:=(les_connectee c2 x). Intros. EApply surj. Intros. EApply exact_section_eq. EApply les_connecter. EApply les_connecter. EApply u. EApply de. EApply deb. Defined. Theorem les_lift_property : (x:X)(op (c1 x) (g x (les_lift x))) == (c2 x). Intros. Unfold les_lift. EApply connecter_three_property. Intros. EApply comp. Save. End delta_sameA. Theorem les_first_exact : (exT [b : (x:X)(B x)] (x:X)(op (c1 x) (g x (b x))) == (c2 x) ). LetTac K:=delta_same_onecoboundary_nonempty. NewInduction K. EApply exT_intro with (les_lift X0). Intros. EApply les_lift_property. Save. End if_delta_same. Section if_h1_trivial. Variable c: (x:X)(C x). Hypothesis h1_trivial : (u,v : (h1 A)) u == v. Definition identity_section : (x:X)(C x) := [x:X](id (C x)). Remark rmk1 : (les_delta identity_section) == (les_delta c). EApply h1_trivial. Save. Remark rmk2 : (exT [b:(x:X)(B x)] (x:X)(op (identity_section x) (g x (b x))) == (c x)). EApply les_first_exact. Exact rmk1. Save. Theorem lift_when_h1_trivial : (exT [b:(x:X)(B x)](x:X)(g x (b x)) == (c x)). LetTac K:=rmk2. NewInduction K. EApply exT_intro with x. Intros. Rewrite <- H. Assert (identity_section x0)==(id (C x0)). Trivial. Rewrite H0. Symmetry. EApply left_id. Save. End if_h1_trivial. (***** ideally we should still define the trivial element of h1 and show that if c is something whose les_delta is the trivial element then it comes from B, the point being to show that the les_delta of the identity section is equivalent to the trivial element ******) End long_exact_sequence_section. Theorem lift_when_h1_trivial_rewrite : (X:Type) ((Y:(X->Type)) ((x:X)(nonempty (Y x)))->(small_cover_replacement Y)) ->(A,B,C:(X->group); f:((x:X)(gmap (A x) (B x))); g:((x:X)(gmap (B x) (C x)))) ((x:X)(description (A x))) ->((x:X)(description (B x))) ->((x:X; a1,a2:(A x))(f x a1)==(f x a2)->a1==a2) ->((x:X; c:(C x))(exT [b:(B x)](g x b)==c)) ->((x:X; a:(A x))(g x (f x a))==(id (C x))) ->((x:X; b:(B x)) (g x b)==(id (C x))->(exT [a:(A x)](f x a)==b)) ->(c:((x:X)(C x))) ((u,v:(h1 A))u==v) ->(exT [b:((x:X)(B x))](x:X)(g x (b x))==(c x)). Proof lift_when_h1_trivial.