equal
deleted
inserted
replaced
538 shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))" |
538 shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))" |
539 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) |
539 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) |
540 |
540 |
541 |
541 |
542 text{*Basis for homomorphism proofs: we assume two groups @{term G} and |
542 text{*Basis for homomorphism proofs: we assume two groups @{term G} and |
543 @term{H}, with a homomorphism @{term h} between them*} |
543 @{term H}, with a homomorphism @{term h} between them*} |
544 locale group_hom = group G + group H + var h + |
544 locale group_hom = group G + group H + var h + |
545 assumes homh: "h \<in> hom G H" |
545 assumes homh: "h \<in> hom G H" |
546 notes hom_mult [simp] = hom_mult [OF homh] |
546 notes hom_mult [simp] = hom_mult [OF homh] |
547 and hom_closed [simp] = hom_closed [OF homh] |
547 and hom_closed [simp] = hom_closed [OF homh] |
548 |
548 |
551 by simp |
551 by simp |
552 |
552 |
553 lemma (in group_hom) hom_one [simp]: |
553 lemma (in group_hom) hom_one [simp]: |
554 "h \<one> = \<one>\<^bsub>H\<^esub>" |
554 "h \<one> = \<one>\<^bsub>H\<^esub>" |
555 proof - |
555 proof - |
556 have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>" |
556 have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>" |
557 by (simp add: hom_mult [symmetric] del: hom_mult) |
557 by (simp add: hom_mult [symmetric] del: hom_mult) |
558 then show ?thesis by (simp del: r_one) |
558 then show ?thesis by (simp del: r_one) |
559 qed |
559 qed |
560 |
560 |
561 lemma (in group_hom) inv_closed [simp]: |
561 lemma (in group_hom) inv_closed [simp]: |