From d2192c72d9352627a8fd6b4f71f577952b77dd57 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Tue, 19 Feb 2019 08:06:19 +0000 Subject: [PATCH] Symmetry group action (#24) --- Groups/FinitePermutations.agda | 34 ++++++++++++++++++++++++++++++++++ Groups/SymmetryGroups.agda | 32 +++++++++++++++++++++----------- Lists/Lists.agda | 4 ++++ 3 files changed, 59 insertions(+), 11 deletions(-) diff --git a/Groups/FinitePermutations.agda b/Groups/FinitePermutations.agda index 8a6187c..e76d926 100644 --- a/Groups/FinitePermutations.agda +++ b/Groups/FinitePermutations.agda @@ -4,6 +4,9 @@ open import LogicalFormulae open import Numbers.Naturals -- for length open import Lists.Lists open import Functions +open import Groups.SymmetryGroups +open import Sets.FinSet +open import Setoids.Setoids module Groups.FinitePermutations where allInsertions : {a : _} {A : Set a} (x : A) (l : List A) → List (List A) @@ -57,3 +60,34 @@ module Groups.FinitePermutations where lemma = allTrueEqual (λ a → succ (length a)) (succ (length l)) (permutations l) (allTrueExtension (λ z → length z ≡ length l) (λ i → succ (length i) ≡ succ (length l)) (permutations l) (λ pr → applyEquality succ pr) (permsAllSameLength l)) ans : length (permutations l) +N length l *N length (permutations l) ≡ factorial (length l) +N length l *N factorial (length l) ans rewrite permsLen l = refl + +{- TODO: show that symmetricGroup acts in the obvious way on permutations FinSet + listElements : {a : _} {A : Set a} (l : List A) → Set + listElements [] = False + listElements (x :: l) = True || listElements l + + listElement : {a : _} {A : Set a} {l : List A} (elt : listElements l) → A + listElement {l = []} () + listElement {l = x :: l} (inl record {}) = x + listElement {l = x :: l} (inr elt) = listElement {l = l} elt + + backwardRange : ℕ → List ℕ + backwardRange zero = [] + backwardRange (succ n) = n :: backwardRange n + + backwardRangeLength : {n : ℕ} → length (backwardRange n) ≡ n + backwardRangeLength {zero} = refl + backwardRangeLength {succ n} rewrite backwardRangeLength {n} = refl + + applyPermutation : {n : ℕ} → (f : FinSet n → FinSet n) → listElements (permutations (backwardRange n)) → listElements (permutations (backwardRange n)) + applyPermutation {zero} f (inl record {}) = inl (record {}) + applyPermutation {zero} f (inr ()) + applyPermutation {succ n} f elt = {!!} + + finitePermutations : (n : ℕ) → SetoidToSet (symmetricSetoid (reflSetoid (FinSet n))) (listElements (permutations (backwardRange n))) + SetoidToSet.project (finitePermutations n) (sym {f} fBij) = {!!} + SetoidToSet.wellDefined (finitePermutations n) = {!!} + SetoidToSet.surj (finitePermutations n) = {!!} + SetoidToSet.inj (finitePermutations n) = {!!} + +-} diff --git a/Groups/SymmetryGroups.agda b/Groups/SymmetryGroups.agda index 87456e3..2560637 100644 --- a/Groups/SymmetryGroups.agda +++ b/Groups/SymmetryGroups.agda @@ -36,7 +36,7 @@ module Groups.SymmetryGroups where Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (symmetricSetoid S))) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} f~g g~h = extensionallyEqualTransitive S S f g h (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) (SetoidBijection.wellDefined bijH) f~g g~h symmetricGroupOp : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (f g : SymmetryGroupElements S) → SymmetryGroupElements S - symmetricGroupOp (sym {f} bijF) (sym {g} bijG) = sym (setoidBijComp bijF bijG) + symmetricGroupOp (sym {f} bijF) (sym {g} bijG) = sym (setoidBijComp bijG bijF) symmetricGroupInv : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → SymmetryGroupElements S → SymmetryGroupElements S symmetricGroupInv S (sym {f} bijF) with setoidBijectiveImpliesInvertible bijF @@ -44,20 +44,22 @@ module Groups.SymmetryGroups where symmetricGroupInvIsLeft : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp (symmetricGroupInv S x) x) (sym setoidIdIsBijective) symmetricGroupInvIsLeft {A = A} S {sym {f = f} fBij} = ExtensionallyEqual.eq ans - where - ans : {x : A} → Setoid._∼_ S (f (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) x)) x - ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {x} - ans {x} | a , b = b - - symmetricGroupInvIsRight : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp x (symmetricGroupInv S x)) (sym setoidIdIsBijective) - symmetricGroupInvIsRight {A = A} S {sym {f = f} fBij} = ExtensionallyEqual.eq ans where ans : {x : A} → Setoid._∼_ S (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) (f x)) x ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {f x} ans {x} | a , b = SetoidInjection.injective (SetoidBijection.inj fBij) b + symmetricGroupInvIsRight : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp x (symmetricGroupInv S x)) (sym setoidIdIsBijective) + symmetricGroupInvIsRight {A = A} S {sym {f = f} fBij} = ExtensionallyEqual.eq ans + where + ans : {x : A} → Setoid._∼_ S (f (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) x)) x + ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {x} + ans {x} | a , b = b + symmetricGroup : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Group (symmetricSetoid S) (symmetricGroupOp {A = A}) - Group.wellDefined (symmetricGroup A) {sym {m} bijM} {sym {n} bijN} {sym {x} bijX} {sym {y} bijY} (ExtensionallyEqual.eq m~x) (ExtensionallyEqual.eq n~y) = ExtensionallyEqual.eq (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq A)) (SetoidBijection.wellDefined bijN m~x) n~y) + Group.wellDefined (symmetricGroup A) {sym {m} bijM} {sym {n} bijN} {sym {x} bijX} {sym {y} bijY} (ExtensionallyEqual.eq m~x) (ExtensionallyEqual.eq n~y) = ExtensionallyEqual.eq (transitive m~x (SetoidBijection.wellDefined bijX n~y)) + where + open Transitive (Equivalence.transitiveEq (Setoid.eq A)) Group.identity (symmetricGroup A) = sym setoidIdIsBijective Group.inverse (symmetricGroup S) = symmetricGroupInv S Group.multAssoc (symmetricGroup A) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} = ExtensionallyEqual.eq λ {x} → Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq A)) @@ -76,5 +78,13 @@ module Groups.SymmetryGroups where SetoidSurjection.surjective (SetoidBijection.surj bij) {x} = GroupAction.action action (Group.inverse G f) x , Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq X)) (GroupAction.associativeAction action)) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (GroupAction.actionWellDefined1 action (Group.invRight G)) (GroupAction.identityAction action)) actionInducesHomIsHom : {a b c d : _} {A : Set a} {S : Setoid {a} {c} A} {_+_ : A → A → A} {G : Group S _+_} {B : Set b} {X : Setoid {b} {d} B} → (action : GroupAction G X) → GroupHom G (symmetricGroup X) (actionInducesHom action) - GroupHom.groupHom (actionInducesHomIsHom action) = {!!} - GroupHom.wellDefined (actionInducesHomIsHom action) x=y = {!!} + GroupHom.groupHom (actionInducesHomIsHom {X = X} action) {s1} {s2} = eq associativeAction + where + open Setoid X renaming (eq to setoidEq) + open Transitive (Equivalence.transitiveEq (Setoid.eq X)) + open Reflexive (Equivalence.reflexiveEq (Setoid.eq X)) + open Symmetric (Equivalence.symmetricEq (Setoid.eq X)) + open GroupAction action + GroupHom.wellDefined (actionInducesHomIsHom action) {s1} {s2} s1=s2 = eq (actionWellDefined1 s1=s2) + where + open GroupAction action diff --git a/Lists/Lists.agda b/Lists/Lists.agda index 3510944..44d8055 100644 --- a/Lists/Lists.agda +++ b/Lists/Lists.agda @@ -151,3 +151,7 @@ module Lists.Lists where head : {a : _} {A : Set a} (l : List A) (pr : 0