import VersoManual
import Manual.Meta
-- Minimal-Imports statt `import Mathlib`: ermittelt mit
-- `#min_imports`, ergänzt um QuotientGroup und die
-- Taktik `group`.
import Mathlib.Algebra.Group.Int.Defs
import Mathlib.Algebra.Group.Subgroup.Ker
import Mathlib.GroupTheory.QuotientGroup.Defs
import Mathlib.Tactic.Group

open Verso.Genre Manual
open Verso.Genre.Manual.InlineLean

set_option pp.rawOnError true
set_option verso.docstring.allowMissing true

#doc (Manual) "Gruppen und Restklassengruppen" =>
%%%
htmlSplit := .never
tag := "quotients"
file := "quotients"
%%%

Dieses Kapitel übersetzt zwei Beweise rund um normale Untergruppen
Satz für Satz nach Lean: das Argument aus Erklärvideo 1-1 des
Skripts, dass Kerne von Gruppenmorphismen abgeschlossen unter
Konjugation sind, und die Beobachtung aus Kapitel 17.3, dass
$`U \cdot N` für normales $`N` wieder eine Untergruppe ist.

# Das Mathlib-Wörterbuch

* Eine Untergruppe von `G` ist ein Term `U : Subgroup G`; die
  Mitgliedschaft schreibt sich `g ∈ U`.  Dass `U` unter Verknüpfung
  und Inversen abgeschlossen ist, sagen `U.mul_mem` und `U.inv_mem`.

* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein „Bündel“ aus
  der Abbildung und den Nachweisen `map_mul : φ (a·b) = φ a · φ b`
  (daraus folgen `map_one` und `map_inv`).  Der Kern heißt `φ.ker`;
  die Mitgliedschaft entpackt
  `MonoidHom.mem_ker : g ∈ φ.ker ↔ φ g = 1`.

* „`N` ist Normalteiler“ ist das Prädikat `N.Normal`; sein Feld
  `conj_mem` ist wörtlich die Bedingung des Skripts: für alle
  $`n \in N` und alle $`g` ist $`g \cdot n \cdot g^{-1} \in N`.

# Kerne sind abgeschlossen unter Konjugation

Aus Erklärvideo 1-1 des Skripts:

> Die Antwort lautet: Nein!  Nicht jede Untergruppe kann Kern eines
  Gruppenmorphismus sein.  Wenn es nämlich einen Gruppenmorphismus
  $`\varphi : G \to Q` mit $`H = \ker(\varphi)` gibt, dann gilt für
  alle $`h \in H` und alle $`g \in G` die Gleichung
  $`\varphi(g \cdot h \cdot g^{-1}) = \varphi(g) \cdot \varphi(h) \cdot \varphi(g)^{-1} = e`,
  wobei $`e` das neutrale Element von $`Q` bezeichnet.  Also ist
  stets $`g \cdot h \cdot g^{-1} \in H`.

```lean
theorem kern_konjugation {G Q : Type*} [Group G] [Group Q]
    (φ : G →* Q) {h : G} (hh : h ∈ φ.ker) (g : G) :
    g * h * g⁻¹ ∈ φ.ker := by
  -- Mitgliedschaft im Kern heißt: φ bildet auf 1 ab.
  rw [MonoidHom.mem_ker] at hh ⊢
  -- „… dann gilt für alle h ∈ H und alle g ∈ G die
  --  Gleichung φ(g·h·g⁻¹) = φ(g)·φ(h)·φ(g)⁻¹ = e …“
  calc φ (g * h * g⁻¹)
      = φ g * φ h * (φ g)⁻¹ := by
        rw [map_mul, map_mul, map_inv]
    _ = φ g * 1 * (φ g)⁻¹ := by rw [hh]
    _ = 1 := by rw [mul_one, mul_inv_cancel]
```

Mathlib kennt diese Aussage als Instanz
`MonoidHom.normal_ker : φ.ker.Normal`.  Das Skript fährt fort:
Untergruppen mit dieser Eigenschaft heißen _normale Untergruppen_
oder _Normalteiler_, und die Bedingung ist nicht nur notwendig,
sondern auch hinreichend — zu jedem Normalteiler existiert eine
Restklassengruppe.

# Die Restklassengruppe und ihre universelle Eigenschaft

