equal
deleted
inserted
replaced
547 {h. h \<in> carrier G -> carrier H & |
547 {h. h \<in> carrier G -> carrier H & |
548 (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}" |
548 (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}" |
549 |
549 |
550 lemma (in group) hom_compose: |
550 lemma (in group) hom_compose: |
551 "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I" |
551 "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I" |
552 by (fastsimp simp add: hom_def compose_def) |
552 by (fastforce simp add: hom_def compose_def) |
553 |
553 |
554 definition |
554 definition |
555 iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) |
555 iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) |
556 where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}" |
556 where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}" |
557 |
557 |
779 qed |
779 qed |
780 next |
780 next |
781 fix A |
781 fix A |
782 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
782 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |
783 then have Int_subgroup: "subgroup (\<Inter>A) G" |
783 then have Int_subgroup: "subgroup (\<Inter>A) G" |
784 by (fastsimp intro: subgroups_Inter) |
784 by (fastforce intro: subgroups_Inter) |
785 show "\<exists>I. greatest ?L I (Lower ?L A)" |
785 show "\<exists>I. greatest ?L I (Lower ?L A)" |
786 proof |
786 proof |
787 show "greatest ?L (\<Inter>A) (Lower ?L A)" |
787 show "greatest ?L (\<Inter>A) (Lower ?L A)" |
788 (is "greatest _ ?Int _") |
788 (is "greatest _ ?Int _") |
789 proof (rule greatest_LowerI) |
789 proof (rule greatest_LowerI) |
792 with L have subgroupH: "subgroup H G" by auto |
792 with L have subgroupH: "subgroup H G" by auto |
793 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
793 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
794 by (rule subgroup_imp_group) |
794 by (rule subgroup_imp_group) |
795 from groupH have monoidH: "monoid ?H" |
795 from groupH have monoidH: "monoid ?H" |
796 by (rule group.is_monoid) |
796 by (rule group.is_monoid) |
797 from H have Int_subset: "?Int \<subseteq> H" by fastsimp |
797 from H have Int_subset: "?Int \<subseteq> H" by fastforce |
798 then show "le ?L ?Int H" by simp |
798 then show "le ?L ?Int H" by simp |
799 next |
799 next |
800 fix H |
800 fix H |
801 assume H: "H \<in> Lower ?L A" |
801 assume H: "H \<in> Lower ?L A" |
802 with L Int_subgroup show "le ?L H ?Int" |
802 with L Int_subgroup show "le ?L H ?Int" |
803 by (fastsimp simp: Lower_def intro: Inter_greatest) |
803 by (fastforce simp: Lower_def intro: Inter_greatest) |
804 next |
804 next |
805 show "A \<subseteq> carrier ?L" by (rule L) |
805 show "A \<subseteq> carrier ?L" by (rule L) |
806 next |
806 next |
807 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
807 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |
808 qed |
808 qed |