Proving two definitions of a factor agree

src/Algebra/Group/QuotientProperties.ard

@@ -62,35 +62,41 @@
     univ_hom (in~ x) ==< idp >== f x `qed)
 }
 
+{- | Let G and H be groups, and $f \colon G \to H$ be a homomorphism. -}
 \class TheoremA \extends QuotientUnivProperty {
   | N => f.Ker
   | p => SubGroupMeetSemilattice.<=-refl
 
+  {- | The image of $f$ is isomorphic to the quotient group $G/Ker(f)$ -}
   \func statement : Iso {_} {G // f.Ker} {f.Im.struct} univ_img => univ_img.asIso
       (\lam {a a' : SubGroup.LeftCosetSet {f.Ker}} p => \case \elim a, \elim a', p \with {
         | in~ b1, in~ b2, p2 => ~-equiv {G} b1 b2 (GroupHom.same-images-test (pmap (\lam x => x.1) p2))
       }, univ_map_surj)
 
+  {- | In particular, if $f$ is surjective then $H$ is isomorphic to $G/Ker(f)$. -}
   \func statement' (p : isSurj f) : Iso {_} {G // f.Ker} {H} ((GroupHom.im {f}) ∘ univ_img) =>
     Iso.composite statement (GroupHom.im.im_iso p)
 }
 
-{- | The quotient groups $SN/N$ and $S/(S \cap N)$ are isomorphic.-}
+{- | Let $G$ be a group. Let $S$ be a subgroup of $G$, and let $N$ be a normal subgroup of $G$. -}
 \class TheoremB (G : Group) (S : SubGroup G) (N : NormalSubGroup G) {
   \func SN : SubGroup G => S *F N
 
+  {- | $N$ can be considered as a normal subgroup of $SN$. -}
   \func N-as-sbgp-SN : NormalSubGroup SN.struct => *F.sbgp-N S N
 
-  {- | Morphism S -> SN -> SN/N -}
+  {- | Morphism f : S -> SN -> SN/N -}
   \func f : GroupHom S.struct N-as-sbgp-SN.QuotientGroup => (NormalSubGroup.quotient {N-as-sbgp-SN}) ∘ *F.embedS {G} {S} {N}
 
+  {- | f is surjective -}
   \lemma f-surj : isSurj f =>
     \lam y => \case \elim y \with {
       | in~ (x, inP (s, n, p)) => inP (s,
         \let | A0 : N (inverse s.1 * x) => rewrite (p, inv *-assoc, inverse-left, ide-left) n.2
         \in (~-pequiv {SubSet.S {N-as-sbgp-SN}} {(~) {SubGroup.leftAdjacency {N-as-sbgp-SN}}}) A0)
     }
 
+  {- | One has $Ker(f) = S \cap N$ -}
   \lemma Kerf=S-cap-N : f.Ker = S ∩.as-sbgp-1' N => SubGroup.normal-subgroup-eq {S.struct}
       (\lam s => (\lam p => (s.2, NormalSubGroup.quotient.Ker->contains {N-as-sbgp-SN} (*F.embedS {G} {S} {N} s) p),
                   \lam p => NormalSubGroup.quotient.contains->Ker {N-as-sbgp-SN} (s.1, inP (s, N.struct.ide, inv ide-right)) p.2))
@@ -100,18 +106,48 @@
   \func statement : Iso {_} {S.struct // f.Ker} {N-as-sbgp-SN.QuotientGroup} ((GroupHom.im {f}) ∘ thmA.univ_img ) =>
     TheoremA.statement' {thmA} f-surj
 
+  {- | The quotient groups $SN/N$ and $S/(S \cap N)$ are isomorphic -}
   \func statement' : Iso {_} {S.struct // (S ∩.as-sbgp-1' N)} {SN.struct // N-as-sbgp-SN} =>
     transport (\lam Q => Iso {_} {S.struct // Q} {SN.struct // N-as-sbgp-SN}) Kerf=S-cap-N statement
 }
 
+{- | Let $G$ be a group, and $N$, $K$ be normal subgroups of $G$ such that $N \subseteq K$. -}
 \class TheoremC (G : Group) (N : NormalSubGroup G) (K : NormalOverGroup { | G => G | H => N }) {
+  \func N-as-sbgp-K : NormalSubGroup K.struct => SubGroup.subgroup-res-normal N K (\lam x => K.isOvergroup x.1 x.2)
+
   \func K/N : NormalSubGroup (G // N) \cowith {
     | SubGroup => GroupHom.sbgp-image {NormalSubGroup.quotient {N}} K
     | isNormal (in~ g) {in~ h} (inP (_, c, p)) =>
       inP (conjugate g h, K.isNormal g (rewrite (inv *-assoc, inverse-right, ide-left) in
         contains_* c (isOvergroup {K} _ (NormalSubGroup.quotient.Ker->contains {N} _ (GroupHom.same-images-test p)))), idp)
   }
 
+  -- two obvious definitions of K/N agree
+  \func K/N-def-compatible : Iso {GroupCat} {NormalSubGroup.QuotientGroup {N-as-sbgp-K}}
+                                            {SubGroup.struct {GroupHom.sbgp-image {NormalSubGroup.quotient {N}} K}} \cowith {
+    | f => \new GroupHom {
+      | func x => \case \elim x \with {
+        | in~ (x : G, c) => (in~ x, inP (x, c, idp))
+        | ~-equiv x y r => ext (path (~-equiv x.1 y.1 r))
+      }
+      | func-* {x} {y} => \case \elim x, \elim y \with {
+        | in~ a, in~ a1 => ext idp
+      }
+    }
+    | hinv => \new GroupHom {
+      | func x => \scase \elim x \with {
+        | (in~ x1, inP (x, c, p)) => in~ (x, c)
+        | (~-equiv x y r i, inP (x1, c, p)) => in~ (x1, c)
+        | (in~ x, truncP (inP (x1, c1, p1)) (inP (x2, c2, p2)) i) => ~-equiv _ _ (Quotient.equalityEquiv _ (p1 *> inv p2)) i
+      }
+      | func-* {x} {y} => \case \elim x, \elim y \with {
+        | (in~ x, inP (x1, c, p)), (in~ y, inP (y1, d, q)) => unfold (SubGroup.struct.*) ({?})
+      }
+    }
+    | hinv_f => {?}
+    | f_hinv => {?}
+  }
+
   \func univ : GroupHom G ((G // N) // K/N) => K/N.quotient ∘ N.quotient
 
   \lemma univ_surj : isSurj univ => isSurj.comp (NormalSubGroup.quotient.surj {N}) (NormalSubGroup.quotient.surj {K/N})
@@ -147,6 +183,17 @@
       | inP (x, c, p) => rewrite (inv *-assoc, inverse-right, ide-left) in contains_* c (OverGroup.isOvergroup {K} _
           (rewrite NormalSubGroup.quotient.quotient-Ker in GroupHom.same-images-test p))
     }, \lam c => inP (g, c, idp))) }
+
+  \func statement_normal : QEquiv {NormalSubGroup (G // N)} {NormalOverGroup {| G => G | H => N }} \cowith {
+    | f Q => \new NormalOverGroup {
+      | OverGroup => TheoremD.statement.f Q
+      | isNormal g h-in-Q => \let | q => NormalSubGroup.quotient {N} \in
+        unfold conjugate (rewrite (func-* {q}, func-* {q} {g}, GroupHom.func-inverse {q}) (NormalSubGroup.isNormal {Q} (in~ g) h-in-Q))
+    }
+    | ret Q => TheoremC.K/N {\new TheoremC G N Q}
+    | ret_f Q => ext NormalSubGroup { | SubGroup => statement.ret_f Q}
+    | f_sec Q => ext NormalOverGroup {  | OverGroup => statement.f_sec Q}
+  }
 }
 
 {- | Now we apply all of these universal properties to the case when $N = \ker f$ and we get the first isomorphism theorem in the end-}