summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/Group.thy

changeset 22063 | 717425609192 |

parent 21041 | 60e418260b4d |

child 23350 | 50c5b0912a0c |

equal
deleted
inserted
replaced

22062:f4cfc4101c8f | 22063:717425609192 |
---|---|

683 subsection {* The Lattice of Subgroups of a Group *} |
683 subsection {* The Lattice of Subgroups of a Group *} |

684 |
684 |

685 text_raw {* \label{sec:subgroup-lattice} *} |
685 text_raw {* \label{sec:subgroup-lattice} *} |

686 |
686 |

687 theorem (in group) subgroups_partial_order: |
687 theorem (in group) subgroups_partial_order: |

688 "partial_order {H. subgroup H G} (op \<subseteq>)" |
688 "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |

689 by (rule partial_order.intro) simp_all |
689 by (rule partial_order.intro) simp_all |

690 |
690 |

691 lemma (in group) subgroup_self: |
691 lemma (in group) subgroup_self: |

692 "subgroup (carrier G) G" |
692 "subgroup (carrier G) G" |

693 by (rule subgroupI) auto |
693 by (rule subgroupI) auto |

728 with subgr [THEN subgroup.m_closed] |
728 with subgr [THEN subgroup.m_closed] |

729 show "x \<otimes> y \<in> \<Inter>A" by blast |
729 show "x \<otimes> y \<in> \<Inter>A" by blast |

730 qed |
730 qed |

731 |
731 |

732 theorem (in group) subgroups_complete_lattice: |
732 theorem (in group) subgroups_complete_lattice: |

733 "complete_lattice {H. subgroup H G} (op \<subseteq>)" |
733 "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" |

734 (is "complete_lattice ?car ?le") |
734 (is "complete_lattice ?L") |

735 proof (rule partial_order.complete_lattice_criterion1) |
735 proof (rule partial_order.complete_lattice_criterion1) |

736 show "partial_order ?car ?le" by (rule subgroups_partial_order) |
736 show "partial_order ?L" by (rule subgroups_partial_order) |

737 next |
737 next |

738 have "order_syntax.greatest ?car ?le (carrier G) ?car" |
738 have "greatest ?L (carrier G) (carrier ?L)" |

739 by (unfold order_syntax.greatest_def) |
739 by (unfold greatest_def) |

740 (simp add: subgroup.subset subgroup_self) |
740 (simp add: subgroup.subset subgroup_self) |

741 then show "\<exists>G. order_syntax.greatest ?car ?le G ?car" .. |
741 then show "\<exists>G. greatest ?L G (carrier ?L)" .. |

742 next |
742 next |

743 fix A |
743 fix A |

744 assume L: "A \<subseteq> ?car" and non_empty: "A ~= {}" |
744 assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}" |

745 then have Int_subgroup: "subgroup (\<Inter>A) G" |
745 then have Int_subgroup: "subgroup (\<Inter>A) G" |

746 by (fastsimp intro: subgroups_Inter) |
746 by (fastsimp intro: subgroups_Inter) |

747 have "order_syntax.greatest ?car ?le (\<Inter>A) (order_syntax.Lower ?car ?le A)" |
747 have "greatest ?L (\<Inter>A) (Lower ?L A)" |

748 (is "order_syntax.greatest _ _ ?Int _") |
748 (is "greatest _ ?Int _") |

749 proof (rule order_syntax.greatest_LowerI) |
749 proof (rule greatest_LowerI) |

750 fix H |
750 fix H |

751 assume H: "H \<in> A" |
751 assume H: "H \<in> A" |

752 with L have subgroupH: "subgroup H G" by auto |
752 with L have subgroupH: "subgroup H G" by auto |

753 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |
753 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") |

754 by (rule subgroup_imp_group) |
754 by (rule subgroup_imp_group) |

755 from groupH have monoidH: "monoid ?H" |
755 from groupH have monoidH: "monoid ?H" |

756 by (rule group.is_monoid) |
756 by (rule group.is_monoid) |

757 from H have Int_subset: "?Int \<subseteq> H" by fastsimp |
757 from H have Int_subset: "?Int \<subseteq> H" by fastsimp |

758 then show "?le ?Int H" by simp |
758 then show "le ?L ?Int H" by simp |

759 next |
759 next |

760 fix H |
760 fix H |

761 assume H: "H \<in> order_syntax.Lower ?car ?le A" |
761 assume H: "H \<in> Lower ?L A" |

762 with L Int_subgroup show "?le H ?Int" |
762 with L Int_subgroup show "le ?L H ?Int" |

763 by (fastsimp simp: order_syntax.Lower_def intro: Inter_greatest) |
763 by (fastsimp simp: Lower_def intro: Inter_greatest) |

764 next |
764 next |

765 show "A \<subseteq> ?car" by (rule L) |
765 show "A \<subseteq> carrier ?L" by (rule L) |

766 next |
766 next |

767 show "?Int \<in> ?car" by simp (rule Int_subgroup) |
767 show "?Int \<in> carrier ?L" by simp (rule Int_subgroup) |

768 qed |
768 qed |

769 then show "\<exists>I. order_syntax.greatest ?car ?le I (order_syntax.Lower ?car ?le A)" .. |
769 then show "\<exists>I. greatest ?L I (Lower ?L A)" .. |

770 qed |
770 qed |

771 |
771 |

772 end |
772 end |