From cd5bfdb778881a106c03b77f6749befa209e5c8d Mon Sep 17 00:00:00 2001 From: artem Date: Sun, 24 Mar 2024 03:47:15 +0200 Subject: [PATCH] upd names and future staff --- .gitignore | 1 + src/Algebra/Group/Category.ard | 16 +++++++++++++- src/Algebra/Group/GSet.ard | 4 +++- src/Algebra/Group/GSetCat.ard | 18 +++++++++------ src/Algebra/Group/QuotientProperties.ard | 28 ++++++++++++------------ src/Algebra/Group/Sub.ard | 7 +----- src/Algebra/Monoid/Category.ard | 9 ++++++++ src/Algebra/Pointed/Category.ard | 4 ++++ 8 files changed, 58 insertions(+), 29 deletions(-) diff --git a/.gitignore b/.gitignore index 913bf564..53618c15 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ /meta/.idea/ bin *.iml +*DS_Store* # Created by https://www.gitignore.io/api/vim diff --git a/src/Algebra/Group/Category.ard b/src/Algebra/Group/Category.ard index de738c0d..02d404d3 100644 --- a/src/Algebra/Group/Category.ard +++ b/src/Algebra/Group/Category.ard @@ -95,7 +95,21 @@ | func-* => idp } - +--\instance ImageMonoid (f : MonoidHom) : Monoid +-- | Pointed => ImageMulPointed f +-- | * a b => (a.1 * b.1, \case a.2, b.2 \with { +-- | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2) +-- }) +-- | ide-left => ext ide-left +-- | ide-right => ext ide-right +-- | *-assoc => ext *-assoc + +\instance ImageGroup (f : GroupHom) : Group + | Monoid => ImageMonoid f + | inverse (x, p) => (inverse x, get-inverse p) + | inverse-left => {?} + | inverse-right => {?} + \where \func get-inverse{x : f.Cod} (p : ∃ (g : f.Dom)(f g = x)) : ∃ (g : f.Dom)(f g = inverse x) => {?} \record AddGroupHom \extends AddMonoidHom { \override Dom : AddGroup diff --git a/src/Algebra/Group/GSet.ard b/src/Algebra/Group/GSet.ard index 28b914d9..7508865c 100644 --- a/src/Algebra/Group/GSet.ard +++ b/src/Algebra/Group/GSet.ard @@ -36,13 +36,15 @@ (inverse m * m) ** s ==< pmap (\lam x => x ** s) inverse-left >== ide ** s ==< id-action >== s `qed + + \func choosePoint (e : E) => action-by-subgroup (Stabilizer e) } \class TransitiveGroupAction \extends GroupAction { | trans : \Pi (v v' : E) -> ∃ (g : G) (g ** v = v') } -\func action-by-subgroup (G : Group) (H : SubGroup G) : GroupAction G \cowith +\func action-by-subgroup {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) diff --git a/src/Algebra/Group/GSetCat.ard b/src/Algebra/Group/GSetCat.ard index 0769c955..c4eff60a 100644 --- a/src/Algebra/Group/GSetCat.ard +++ b/src/Algebra/Group/GSetCat.ard @@ -1,34 +1,38 @@ \import Algebra.Group \import Algebra.Group.GSet \import Category +\import Category.Meta \import Function (isInj, isSurj) \import Function.Meta ($) \import Paths +\import Paths.Meta \import Set \import Set.Category \record EquivariantMaps (G : Group) \extends SetHom{ \override Dom : GroupAction G \override Cod : GroupAction G - | **-equiv {e : Dom} {g : G} : func (g ** e) = g ** func e + | 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) : EquivariantMaps G { | Dom => X | Cod => X} \cowith | func (x : X) => x - | **-equiv {x : X} {g : G} => idp + | func-** {x : X} {g : G} => idp -\instance GSet (G : Group) : Precat (GroupAction G) +\instance GSet (G : Group) : Cat (GroupAction G) | Hom A B => EquivariantMaps G { | Dom => A | Cod => B} | id X => id-equivar X | o {x y z : GroupAction G} (g : EquivariantMaps G y z) (f : EquivariantMaps G x y) => \new EquivariantMaps G { | func (a : x) => g (f a) - | **-equiv {a : x} {h : G} => - g ( f (h ** a)) ==< pmap g **-equiv >== - g (h ** f a) ==< **-equiv >== + | 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 \ No newline at end of file + | o-assoc => idp + | univalence => sip \lam e _ => exts \lam g x => func-** {e} \ No newline at end of file diff --git a/src/Algebra/Group/QuotientProperties.ard b/src/Algebra/Group/QuotientProperties.ard index 5a90adc1..ab5307db 100644 --- a/src/Algebra/Group/QuotientProperties.ard +++ b/src/Algebra/Group/QuotientProperties.ard @@ -21,9 +21,9 @@ \open Group \open Algebra.Group.Sub -\func universal-quotient-morphism-setwise {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) - (p : N SubGroupPreorder.<= f.Kernel) - (a : N.quotient) : H \elim a +\func universalQuotientMorphismSetwise {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) + (p : N SubGroupPreorder.<= f.Kernel) + (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-* >== @@ -33,27 +33,27 @@ (r : N.contains ((inverse y) * x)) : f (inverse y * x) = ide => f (inverse y * x) ==< p ((inverse y) * x) r >== ide `qed -\func uqms {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) => universal-quotient-morphism-setwise f N p +\func uqms {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) => universalQuotientMorphismSetwise f N p -\func universal-quotient-morphism-multiplicative {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) - (x y : N.quotient) : uqms f N p (x N.quotient.* y) = (uqms f N p x) * (uqms f N p y) \elim x, y +\func universalQuotientMorphismMultiplicative {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel) + (x y : N.quotient) : uqms f N p (x N.quotient.* y) = (uqms f N p x) * (uqms f N p y) \elim x, y | in~ a, in~ a1 => uqms f N p ((in~ a) N.quotient.* (in~ a1)) ==< idp >== uqms f N p (in~ (a * a1)) ==< idp >== f (a * a1) ==< f.func-* >== (f a) * (f a1) ==< pmap ((f a)*) idp >== (f a) * uqms f N p (in~ a1) ==< pmap (\lam x => x * uqms f N p (in~ a1)) idp >== (uqms f N p (in~ a)) * (uqms f N p (in~ a1)) `qed -\func universal-quotient-morph {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) - (p : N SubGroupPreorder.<= f.Kernel) : GroupHom N.quotient H \cowith +\func universalQuotientMorph {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) + (p : N SubGroupPreorder.<= f.Kernel) : GroupHom N.quotient H \cowith | func => uqms f N p | func-ide => uqms f N p N.quotient.ide ==< idp >== uqms f N p (in~ 1) ==< idp >== f ide ==< f.func-ide >== ide `qed - | func-* {x y : N.quotient} => universal-quotient-morphism-multiplicative f N p x y + | func-* {x y : N.quotient} => universalQuotientMorphismMultiplicative f N p x y -\lemma universal-quotient-property {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) - (p : N SubGroupPreorder.<= f.Kernel) : (universal-quotient-morph f N p) GroupCat.∘ quotient-map = f - => exts (\lam (x : G) => ((universal-quotient-morph f N p) GroupCat.∘ quotient-map) x ==< idp >== - (universal-quotient-morph f N p) (quotient-map x) ==< idp >== - (universal-quotient-morph f N p) (in~ x) ==< idp >== f x `qed) +\lemma universalQuotientProperty {G H : Group} (f : GroupHom G H) (N : NormalSubGroup G) + (p : N SubGroupPreorder.<= f.Kernel) : (universalQuotientMorph f N p) GroupCat.∘ quotient-map = f + => exts (\lam (x : G) => ((universalQuotientMorph f N p) GroupCat.∘ quotient-map) x ==< idp >== + (universalQuotientMorph f N p) (quotient-map x) ==< idp >== + (universalQuotientMorph f N p) (in~ x) ==< idp >== f x `qed) diff --git a/src/Algebra/Group/Sub.ard b/src/Algebra/Group/Sub.ard index f7512050..dce27c86 100644 --- a/src/Algebra/Group/Sub.ard +++ b/src/Algebra/Group/Sub.ard @@ -32,13 +32,8 @@ \func Cosets => Quotient (equivalence.~) \lemma invariant-right-multiplication {x y : S} (p : 1 equivalence.~ y) : in~{S} {equivalence.~} x = in~ {S} {equivalence.~} (x * y) => {?} --- in~ {S} {equivalence.~} x = in~ {S} {equivalence.~} (x * y) => --- in~ {S} {equivalence.~} x ==< pmap (in~ {S} {equivalence.~}) (inv ide-right) >== --- in~ {S} {equivalence.~} (x * 1) ==< - - \lemma equivalence-to-1 {x y : S} (p : x equivalence.~ y) : 1 equivalence.~ inverse x * y - => {?} + \lemma equivalence-to-1 {x y : S} (p : x equivalence.~ y) : 1 equivalence.~ inverse x * y => {?} } \where { \func cStruct {G : CGroup} (S : SubGroup G) : CGroup \cowith diff --git a/src/Algebra/Monoid/Category.ard b/src/Algebra/Monoid/Category.ard index 3de25a50..8c0bab97 100644 --- a/src/Algebra/Monoid/Category.ard +++ b/src/Algebra/Monoid/Category.ard @@ -251,6 +251,15 @@ | zro-right => ext zro-right | +-assoc => ext +-assoc +\instance ImageMonoid (f : MonoidHom) : Monoid + | Pointed => ImageMulPointed f + | * a b => (a.1 * b.1, \case a.2, b.2 \with { + | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2) + }) + | ide-left => ext ide-left + | ide-right => ext ide-right + | *-assoc => ext *-assoc + \func ImageMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith | AddPointedHom => ImagePointedLeftHom f | func-+ => ext func-+ diff --git a/src/Algebra/Pointed/Category.ard b/src/Algebra/Pointed/Category.ard index 02e20239..6bc7f28a 100644 --- a/src/Algebra/Pointed/Category.ard +++ b/src/Algebra/Pointed/Category.ard @@ -66,6 +66,10 @@ \instance ImageAddPointed (f : AddPointedHom) : AddPointed (Image f) | zro => (0, inP (0, func-zro)) +\instance ImageMulPointed (f : PointedHom) : Pointed (Image f) + | ide => (ide, inP (ide, func-ide)) + + \func ImagePointedLeftHom (f : AddPointedHom) : AddPointedHom f.Dom (ImageAddPointed f) \cowith | func a => (f a, inP (a, idp)) | func-zro => ext func-zro