From 3c800a630d457c4ccbc83df162babe46283ef7cb Mon Sep 17 00:00:00 2001 From: sxhya Date: Thu, 30 Jan 2025 20:58:20 +0100 Subject: [PATCH] Proving two definitions of a factor agree --- src/Algebra/Group/QuotientProperties.ard | 51 +++++++++++++++++++++++- 1 file changed, 49 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Group/QuotientProperties.ard b/src/Algebra/Group/QuotientProperties.ard index 36918dc8..26150a6c 100644 --- a/src/Algebra/Group/QuotientProperties.ard +++ b/src/Algebra/Group/QuotientProperties.ard @@ -62,28 +62,33 @@ 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, @@ -91,6 +96,7 @@ \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,11 +106,15 @@ \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)) => @@ -112,6 +122,32 @@ 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-}