Das Skript definiert die Restklassengruppe in Kapitel 17.3 über ihre
universelle Eigenschaft.  Mathlib stellt beides bereit: den
Quotienten `G ⧸ N` mit der Quotientenabbildung
`QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle Eigenschaft
als `QuotientGroup.lift` — gegeben ein Morphismus `α : G →* H` mit
`N ≤ α.ker` erhält man den induzierten Morphismus auf dem
Quotienten:

```lean
example {G H : Type*} [Group G] [Group H] (N : Subgroup G)
    [N.Normal] (α : G →* H) (hα : N ≤ α.ker) :
    G ⧸ N →* H :=
  QuotientGroup.lift N α
    fun _g hg => MonoidHom.mem_ker.mp (hα hg)
```

# Die Beobachtung: U·N ist eine Untergruppe

Beobachtung 17.3.5 des Skripts:

> Es sei $`G` eine Gruppe und es sei $`N \subset G` eine normale
  Untergruppe.  Weiter sei $`U \subset G` irgendeine Untergruppe.
  Dann ist $`U \cdot N = \{u \cdot n : u \in U,\ n \in N\}` wieder
  eine Untergruppe.  Zum Beweis müssen wir lediglich zeigen, dass
  $`U \cdot N` abgeschlossen unter der Gruppenoperation ist.  …  Wir
  wissen, dass $`N` normal ist.  Also ist
  $`\widetilde{n_1} := u_2^{-1} \cdot n_1 \cdot u_2 \in N` und es
  gilt $`n_1 \cdot u_2 = u_2 \cdot \widetilde{n_1}`.  Demnach ist
  $`u_1 n_1 u_2 n_2 = u_1 u_2 \cdot \widetilde{n_1} n_2 \in U \cdot N`.
  Fertig ist der Beweis.

Neu ist hier die Taktik `group`: Sie verrechnet Ausdrücke, die
allein mit den Gruppenaxiomen ineinander umgeformt werden können.
(Das $`\widetilde{n_1}` des Skripts heißt im Code `n₁'`.)

```lean
theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
    (hN : N.Normal) {u₁ n₁ u₂ n₂ : G}
    (hu₁ : u₁ ∈ U) (hn₁ : n₁ ∈ N)
    (hu₂ : u₂ ∈ U) (hn₂ : n₂ ∈ N) :
    ∃ u ∈ U, ∃ n ∈ N, u₁ * n₁ * (u₂ * n₂) = u * n := by
  -- „Wir wissen, dass N normal ist.  Also ist
  --  ñ₁ := u₂⁻¹·n₁·u₂ ∈ N …“
  set n₁' := u₂⁻¹ * n₁ * u₂ with hn₁'_def
  have hn₁' : n₁' ∈ N := hN.conj_mem' n₁ hn₁ u₂
  -- „… und es gilt n₁·u₂ = u₂·ñ₁.“
  have hswap : n₁ * u₂ = u₂ * n₁' := by
    rw [hn₁'_def]; group
  -- „Demnach ist u₁n₁u₂n₂ = u₁u₂·ñ₁n₂ ∈ U·N.“
  refine ⟨u₁ * u₂, U.mul_mem hu₁ hu₂,
    n₁' * n₂, N.mul_mem hn₁' hn₂, ?_⟩
  calc u₁ * n₁ * (u₂ * n₂)
      = u₁ * (n₁ * u₂) * n₂ := by group
    _ = u₁ * (u₂ * n₁') * n₂ := by rw [hswap]
    _ = u₁ * u₂ * (n₁' * n₂) := by group
```

# Übungsaufgabe

Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit unter der
Verknüpfung zu zeigen — prüfen Sie den verschwiegenen Teil selbst
nach: $`U \cdot N` ist auch abgeschlossen unter Inversen.  Tipp:
$`(u \cdot n)^{-1} = u^{-1} \cdot (u \cdot n^{-1} \cdot u^{-1})`,
und der zweite Faktor liegt nach `conj_mem` in $`N`.  Öffnen Sie `AlgebraInLean/Quotients.lean` und
ersetzen Sie das `sorry` durch einen Beweis.

```lean
theorem inv_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
    (hN : N.Normal) {u n : G} (hu : u ∈ U) (hn : n ∈ N) :
    ∃ u' ∈ U, ∃ n' ∈ N, (u * n)⁻¹ = u' * n' := by
  sorry
```