mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-07 04:48:41 +00:00
Rejig subgroups, add ideals (#79)
This commit is contained in:
Patrick Stevens
GitHub
@@ -20,11 +20,11 @@ module Groups.Abelian.Lemmas where
|
||||
directSumAbelianGroup : {m n o p : _} → {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} {underG : Group S _·A_} {underH : Group T _·B_} (G : AbelianGroup underG) (h : AbelianGroup underH) → (AbelianGroup (directSumGroup underG underH))
|
||||
AbelianGroup.commutative (directSumAbelianGroup {A = A} {B} G H) = AbelianGroup.commutative G ,, AbelianGroup.commutative H
|
||||
|
||||
subgroupOfAbelianIsAbelian : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → Subgroup G H fHom → AbelianGroup G → AbelianGroup H
|
||||
AbelianGroup.commutative (subgroupOfAbelianIsAbelian {S = S} {_+B_ = _+B_} {fHom = fHom} record { fInj = fInj } record { commutative = commutative }) {x} {y} = SetoidInjection.injective fInj (transitive (GroupHom.groupHom fHom) (transitive commutative (symmetric (GroupHom.groupHom fHom))))
|
||||
subgroupOfAbelianIsAbelian : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → SetoidInjection T S f → AbelianGroup G → AbelianGroup H
|
||||
AbelianGroup.commutative (subgroupOfAbelianIsAbelian {S = S} {_+B_ = _+B_} {fHom = fHom} fInj record { commutative = commutative }) {x} {y} = SetoidInjection.injective fInj (transitive (GroupHom.groupHom fHom) (transitive commutative (symmetric (GroupHom.groupHom fHom))))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
|
||||
abelianIsGroupProperty : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} → GroupsIsomorphic G H → AbelianGroup H → AbelianGroup G
|
||||
abelianIsGroupProperty iso abH = subgroupOfAbelianIsAbelian {fHom = GroupIso.groupHom (GroupsIsomorphic.proof iso)} (record { fInj = SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof iso)) }) abH
|
||||
abelianIsGroupProperty iso abH = subgroupOfAbelianIsAbelian {fHom = GroupIso.groupHom (GroupsIsomorphic.proof iso)} (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof iso))) abH
|
||||
|
||||
@@ -16,47 +16,25 @@ open import Groups.Groups2
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Groups.Actions.Definition
|
||||
|
||||
module Groups.Actions.Stabiliser where
|
||||
module Groups.Actions.Stabiliser {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (act : GroupAction G T) where
|
||||
|
||||
data Stabiliser {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) : Set (a ⊔ b ⊔ c ⊔ d) where
|
||||
stab : (g : A) → Setoid._∼_ T (GroupAction.action action g x) x → Stabiliser action x
|
||||
open GroupAction act
|
||||
open Setoid T
|
||||
|
||||
stabiliserSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Setoid (Stabiliser action x)
|
||||
Setoid._∼_ (stabiliserSetoid {S = S} action x) (stab g gx=x) (stab h hx=x) = Setoid._∼_ S g h
|
||||
Equivalence.reflexive (Setoid.eq (stabiliserSetoid {S = S} action x)) {stab g _} = Equivalence.reflexive (Setoid.eq S)
|
||||
Equivalence.symmetric (Setoid.eq (stabiliserSetoid {S = S} action x)) {stab g _} {stab h _} = Equivalence.symmetric (Setoid.eq S)
|
||||
Equivalence.transitive (Setoid.eq (stabiliserSetoid {S = S} action x)) {stab g _} {stab h _} {stab i _} = Equivalence.transitive (Setoid.eq S)
|
||||
stabiliserPred : (x : B) → (g : A) → Set d
|
||||
stabiliserPred x g = (action g x) ∼ x
|
||||
|
||||
stabiliserGroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Stabiliser action x → Stabiliser action x → Stabiliser action x
|
||||
stabiliserGroupOp {T = T} {_+_ = _+_} action (stab p px=x) (stab q qx=x) = stab (p + q) (transitive (GroupAction.associativeAction action) (transitive (GroupAction.actionWellDefined2 action qx=x) px=x))
|
||||
stabiliserWellDefined : (x : B) → {g h : A} → Setoid._∼_ S g h → (stabiliserPred x g) → stabiliserPred x h
|
||||
stabiliserWellDefined x {g} {h} g=h gx=x = transitive (actionWellDefined1 (Equivalence.symmetric (Setoid.eq S) g=h)) gx=x
|
||||
where
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
|
||||
stabiliserGroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Group (stabiliserSetoid action x) (stabiliserGroupOp action)
|
||||
Group.+WellDefined (stabiliserGroup {T = T} {G = G} action {x}) {stab m mx=x} {stab n nx=x} {stab r rx=x} {stab s sx=x} m=r n=s = Group.+WellDefined G m=r n=s
|
||||
stabiliserSubgroup : (x : B) → subgroup G (stabiliserWellDefined x)
|
||||
_&_&_.one (stabiliserSubgroup x) gx=x hx=x = transitive associativeAction (transitive (actionWellDefined2 hx=x) gx=x)
|
||||
where
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
Group.0G (stabiliserGroup {G = G} action) = stab (Group.0G G) (GroupAction.identityAction action)
|
||||
Group.inverse (stabiliserGroup {T = T} {_+_ = _+_} {G = G} action {x}) (stab g gx=x) = stab (Group.inverse G g) (transitive {_} {GroupAction.action action ((inverse g) + g) x} (symmetric (transitive (GroupAction.associativeAction action) (GroupAction.actionWellDefined2 action gx=x))) (transitive (GroupAction.actionWellDefined1 action invLeft) (GroupAction.identityAction action)))
|
||||
_&_&_.two (stabiliserSubgroup x) = identityAction
|
||||
_&_&_.three (stabiliserSubgroup x) {g = g} gx=x = transitive (transitive (transitive (actionWellDefined2 (symmetric gx=x)) (symmetric associativeAction)) (actionWellDefined1 (invLeft {g}))) identityAction
|
||||
where
|
||||
open Equivalence eq
|
||||
open Group G
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
Group.+Associative (stabiliserGroup {G = G} action) {stab m mx=x} {stab n nx=x} {stab o ox=x} = Group.+Associative G
|
||||
Group.identRight (stabiliserGroup {G = G} action) {stab m mx=x} = Group.identRight G
|
||||
Group.identLeft (stabiliserGroup {G = G} action) {stab m mx=x }= Group.identLeft G
|
||||
Group.invLeft (stabiliserGroup {G = G} action) {stab m mx=x} = Group.invLeft G
|
||||
Group.invRight (stabiliserGroup {G = G} action) {stab m mx=x} = Group.invRight G
|
||||
|
||||
stabiliserInjection : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Stabiliser action x → A
|
||||
stabiliserInjection action (stab g gx=x) = g
|
||||
|
||||
stabiliserInjectionIsHom : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → GroupHom (stabiliserGroup action {x}) G (stabiliserInjection action {x})
|
||||
GroupHom.groupHom (stabiliserInjectionIsHom {S = S} action) {stab g gx=x} {stab h hx=x} = Equivalence.reflexive (Setoid.eq S)
|
||||
GroupHom.wellDefined (stabiliserInjectionIsHom action) {stab g gx=x} {stab h hx=x} g=h = g=h
|
||||
|
||||
stabiliserIsSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Subgroup G (stabiliserGroup action) (stabiliserInjectionIsHom action {x})
|
||||
SetoidInjection.wellDefined (Subgroup.fInj (stabiliserIsSubgroup action)) {stab g gx=x} {stab h hx=x} g=h = g=h
|
||||
SetoidInjection.injective (Subgroup.fInj (stabiliserIsSubgroup action)) {stab g gx=x} {stab h hx=x} g=h = g=h
|
||||
|
||||
@@ -35,85 +35,6 @@ module Groups.Examples.ExampleSheet1 where
|
||||
question1' : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} → (G : Group S _+_) → Setoid._∼_ S ((Group.0G G) + (Group.0G G)) (Group.0G G)
|
||||
question1' G = Group.identRight G
|
||||
|
||||
{-
|
||||
Question 2: intersection of subgroups is a subgroup; union of subgroups is a subgroup iff one is contained in the other.
|
||||
|
||||
First, define the intersection of subgroups and show that it is a subgroup.
|
||||
-}
|
||||
data SubgroupIntersectionElement {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) : Set (a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ f) where
|
||||
ofElt : {x : A} → Sg B (λ b → Setoid._∼_ S (h1Inj b) x) → Sg C (λ c → Setoid._∼_ S (h2Inj c) x) → SubgroupIntersectionElement G H1 H2
|
||||
|
||||
subgroupIntersectionOp : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → (r : SubgroupIntersectionElement G H1 H2) → (s : SubgroupIntersectionElement G H1 H2) → SubgroupIntersectionElement G H1 H2
|
||||
subgroupIntersectionOp {S = S} {_+_ = _+_} {_+H1_ = _+H1_} {_+H2_ = _+H2_} G {h1Hom = h1Hom} {h2Hom = h2Hom} H1 H2 (ofElt (b , prB) (c , prC)) (ofElt (b2 , prB2) (c2 , prC2)) = ofElt ((b +H1 b2) , GroupHom.groupHom h1Hom) ((c +H2 c2) , transitive (GroupHom.groupHom h2Hom) (transitive (Group.+WellDefined G prC prC2) (Group.+WellDefined G (symmetric prB) (symmetric prB2))))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
|
||||
subgroupIntersectionSetoid : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → Setoid (SubgroupIntersectionElement G H1 H2)
|
||||
Setoid._∼_ (subgroupIntersectionSetoid {T = T} {U = U} G {h1Inj = h1} {h2Inj = h2} H1 H2) (ofElt (xH1 , prxH1) (xH2 , prxH2)) (ofElt (yH1 , pryH1) (yH2 , pryH2)) = (Setoid._∼_ T xH1 yH1) && (Setoid._∼_ U xH2 yH2)
|
||||
Equivalence.reflexive (Setoid.eq (subgroupIntersectionSetoid {T = T} {U = U} G H1 H2)) {ofElt (a , prA) (b , prB)} = (Equivalence.reflexive (Setoid.eq T)) ,, (Equivalence.reflexive (Setoid.eq U))
|
||||
Equivalence.symmetric (Setoid.eq (subgroupIntersectionSetoid {T = T} {U = U} G H1 H2)) {ofElt (a , prA) (b , prB)} {ofElt (c , prC) (d , prD)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq T) fst ,, Equivalence.symmetric (Setoid.eq U) snd
|
||||
Equivalence.transitive (Setoid.eq (subgroupIntersectionSetoid {T = T} {U = U} G H1 H2)) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq T) fst1 fst2 ,, Equivalence.transitive (Setoid.eq U) snd1 snd2
|
||||
|
||||
subgroupIntersectionGroup : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → Group (subgroupIntersectionSetoid G H1 H2) (subgroupIntersectionOp G H1 H2)
|
||||
Group.+WellDefined (subgroupIntersectionGroup {S = S} {T = T} {U = U} G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (_ , _) (_ , _)} {ofElt (_ , _ ) (_ , _)} {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (pr1 ,, pr2) (pr3 ,, pr4) = transitiveT (Group.+WellDefined h1 pr1 reflexiveT) (Group.+WellDefined h1 reflexiveT pr3) ,, transitiveU (Group.+WellDefined h2 pr2 reflexiveU) ((Group.+WellDefined h2 reflexiveU pr4))
|
||||
where
|
||||
open Group G
|
||||
open Setoid T
|
||||
open Equivalence (Setoid.eq T) renaming (transitive to transitiveT ; symmetric to symmetricT ; reflexive to reflexiveT)
|
||||
open Equivalence (Setoid.eq U) renaming (transitive to transitiveU ; symmetric to symmetricU ; reflexive to reflexiveU)
|
||||
Group.0G (subgroupIntersectionGroup G {H1grp = H1grp} {H2grp = H2grp} {h1Hom = h1Hom} {h2Hom = h2Hom} H1 H2) = ofElt {x = Group.0G G} (Group.0G H1grp , imageOfIdentityIsIdentity h1Hom) (Group.0G H2grp , imageOfIdentityIsIdentity h2Hom)
|
||||
Group.inverse (subgroupIntersectionGroup {S = S} G {H1grp = h1} {H2grp = h2} {h1Hom = h1hom} {h2Hom = h2hom} H1 H2) (ofElt (a , prA) (b , prB)) = ofElt (Group.inverse h1 a , homRespectsInverse h1hom) (Group.inverse h2 b , transitive (homRespectsInverse h2hom) (inverseWellDefined G (transitive prB (symmetric prA))))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
Group.+Associative (subgroupIntersectionGroup G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (a , prA) (b , prB)} {ofElt (c , prC) (d , prD)} {ofElt (e , prE) (f , prF)} = Group.+Associative h1 ,, Group.+Associative h2
|
||||
Group.identRight (subgroupIntersectionGroup G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (_ , _) (_ , _)} = Group.identRight h1 ,, Group.identRight h2
|
||||
Group.identLeft (subgroupIntersectionGroup G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (_ , _) (_ , _)} = Group.identLeft h1 ,, Group.identLeft h2
|
||||
Group.invLeft (subgroupIntersectionGroup G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (_ , _) (_ , _)} = Group.invLeft h1 ,, Group.invLeft h2
|
||||
Group.invRight (subgroupIntersectionGroup G {H1grp = h1} {H2grp = h2} H1 H2) {ofElt (_ , _) (_ , _)} = Group.invRight h1 ,, Group.invRight h2
|
||||
|
||||
subgroupIntersectionInjectionIntoMain : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → SubgroupIntersectionElement G H1 H2 → A
|
||||
subgroupIntersectionInjectionIntoMain G {h1Inj = f} H1 H2 (ofElt (a , prA) (b , prB)) = f a
|
||||
|
||||
subgroupIntersectionInjectionIntoMainIsHom : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → GroupHom (subgroupIntersectionGroup G H1 H2) G (subgroupIntersectionInjectionIntoMain G H1 H2)
|
||||
GroupHom.groupHom (subgroupIntersectionInjectionIntoMainIsHom G {h1Hom = h1} H1 H2) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} = GroupHom.groupHom h1
|
||||
GroupHom.wellDefined (subgroupIntersectionInjectionIntoMainIsHom G {h1Hom = h1} H1 H2) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = GroupHom.wellDefined h1 fst
|
||||
|
||||
subgroupIntersectionIsSubgroup : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → Subgroup G (subgroupIntersectionGroup G H1 H2) (subgroupIntersectionInjectionIntoMainIsHom G H1 H2)
|
||||
SetoidInjection.wellDefined (Subgroup.fInj (subgroupIntersectionIsSubgroup G {h1Hom = h1} H1 H2)) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = GroupHom.wellDefined h1 fst
|
||||
SetoidInjection.injective (Subgroup.fInj (subgroupIntersectionIsSubgroup {S = S} G H1 H2)) {ofElt (a , prA) (b , prB)} {ofElt (c , prC) (d , prD)} x~y = SetoidInjection.injective (Subgroup.fInj H1) x~y ,, SetoidInjection.injective (Subgroup.fInj H2) (transitive prB (transitive (transitive (symmetric prA) (transitive x~y prC) ) (symmetric prD)))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
|
||||
{-
|
||||
To make sure we haven't defined something stupid, check that the intersection doesn't care which order the two subgroups came in, and check that the subgroup intersection is isomorphic to the original group in the case that the two were the same, and check that the intersection injects into the first subgroup.
|
||||
-}
|
||||
|
||||
subgroupIntersectionIsomorphic : {a b c d e f : _} {A : Set a} {B : Set b} {C : Set c} {S : Setoid {a} {d} A} {T : Setoid {b} {e} B} {U : Setoid {c} {f} C} {_+_ : A → A → A} {_+H1_ : B → B → B} {_+H2_ : C → C → C} (G : Group S _+_) {H1grp : Group T _+H1_} {H2grp : Group U _+H2_} {h1Inj : B → A} {h2Inj : C → A} {h1Hom : GroupHom H1grp G h1Inj} {h2Hom : GroupHom H2grp G h2Inj} (H1 : Subgroup G H1grp h1Hom) (H2 : Subgroup G H2grp h2Hom) → GroupsIsomorphic (subgroupIntersectionGroup G H1 H2) (subgroupIntersectionGroup G H2 H1)
|
||||
GroupsIsomorphic.isomorphism (subgroupIntersectionIsomorphic G H1 H2) (ofElt (a , prA) (b , prB)) = ofElt (b , prB) (a , prA)
|
||||
GroupHom.groupHom (GroupIso.groupHom (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic {T = T} {U = U} G H1 H2))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} = Equivalence.reflexive (Setoid.eq U) ,, Equivalence.reflexive (Setoid.eq T)
|
||||
GroupHom.wellDefined (GroupIso.groupHom (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic G H1 H2))) {ofElt (a , prA) (b , prB)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = snd ,, fst
|
||||
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic G H1 H2)))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = snd ,, fst
|
||||
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic G H1 H2)))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = snd ,, fst
|
||||
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic G H1 H2)))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, snd) = snd ,, fst
|
||||
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionIsomorphic {T = T} {U = U} G H1 H2)))) {ofElt (a , prA) (b , prB)} = ofElt (b , prB) (a , prA) , (Equivalence.reflexive (Setoid.eq U) ,, Equivalence.reflexive (Setoid.eq T))
|
||||
|
||||
subgroupIntersectionOfSame : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {_+H1_ : B → B → B} (G : Group S _+_) {H1grp : Group T _+H1_} {h1Inj : B → A} {h1Hom : GroupHom H1grp G h1Inj} (H1 : Subgroup G H1grp h1Hom) → GroupsIsomorphic (subgroupIntersectionGroup G H1 H1) H1grp
|
||||
GroupsIsomorphic.isomorphism (subgroupIntersectionOfSame G H1) (ofElt (a , prA) (b , prB)) = a
|
||||
GroupHom.groupHom (GroupIso.groupHom (GroupsIsomorphic.proof (subgroupIntersectionOfSame {T = T} G H1))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} = Equivalence.reflexive (Setoid.eq T)
|
||||
GroupHom.wellDefined (GroupIso.groupHom (GroupsIsomorphic.proof (subgroupIntersectionOfSame G H1))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, _) = fst
|
||||
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionOfSame G H1)))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, _) = fst
|
||||
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionOfSame {S = S} {T = T} G {h1Hom = h1Hom} H1)))) {ofElt (a , prA) (b , prB)} {ofElt (c , prC) (d , prD)} a~b = a~b ,, SetoidInjection.injective (Subgroup.fInj H1) (transitive prB (transitive (transitive (symmetric prA) (transitive (GroupHom.wellDefined h1Hom a~b) prC)) (symmetric prD)))
|
||||
where
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionOfSame G H1)))) {ofElt (_ , _) (_ , _)} {ofElt (_ , _) (_ , _)} (fst ,, _) = fst
|
||||
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (subgroupIntersectionOfSame {S = S} {T = T} G H1)))) {b} = ofElt (b , Equivalence.reflexive (Setoid.eq S)) (b , Equivalence.reflexive (Setoid.eq S)) , (Equivalence.reflexive (Setoid.eq T))
|
||||
|
||||
{- TODO: finish question 2 -}
|
||||
|
||||
{-
|
||||
Question 3. We can't talk about ℝ yet, so we'll just work in an arbitrary integral domain.
|
||||
Show that the collection of linear functions over a ring forms a group; is it abelian?
|
||||
|
||||
@@ -56,8 +56,8 @@ groupHomImageIncludes : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c
|
||||
GroupHom.groupHom (groupHomImageIncludes fHom) {ofElt x} {ofElt y} = GroupHom.groupHom fHom
|
||||
GroupHom.wellDefined (groupHomImageIncludes fHom) {ofElt x} {ofElt y} x~y = x~y
|
||||
|
||||
groupHomImageIsSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → Subgroup H (imageGroup fHom) (groupHomImageIncludes fHom)
|
||||
Subgroup.fInj (groupHomImageIsSubgroup {S = S} {T} {_+G_} {_+H_} {G} {H} {f} fHom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (groupHomImageIncludes fHom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
|
||||
groupHomImageInjects : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) → SetoidInjection (imageGroupSetoid fHom) T (groupHomImageInclusion fHom)
|
||||
groupHomImageInjects {S = S} {T} {_+G_} {_+H_} {G} {H} {f} fHom = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (groupHomImageIncludes fHom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
|
||||
where
|
||||
inj : {x y : GroupHomImageElement fHom} → (Setoid._∼_ T (groupHomImageInclusion fHom x) (groupHomImageInclusion fHom y)) → Setoid._∼_ (imageGroupSetoid fHom) x y
|
||||
inj {ofElt x} {ofElt y} x~y = x~y
|
||||
|
||||
@@ -9,10 +9,9 @@ open import Sets.FinSet
|
||||
open import Groups.Definition
|
||||
open import Groups.Homomorphisms.Definition
|
||||
|
||||
module Groups.Subgroups.Definition where
|
||||
module Groups.Subgroups.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
|
||||
|
||||
record Subgroup {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) {f : B → A} (hom : GroupHom H G f) : Set (a ⊔ b ⊔ c ⊔ d) where
|
||||
open Setoid T renaming (_∼_ to _∼G_)
|
||||
open Setoid S renaming (_∼_ to _∼H_)
|
||||
field
|
||||
fInj : SetoidInjection T S f
|
||||
open Group G
|
||||
|
||||
subgroup : {c : _} {pred : A → Set c} → (wd : {x y : A} → (Setoid._∼_ S x y) → (pred x → pred y)) → Set (a ⊔ c)
|
||||
subgroup {pred = pred} wd = ({g h : A} → (pred g) → (pred h) → pred (g + h)) & pred 0G & ({g : A} → (pred g) → (pred (inverse g)))
|
||||
|
||||
@@ -20,10 +20,7 @@ open import Groups.QuotientGroup.Definition
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
module Groups.Subgroups.Normal.Definition where
|
||||
module Groups.Subgroups.Normal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
|
||||
|
||||
record NormalSubgroup {a} {b} {c} {d} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) {f : B → A} (hom : GroupHom H G f) : Set (a ⊔ b ⊔ c ⊔ d) where
|
||||
open Setoid S
|
||||
field
|
||||
subgroup : Subgroup G H hom
|
||||
normal : {g : A} {h : B} → Sg B (λ fromH → (g ·A (f h)) ·A (Group.inverse G g) ∼ f fromH)
|
||||
normalSubgroup : {c : _} {pred : A → Set c} (wd : {x y : A} → (Setoid._∼_ S x y) → (pred x → pred y)) (sub : subgroup G wd) → Set (a ⊔ c)
|
||||
normalSubgroup {pred = pred} wd sub = {g k : A} → pred k → pred (g + (k + Group.inverse G g))
|
||||
|
||||
@@ -58,25 +58,29 @@ injectionFromKernelToGIsHom : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid
|
||||
GroupHom.groupHom (injectionFromKernelToGIsHom {S = S} G hom) {kerOfElt x prX} {kerOfElt y prY} = Equivalence.reflexive (Setoid.eq S)
|
||||
GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {kerOfElt x prX} {kerOfElt y prY} i = i
|
||||
|
||||
groupKernelGroupIsSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → Subgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
|
||||
Subgroup.fInj (groupKernelGroupIsSubgroup {S = S} {T = T} G {f = f} hom) = record { wellDefined = λ {x} {y} → GroupHom.wellDefined (injectionFromKernelToGIsHom G hom) {x} {y} ; injective = λ {x} {y} → inj {x} {y} }
|
||||
where
|
||||
inj : {x : GroupKernelElement G hom} → {y : GroupKernelElement G hom} → Setoid._∼_ S (injectionFromKernelToG G hom x) (injectionFromKernelToG G hom y) → Setoid._∼_ (groupKernel G hom) x y
|
||||
inj {kerOfElt x prX} {kerOfElt y prY} = id
|
||||
groupKernelGroupPred : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → A → Set d
|
||||
groupKernelGroupPred {T = T} G {H = H} {f = f} hom a = Setoid._∼_ T (f a) (Group.0G H)
|
||||
|
||||
groupKernelGroupIsNormalSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → NormalSubgroup G (groupKernelGroup G hom) (injectionFromKernelToGIsHom G hom)
|
||||
NormalSubgroup.subgroup (groupKernelGroupIsNormalSubgroup G hom) = groupKernelGroupIsSubgroup G hom
|
||||
NormalSubgroup.normal (groupKernelGroupIsNormalSubgroup {S = S} {T = T} {_·A_ = _·A_} G {H = H} {f = f} hom) {g} {kerOfElt h prH} = kerOfElt ((g ·A h) ·A Group.inverse G g) ans , Equivalence.reflexive (Setoid.eq S)
|
||||
groupKernelGroupPredWd : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → {x y : A} → (Setoid._∼_ S x y) → (groupKernelGroupPred G hom x → groupKernelGroupPred G hom y)
|
||||
groupKernelGroupPredWd {S = S} {T = T} G hom {x} {y} x=y fx=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined hom (Equivalence.symmetric (Setoid.eq S) x=y)) fx=0
|
||||
|
||||
groupKernelGroupIsSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → subgroup G (groupKernelGroupPredWd G hom)
|
||||
_&_&_.one (groupKernelGroupIsSubgroup {S = S} {T = T} G {H = H} hom) g=0 h=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.groupHom hom) (Equivalence.transitive (Setoid.eq T) (Group.+WellDefined H g=0 h=0) (Group.identLeft H))
|
||||
_&_&_.two (groupKernelGroupIsSubgroup G hom) = imageOfIdentityIsIdentity hom
|
||||
_&_&_.three (groupKernelGroupIsSubgroup {S = S} {T = T} G {H = H} hom) g=0 = Equivalence.transitive (Setoid.eq T) (homRespectsInverse hom) (Equivalence.transitive (Setoid.eq T) (inverseWellDefined H g=0) (invIdent H))
|
||||
|
||||
groupKernelGroupIsNormalSubgroup : {a b c d : _} {A : Set a} {B : Set c} {S : Setoid {a} {b} A} {T : Setoid {c} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (hom : GroupHom G H f) → normalSubgroup G (groupKernelGroupPredWd G hom) (groupKernelGroupIsSubgroup G hom)
|
||||
groupKernelGroupIsNormalSubgroup {T = T} G {H = H} hom k=0 = transitive groupHom (transitive (+WellDefined reflexive groupHom) (transitive (+WellDefined reflexive (transitive (+WellDefined k=0 reflexive) identLeft)) (transitive (symmetric groupHom) (transitive (wellDefined (Group.invRight G)) (imageOfIdentityIsIdentity hom)))))
|
||||
where
|
||||
open Setoid T
|
||||
open Group H
|
||||
open Equivalence eq
|
||||
ans : f ((g ·A h) ·A Group.inverse G g) ∼ Group.0G H
|
||||
ans = transitive (GroupHom.groupHom hom) (transitive (Group.+WellDefined H (GroupHom.groupHom hom) reflexive) (transitive (Group.+WellDefined H (Group.+WellDefined H reflexive prH) reflexive) (transitive (Group.+WellDefined H (Group.identRight H) reflexive) (transitive (symmetric (GroupHom.groupHom hom)) (transitive (GroupHom.wellDefined hom (Group.invRight G)) (imageOfIdentityIsIdentity hom))))))
|
||||
open GroupHom hom
|
||||
|
||||
abelianGroupSubgroupIsNormal : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {underG : Group S _+A_} (G : AbelianGroup underG) {H : Group T _+B_} {f : B → A} {hom : GroupHom H underG f} (s : Subgroup underG H hom) → NormalSubgroup underG H hom
|
||||
NormalSubgroup.subgroup (abelianGroupSubgroupIsNormal G H) = H
|
||||
NormalSubgroup.normal (abelianGroupSubgroupIsNormal {S = S} {underG = G} record { commutative = commutative } H) {g} {h} = h , transitive (+WellDefined commutative reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight))
|
||||
abelianGroupSubgroupIsNormal : {a b c : _} {A : Set a} {B : Set b} {S : Setoid {a} {b} A} {_+_ : A → A → A} {G : Group S _+_} {pred : A → Set c} (predWd : {x y : A} → (Setoid._∼_ S x y) → (pred x → pred y)) → (s : subgroup G predWd) → AbelianGroup G → normalSubgroup G predWd s
|
||||
abelianGroupSubgroupIsNormal {S = S} {_+_ = _+_} {G = G} predWd record { one = respectsPlus ; two = respectsId ; three = respectsInv } abelian {k} {l} prK = predWd (transitive (transitive (transitive (symmetric identLeft) (+WellDefined (symmetric invRight) reflexive)) (symmetric +Associative)) (+WellDefined reflexive commutative)) prK
|
||||
where
|
||||
open Setoid S
|
||||
open Group G
|
||||
open Equivalence (Setoid.eq S)
|
||||
open AbelianGroup abelian
|
||||
open Setoid S
|
||||
open Equivalence eq
|
||||
|
||||
@@ -11,6 +11,7 @@ open import Functions
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Rings.Definition
|
||||
open import Rings.Homomorphisms.Definition
|
||||
open import Groups.Homomorphisms.Lemmas
|
||||
|
||||
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
|
||||
|
||||
@@ -18,3 +19,27 @@ module Rings.Ideals.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_
|
||||
|
||||
ringKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → Set (a ⊔ d)
|
||||
ringKernel {T = T} R2 {f} fHom = Sg A (λ a → Setoid._∼_ T (f a) (Ring.0R R2))
|
||||
|
||||
ideal : {c : _} {pred : A → Set c} → (wd : {x y : A} → (Setoid._∼_ S x y) → (pred x → pred y)) → Set (a ⊔ c)
|
||||
ideal {pred = pred} wd = (pred (Ring.0R R)) & ({x y : A} → pred x → pred y → pred (x + y)) & ({x : A} → {y : A} → pred x → pred (x * y))
|
||||
|
||||
idealPredForKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → A → Set d
|
||||
idealPredForKernel {T = T} R2 {f} fHom a = Setoid._∼_ T (f a) (Ring.0R R2)
|
||||
|
||||
idealPredForKernelWellDefined : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → {x y : A} → (Setoid._∼_ S x y) → (idealPredForKernel R2 fHom x → idealPredForKernel R2 fHom y)
|
||||
idealPredForKernelWellDefined {T = T} R2 {f} fHom a x=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined (RingHom.groupHom fHom) (Equivalence.symmetric (Setoid.eq S) a)) x=0
|
||||
|
||||
kernelIdealIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : A → C} (fHom : RingHom R R2 f) → ideal {pred = idealPredForKernel R2 fHom} (idealPredForKernelWellDefined R2 fHom)
|
||||
_&_&_.one (kernelIdealIsIdeal fHom) = imageOfIdentityIsIdentity (RingHom.groupHom fHom)
|
||||
_&_&_.two (kernelIdealIsIdeal {T = T} {R2 = R2} fHom) fx=0 fy=0 = transitive (transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fx=0 fy=0)) identLeft
|
||||
where
|
||||
open Ring R2
|
||||
open Group (Ring.additiveGroup R2)
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
_&_&_.three (kernelIdealIsIdeal {T = T} {R2 = R2} fHom) fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2)))
|
||||
where
|
||||
open Ring R2
|
||||
open Group (Ring.additiveGroup R2)
|
||||
open Setoid T
|
||||
open Equivalence eq
|
||||
|
||||
Reference in New Issue
Block a user