部分群

Subgroup G は G の部分群の型です． これは Set G に「閉性の証明」を追加した bundled structure です． そのため，x ∈ H のように集合として使えますが，同時に部分群としての構造も持っています．

#check Subgroup
#check AddSubgroup

section Subgroups

variable {G H : Type*} [Group G] [Group H]
variable (S T : Subgroup G)

example {x y : G} (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S := by
  exact S.mul_mem hx hy

example {x : G} (hx : x ∈ S) : x⁻¹ ∈ S := by
  exact S.inv_mem hx

example : ((S ⊓ T : Subgroup G) : Set G) = (S : Set G) ∩ (T : Set G) := by
  rfl

example (x : G) : x ∈ (⊤ : Subgroup G) := by
  trivial

example (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := by
  exact Subgroup.mem_bot

variable (f : G →* H) (U : Subgroup H)

example : Subgroup H :=
  Subgroup.map f S

example : Subgroup G :=
  Subgroup.comap f U

example (x : G) : x ∈ Subgroup.comap f U ↔ f x ∈ U := by
  rfl

#check Subgroup.mem_map
#check MonoidHom.ker
#check MonoidHom.range

end Subgroups

部分群全体は包含関係で順序づけられ，束構造を持ちます． S ⊓ T は交わりに対応します． 一方，S ⊔ T は単純な和集合ではなく，和集合で生成される部分群です． これは「和集合は一般には部分群でない」ことを反映しています．

演習問題

1. 部分群の map が包含を保つことを示してください．

   example {G H : Type*} [Group G] [Group H]
       (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) :
       Subgroup.map φ S ≤ Subgroup.map φ T := by
     -- `Subgroup.mem_map` で元を存在記号に分解する．
     sorry
   

2. 部分群の comap が包含を保つことを示してください．

   example {G H : Type*} [Group G] [Group H]
       (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) :
       Subgroup.comap φ S ≤ Subgroup.comap φ T := by
     -- `rfl` で membership を展開できる．
     sorry
   

3. MonoidHom.ker f の membership を読み替えてください．

   example {G H : Type*} [Group G] [Group H] (f : G →* H) (x : G) :
       x ∈ MonoidHom.ker f ↔ f x = 1 := by
     -- `f.mem_ker` を調べる．
     sorry
   

4. MonoidHom.range f の membership を読み替えてください．

   example {G H : Type*} [Group G] [Group H] (f : G →* H) (y : H) :
       y ∈ MonoidHom.range f ↔ ∃ x : G, f x = y := by
     -- `f.mem_range` を調べる．
     sorry
   

5. 部分群の積で閉じていることを，S.mul_mem ではなく show でゴールを明示して証明してください．

   example {G : Type*} [Group G] (S : Subgroup G) {x y : G}
       (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S := by
     -- ヒント:
     --   show x * y ∈ S
     --   exact S.mul_mem hx hy
     sorry