-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
9 changed files
with
420 additions
and
13 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -4,6 +4,7 @@ | |
| /meta/.idea/ | ||
| bin | ||
| *.iml | ||
| *DS_Store* | ||
|
|
||
| # Created by https://www.gitignore.io/api/vim | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| \import Algebra.Group | ||
| \import Algebra.Group.GSet.GSet | ||
| \import Algebra.Group.Sub | ||
| \import Category | ||
| \import Category.Meta | ||
| \import Function (isInj, isSurj) | ||
| \import Function.Meta ($) | ||
| \import Paths | ||
| \import Paths.Meta | ||
| \import Relation.Equivalence | ||
| \import Set | ||
| \import Set.Category | ||
|
|
||
| \record EquivariantMap (G : Group) \extends SetHom{ | ||
| \override Dom : GroupAction G | ||
| \override Cod : GroupAction G | ||
| | func-** {e : Dom} {g : G} : func (g ** e) = g ** func e -- equivariance | ||
|
|
||
| \func isIso => \Sigma (isSurj func) (isInj func) | ||
| } | ||
|
|
||
| \func id-equivar {G : Group} (X : GroupAction G) : EquivariantMap G { | Dom => X | Cod => X} \cowith | ||
| | func (x : X) => x | ||
| | func-** {x : X} {g : G} => idp | ||
|
|
||
| \instance GSet (G : Group) : Cat (GroupAction G) | ||
| | Hom A B => EquivariantMap G { | Dom => A | Cod => B} | ||
| | id X => id-equivar X | ||
| | o {x y z : GroupAction G} (g : EquivariantMap G y z) (f : EquivariantMap G x y) => \new EquivariantMap G { | ||
| | func (a : x) => g (f a) | ||
| | func-** {a : x} {h : G} => | ||
| g ( f (h ** a)) ==< pmap g func-** >== | ||
| g (h ** f a) ==< func-** >== | ||
| h ** (g (f a)) `qed | ||
| } | ||
| | id-left => idp | ||
| | id-right => idp | ||
| | o-assoc => idp | ||
| | univalence => sip \lam e _ => exts \lam g x => func-** {e} | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| \import Algebra.Group | ||
| \import Algebra.Group.Sub | ||
| \import Algebra.Meta | ||
| \import Algebra.Monoid | ||
| \import Algebra.Monoid.Sub | ||
| \import Algebra.Pointed | ||
| \import Equiv | ||
| \import Function | ||
| \import Function.Meta ($) | ||
| \import Logic | ||
| \import Logic.Meta | ||
| \import Paths | ||
| \import Paths.Meta | ||
| \import Relation.Equivalence | ||
| \import Set | ||
| \import Algebra.Monoid | ||
| \import Set.Category | ||
|
|
||
| \class GroupAction (G : Group) \extends BaseSet { | ||
| | \infixl 8 ** : G -> E -> E -- priority should be bigger than that of "+" in LModule (=7) | ||
| | **-assoc {m n : G} {e : E} : m ** (n ** e) = (m * n) ** e | ||
| | id-action {e : E} : ide ** e = e | ||
|
|
||
| \func Stabilizer (s : E) : SubGroup G \cowith | ||
| | contains m => m ** s = s | ||
| | contains_* {m n : G} (p : m ** s = s) (q : n ** s = s) => | ||
| (m * n) ** s ==< inv **-assoc >== | ||
| m ** (n ** s) ==< pmap (\lam x => m ** x) q >== | ||
| m ** s ==< p >== | ||
| s `qed | ||
|
|
||
| | contains_ide => id-action | ||
|
|
||
| | contains_inverse {m : G} (p : m ** s = s) => | ||
| inverse m ** s ==< pmap (\lam x => inverse m ** x) (inv p) >== | ||
| inverse m ** (m ** s) ==< **-assoc >== | ||
| (inverse m * m) ** s ==< pmap (\lam x => x ** s) inverse-left >== | ||
| ide ** s ==< id-action >== | ||
| s `qed | ||
|
|
||
| \func choosePoint (e : E) => ActionBySubgroup (Stabilizer e) | ||
| } | ||
|
|
||
| \class TransitiveGroupAction \extends GroupAction { | ||
| | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v') | ||
| } | ||
| \func ActionBySubgroup {G : Group} (H : SubGroup G) : GroupAction G \cowith | ||
| | E => H.Cosets | ||
| | ** (g : G) (e : H.Cosets) : H.Cosets \with { | ||
| | g, in~ a => in~ (g * a) | ||
| | g, ~-equiv x y r => in~ (g * x) ==< H.invariant-right-multiplication (H.equivalence-to-1 r) >== | ||
| in~ (g * x * (inverse x * y)) ==< pmap in~ (trivialRelation g x y ) >== in~ (g * y) `qed | ||
| } | ||
| | **-assoc {m n : G} {e : H.Cosets} : m ** (n ** e) = (m * n) ** e => \case \elim e \with{ | ||
| | in~ a => m ** (n ** in~ a) ==< pmap (m **) {n ** in~ a} {in~ (n * a)} idp >== | ||
| m ** in~ (n * a) ==< idp >== | ||
| in~ (m * (n * a)) ==< pmap in~ (inv *-assoc) >== | ||
| in~ ((m * n) * a) ==< idp >== | ||
| (m * n) ** in~ a `qed | ||
| } | ||
| | id-action {e : H.Cosets} : ide ** e = e => \case \elim e \with{ | ||
| | in~ a => ide ** in~ a ==< idp >== | ||
| in~ (ide * a) ==< pmap in~ ide-left >== | ||
| in~ a `qed | ||
| } | ||
| \where \func trivialRelation (g x y : G) : g * x * (inverse x * y) = g * y => | ||
| g * x * (inverse x * y) ==< *-assoc >== | ||
| g * (x * (inverse x * y)) ==< pmap (g *) (inv *-assoc) >== | ||
| g * ((x * inverse x) * y) ==< pmap (\lam z => g *( z * y)) inverse-right >== | ||
| g * (ide * y) ==< pmap (g *) ide-left >== | ||
| g * y `qed | ||
|
|
||
|
|
||
| \instance TransitiveActionBySubgroup {G : Group} (H : SubGroup G) : TransitiveGroupAction G | ||
| | GroupAction => ActionBySubgroup H | ||
| | trans (v v' : H.Cosets) : ∃ (g : G) (g ActionBySubgroup.** v = v') => \case \elim v, \elim v'\with{ | ||
| | in~ a, in~ a1 => inP(a1 * inverse a , | ||
| in~ (a1 * inverse a * a) ==< pmap in~ *-assoc >== | ||
| in~ (a1 * (inverse a * a)) ==< pmap (\lam z => in~ (a1 * z)) inverse-left >== | ||
| in~ (a1 * ide) ==< pmap in~ ide-right >== | ||
| in~ a1 `qed | ||
| ) | ||
| } | ||
|
|
||
| -- action by conjugating its own elements | ||
| \func conjAction (G : Group) : GroupAction G \cowith | ||
| | E => G | ||
| | ** (g : G) => conjugate g | ||
| | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e => | ||
| conjugate m (conjugate n e) ==< pmap (conjugate m) idp >== | ||
| conjugate m (n * e * inverse n ) ==< idp >== | ||
| m * (n * e * inverse n ) * inverse m ==< lemma-par >== | ||
| (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >== | ||
| (m * n) * e * (inverse (m * n)) ==< idp >== | ||
| conjugate (m * n) e `qed | ||
| | id-action {e : G} : conjugate ide e = e => conjugate-via-id e | ||
| \where \lemma lemma-par {a b c d e : G} : a * (b * c * d) * e = (a * b) * c * (d * e) => equation |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,147 @@ | ||
| \import Algebra.Group | ||
| \import Algebra.Group.Sub | ||
| \import Algebra.Monoid | ||
| \import Algebra.Monoid.Category | ||
| \import Algebra.Pointed | ||
| \import Algebra.Pointed.Category | ||
| \import Category (Cat, Precat) | ||
| \import Category.Functor | ||
| \import Category.Meta | ||
| \import Category.Subcat | ||
| \import Equiv | ||
| \import Function | ||
| \import Function.Meta | ||
| \import Logic | ||
| \import Logic.Meta | ||
| \import Paths | ||
| \import Paths.Meta | ||
| \import Relation.Equivalence | ||
| \import Set.Category | ||
| \import Algebra.Group.Category | ||
| \open Group | ||
| \open Algebra.Group.Sub | ||
|
|
||
| \func \infix 7 // (G : Group) (H : NormalSubGroup G) : Group => H.quotient | ||
|
|
||
| {- | properties needed from a commutative triangle $$X \to Y \to Z$$ in the category of groups -} | ||
| \class GroupTriangle \noclassifying (X Y Z : Group) (f : GroupHom X Y) (g : GroupHom Y Z) (h : GroupHom X Z)(comm : h = g GroupCat.∘ f){ | ||
|
|
||
| \func surjectivity-2-out-3 (p : isSurj h) (q : isSurj f) : isSurj g | ||
| => \lam (z : Z) => surjectivity-2-out-3-pw p q z | ||
|
|
||
| \func surjectivity-2-out-3-pw (p : isSurj h) (q : isSurj f) (z : Z): ∃(y : Y) (g y = z) => | ||
| \case p z \with { | ||
| | inP a => inP (f a.1, g (f a.1) ==< helper >== h a.1 ==< a.2 >== z `qed) | ||
| } | ||
| \where \func helper {a : X} : g (f a) = h a => | ||
| g (f a) ==< idp >== | ||
| (g GroupCat.∘ f) a ==< pmap (\lam (e : GroupHom X Z) => e a) (inv comm) >== | ||
| h a `qed | ||
| } | ||
|
|
||
|
|
||
| \class UniversalGroupQuotient \noclassifying (G H : Group)(f : GroupHom G H)(N : NormalSubGroup G)(p : N SubGroupPreorder.<= f.Kernel){ | ||
| {- | a set function that having $G, H$ and $f : G \to H$ and a | ||
| - normal subgroup $N \leq G$ s.t. $N \leqslant \ker(f)$ produces for each element of $G/N$ an element of $H$. | ||
| - One gets a diagram of the form | ||
| - $$G \xrightarrow{\pi} G/N \xrightarrow{\text{this\, function}} H $$ -} | ||
| \func universalQuotientMorphismSetwise (a : N.quotient) : H \elim a | ||
| | in~ n => f n | ||
| | ~-equiv y x r => equality-check (inverse (f y) * (f x) ==< pmap (\lam y => y * (f x)) (inv f.func-inverse) >== | ||
| f (inverse y) * (f x) ==< inv func-* >== | ||
| f (inverse y * x) ==< lemma' f N p r >== ide `qed) | ||
| \where | ||
| \lemma lemma' {x y : G} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) | ||
| (r : N.contains ((inverse y) * x)) : f (inverse y * x) = ide => | ||
| f (inverse y * x) ==< p ((inverse y) * x) r >== ide `qed | ||
|
|
||
|
|
||
| {- | this a synonym for universalQuotientMorphismSetwise used because it is shorter-} | ||
| \func uqms => universalQuotientMorphismSetwise | ||
|
|
||
|
|
||
| {- | this is a proof that in the previous assumptions the function | ||
| - universalQuotientMorphismSetwise is multiplicative -} | ||
| \func universalQuotientMorphismMultiplicative (x y : N.quotient) : uqms (x N.quotient.* y) = (uqms x) * (uqms y) \elim x, y | ||
| | in~ a, in~ a1 => uqms ((in~ a) N.quotient.* (in~ a1)) ==< idp >== | ||
| uqms (in~ (a * a1)) ==< idp >== | ||
| f (a * a1) ==< f.func-* >== | ||
| (f a) * (f a1) ==< pmap ((f a)*) idp >== | ||
| (f a) * uqms (in~ a1) ==< pmap (\lam x => x * uqms (in~ a1)) idp >== | ||
| (uqms (in~ a)) * (uqms (in~ a1)) `qed | ||
|
|
||
|
|
||
| {- | this is a function which gives the homomorphism in the universal property | ||
| - of quotient groups. Basically, it proves | ||
| - that the function universalQuotientMorphismSetwise | ||
| - indeed gives a group homomorphism. Thus the arrow $G/N \xrightarrow{\text{uqms}} H$ indeed lies in Group-} | ||
| \func universalQuotientMorph : GroupHom (G // N) H \cowith | ||
| | func => uqms | ||
| | func-ide => uqms N.quotient.ide ==< idp >== uqms (in~ 1) ==< idp >== f ide ==< f.func-ide >== ide `qed | ||
| | func-* {x y : N.quotient} => universalQuotientMorphismMultiplicative x y | ||
|
|
||
|
|
||
| \lemma universalQuotientProperty : universalQuotientMorph GroupCat.∘ quotient-map = f | ||
| => exts (\lam (x : G) => (universalQuotientMorph GroupCat.∘ quotient-map) x ==< idp >== | ||
| universalQuotientMorph (quotient-map x) ==< idp >== | ||
| universalQuotientMorph (in~ x) ==< idp >== f x `qed) | ||
| } | ||
|
|
||
| {- | 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-} | ||
| \class FirstIsomorphismTheorem \noclassifying (G : Group) (H : Group) (f : GroupHom G H) { | ||
|
|
||
| \func UniversalProperties : UniversalGroupQuotient {| G => G | H => H | f => f} \cowith | ||
| | N => f.Kernel | ||
| | p => SubGroupPreorder.<=-refl | ||
|
|
||
| \func Triangle : GroupTriangle \cowith | ||
| | X => G | ||
| | Y => G // f.Kernel | ||
| | Z => H | ||
| | f => quot | ||
| | g => UniversalProperties.universalQuotientMorph | ||
| | h => f | ||
| | comm => UniversalProperties.universalQuotientProperty | ||
|
|
||
| \func univ : GroupHom (G // f.Kernel) H => UniversalProperties.universalQuotientMorph | ||
| \func quot : GroupHom G (G // f.Kernel) => quotient-map | ||
|
|
||
| \lemma universalKerProp : univ GroupCat.∘ quot = f | ||
| => UniversalProperties.universalQuotientProperty | ||
|
|
||
| \lemma universalQuotientKernel (g : G // f.Kernel) | ||
| (q : univ g = ide) : g = f.Kernel.quotient.ide | ||
| => \case g \as b, idp : g = b \return b = f.Kernel.quotient.ide\with{ | ||
| | in~ a, p => inv (f.Kernel.criterionForKernel a (universalQuotientKernel' a (transport (\lam z => univ z = ide) p q)) | ||
| ) | ||
| } | ||
| \where{ | ||
| \func helper-1 (a : G) | ||
| (q : univ (in~ a) = ide) : in~ a = f.Kernel.quotient.ide => | ||
| inv (f.Kernel.criterionForKernel a (universalQuotientKernel' a q)) | ||
| } | ||
|
|
||
|
|
||
| \func evidTrivKer : univ.TrivialKernel => | ||
| \lam {g : G // f.Kernel} (p : univ.Kernel.contains g) => universalQuotientKernel g p | ||
|
|
||
| \lemma universalQuotientKernel' (a : G) | ||
| (q : univ (in~ a) = ide) : f.Kernel.contains a | ||
| => | ||
| f a ==< inv (technical-helper a) >== | ||
| univ (in~ a) ==< q >== | ||
| ide `qed | ||
| \where \lemma technical-helper (a : G) : univ (in~ a) = f a => | ||
| univ (in~ a) ==< pmap univ {in~ a} {quot a} idp >== | ||
| univ (quot a) ==< idp >== | ||
| (univ GroupCat.∘ quot) a ==< pmap (\lam (z : GroupHom G H) => z a) universalKerProp >== | ||
| f a `qed | ||
|
|
||
|
|
||
| \lemma univKer-mono : isInj univ.func => univ.Kernel-injectivity-test evidTrivKer | ||
|
|
||
| \func univKer-epi (p : isSurj f): isSurj univ | ||
| => Triangle.surjectivity-2-out-3 p f.Kernel.quotIsSurj | ||
|
|
||
| \func FirstIsoTheorem (p : isSurj f) : univ.isIsomorphism => (univKer-mono, univKer-epi p) | ||
| } |
Oops, something went wrong.