Theory Subgroup_Lattice

section ‹The lattice of subgroups›

theory Subgroup_Lattice
  imports Group_Theory Order_Theory
begin

text ‹The subgroups of a group ‹G›, ordered by inclusion, form a complete lattice: the infimum of a
  family of subgroups is their intersection (taken together with ‹G› itself, so the empty family has
  infimum ‹G›), and the supremum is the subgroup generated by their union.  This is the first concrete
  consumer of the abstract order theory of ‹Order_Theory›.›

context Group
begin

subsection ‹Intersections of subgroups›

text ‹The intersection of a nonempty family of subgroups is a subgroup.›
lemma subgroup_Inter:
  assumes ne: "𝒜 ≠ {}" and sub: "⋀H. H ∈ 𝒜 ⟹ Subgroup H G (⋅) 𝟭"
  shows "Subgroup (⋂ 𝒜) G (⋅) 𝟭"
proof -
  obtain H0 where H0: "H0 ∈ 𝒜" using ne by blast
  interpret H0: Subgroup H0 G "(⋅)" 𝟭 by (rule sub[OF H0])
  show ?thesis
  proof (rule subgroupI)
    show "⋂ 𝒜 ⊆ G" using H0 H0.subset by blast
    show "𝟭 ∈ ⋂ 𝒜"
      using Subgroup_def Submonoid.sub_unit_closed sub by fastforce
  next
    fix g h assume g: "g ∈ ⋂ 𝒜" and h: "h ∈ ⋂ 𝒜"
    show "g ⋅ h ∈ ⋂ 𝒜"
      using Subgroup_def Submonoid.sub_composition_closed g h sub by fastforce
  next
    fix g assume g: "g ∈ ⋂ 𝒜"
    then show "invertible g" using H0.sub H0 by blast
    show "inverse g ∈ ⋂ 𝒜"
      using H0 H0.sub g invertible sub by (meson Inter_iff Subgroup.subgroup_inverse_iff)
  qed
qed


subsection ‹The complete lattice of subgroups›

text ‹Carrier: the set of all subgroups of ‹G›; order: inclusion.›
definition subgroups :: "'a set set"
  where "subgroups = {H. Subgroup H G (⋅) 𝟭}"

lemma subgroups_iff [simp]: "H ∈ subgroups ⟷ Subgroup H G (⋅) 𝟭"
  by (simp add: subgroups_def)

text ‹Inclusion is a partial order on the subgroups.›
interpretation subgroup_order: Partial_Order subgroups "(⊆)"
  by unfold_locales auto

text ‹Every family of subgroups has an infimum (its intersection with ‹G›) and a supremum (the
  subgroup generated by its union), so the subgroups form a complete lattice.›
interpretation subgroup_lattice: Complete_Lattice subgroups "(⊆)"
proof (unfold_locales)
  fix 𝒜 :: "'a set set" assume 𝒜: "𝒜 ⊆ subgroups"
  ― ‹Supremum: the subgroup generated by the union.›
  have s_sub: "Subgroup ⟨⋃𝒜⟩ G (⋅) 𝟭" by (rule Gen_is_subgroup)
  have "subgroup_order.is_sup ⟨⋃𝒜⟩ 𝒜"
  proof (intro subgroup_order.upper_boundI subgroup_order.is_supI)
    show "⟨⋃𝒜⟩ ∈ subgroups" using s_sub by simp
    fix H assume H: "H ∈ 𝒜"
    then interpret H: Subgroup H G "(⋅)" 𝟭 using 𝒜 by auto
    show "H ⊆ ⟨⋃𝒜⟩" using Gen_incl H H.subset by blast
  next
    fix A assume "subgroup_order.upper_bound A 𝒜"
    then have xsub: "Subgroup A G (⋅) 𝟭" and dom: "⋀H. H ∈ 𝒜 ⟹ H ⊆ A"
      by (auto dest: subgroup_order.upper_boundD simp: subgroup_order.upper_bound_def)
    then show "⟨⋃𝒜⟩ ⊆ A" using xsub by (intro Gen_minimal) auto
  qed
  then show "∃s. subgroup_order.is_sup s 𝒜" ..
next
  fix 𝒜 :: "'a set set" assume 𝒜: "𝒜 ⊆ subgroups"
  ― ‹Infimum: the intersection of ‹𝒜› together with ‹G› (so the empty family gives ‹G›).›
  let ?i = "⋂ (insert G 𝒜)"
  have all_sub: "⋀H. H ∈ insert G 𝒜 ⟹ Subgroup H G (⋅) 𝟭"
    using 𝒜 group_self_subgroup by auto
  have i_sub: "Subgroup ?i G (⋅) 𝟭" by (rule subgroup_Inter) (use all_sub in auto)
  have "subgroup_order.is_inf ?i 𝒜"
  proof (intro subgroup_order.is_infI)
    show "subgroup_order.lower_bound ?i 𝒜"
      using i_sub subgroup_order.lower_boundI by fastforce
  next
    fix x assume "subgroup_order.lower_bound x 𝒜"
    then have xsub: "Subgroup x G (⋅) 𝟭" and dom: "⋀H. H ∈ 𝒜 ⟹ x ⊆ H"
      by (auto dest: subgroup_order.lower_boundD simp: subgroup_order.lower_bound_def)
    interpret x: Subgroup x G "(⋅)" 𝟭 by (rule xsub)
    show "x ⊆ ?i" using dom x.subset by blast
  qed
  then show "∃i. subgroup_order.is_inf i 𝒜" ..
qed

text ‹The lattice operations are the familiar ones: meet is intersection, join is the subgroup
  generated by the union, top is ‹G› and bottom is the trivial subgroup ‹{𝟭}›.›

lemma subgroup_top: "subgroup_lattice.top = G"
proof -
  have "subgroup_order.is_sup G subgroups"
  proof (intro subgroup_order.upper_boundI subgroup_order.is_supI)
    show "G ∈ subgroups" by (simp add: group_self_subgroup)
    fix H assume "H ∈ subgroups"
    then show "H ⊆ G"
      using Gen_subgroup_eq Gen_subset_carrier by fastforce
  next
    fix A assume "subgroup_order.upper_bound A subgroups"
    then show "G ⊆ A" by (auto simp: subgroup_order.upper_bound_def group_self_subgroup)
  qed
  then show ?thesis
    unfolding subgroup_lattice.top_def
    using subgroup_order.is_sup_unique subgroup_lattice.is_sup_Sup[OF subset_refl] by blast
qed

end

end