Move GSet and make some functions into lemmas

JetBrains · Jul 5, 2024 · 5e3d345 · 5e3d345
1 parent f8b4348
commit 5e3d345
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 10 deletions.
diff --git a/src/Algebra/Group/GSet/GSet.ard → src/Algebra/Group/GSet.ard b/src/Algebra/Group/GSet/GSet.ard → src/Algebra/Group/GSet.ard
diff --git a/src/Algebra/Group/GSet/Category.ard b/src/Algebra/Group/GSet/Category.ard
@@ -1,5 +1,5 @@
 \import Algebra.Group
-\import Algebra.Group.GSet.GSet
+\import Algebra.Group.GSet
 \import Algebra.Group.Sub
 \import Category
 \import Category.Meta

diff --git a/src/Algebra/Group/QuotientProperties.ard b/src/Algebra/Group/QuotientProperties.ard
@@ -26,14 +26,14 @@
 {- | 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
+  \lemma 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) =>
+    \lemma 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 =>
+      \where \lemma 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
@@ -62,7 +62,7 @@
 
   {- | 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
+  \lemma 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-* >==
@@ -116,13 +116,12 @@
                         )
     }
     \where{
-      \func helper-1 (a : G)
-                     (q : univ (in~ a) = ide) : in~ a = f.Kernel.quotient.ide =>
+      \lemma 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 =>
+  \lemma evidTrivKer : univ.TrivialKernel =>
     \lam {g : G // f.Kernel} (p : univ.Kernel.contains g) => universalQuotientKernel g p
 
   \lemma universalQuotientKernel'  (a : G)
@@ -140,8 +139,8 @@
 
   \lemma univKer-mono : isInj univ.func => univ.Kernel-injectivity-test evidTrivKer
 
-  \func univKer-epi (p : isSurj f): isSurj univ
+  \lemma 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)
+  \lemma FirstIsoTheorem (p : isSurj f) : univ.isIsomorphism => (univKer-mono, univKer-epi p)
 }