{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Subgroup where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
private
variable
ℓ : Level
module _ (G' : Group ℓ) where
open GroupStr (snd G')
private G = ⟨ G' ⟩
record isSubgroup (H : ℙ G) : Type ℓ where
field
id-closed : (1g ∈ H)
op-closed : {x y : G} → x ∈ H → y ∈ H → x · y ∈ H
inv-closed : {x : G} → x ∈ H → inv x ∈ H
open isSubgroup
Subgroup : Type (ℓ-suc ℓ)
Subgroup = Σ[ H ∈ ℙ G ] isSubgroup H
isPropIsSubgroup : (H : ℙ G) → isProp (isSubgroup H)
id-closed (isPropIsSubgroup H h1 h2 i) =
∈-isProp H 1g (h1 .id-closed) (h2 .id-closed) i
op-closed (isPropIsSubgroup H h1 h2 i) Hx Hy =
∈-isProp H _ (h1 .op-closed Hx Hy) (h2 .op-closed Hx Hy) i
inv-closed (isPropIsSubgroup H h1 h2 i) Hx =
∈-isProp H _ (h1 .inv-closed Hx) (h2 .inv-closed Hx) i
isSetSubgroup : isSet Subgroup
isSetSubgroup = isSetΣ isSetℙ λ x → isProp→isSet (isPropIsSubgroup x)
Subgroup→Group : Subgroup → Group ℓ
Subgroup→Group (H , Hh) = makeGroup-right 1HG _·HG_ invHG isSetHG assocHG ridHG invrHG
where
HG = Σ[ x ∈ G ] ⟨ H x ⟩
isSetHG = isSetΣ is-set (λ x → isProp→isSet (H x .snd))
1HG : HG
1HG = (1g , (id-closed Hh))
_·HG_ : HG → HG → HG
(x , Hx) ·HG (y , Hy) = (x · y) , (op-closed Hh Hx Hy)
invHG : HG → HG
invHG (x , Hx) = inv x , inv-closed Hh Hx
assocHG : (x y z : HG) → x ·HG (y ·HG z) ≡ (x ·HG y) ·HG z
assocHG (x , Hx) (y , Hy) (z , Hz) =
ΣPathP (·Assoc x y z , isProp→PathP (λ i → H (·Assoc x y z i) .snd) _ _)
ridHG : (x : HG) → x ·HG 1HG ≡ x
ridHG (x , Hx) = ΣPathP (·IdR x , isProp→PathP (λ i → H (·IdR x i) .snd) _ _)
invrHG : (x : HG) → x ·HG invHG x ≡ 1HG
invrHG (x , Hx) = ΣPathP (·InvR x , isProp→PathP (λ i → H (·InvR x i) .snd) _ _)
⟪_⟫ : {G' : Group ℓ} → Subgroup G' → ℙ (G' .fst)
⟪ H , _ ⟫ = H
module _ {G' : Group ℓ} where
open GroupStr (snd G')
open isSubgroup
open GroupTheory G'
private G = ⟨ G' ⟩
isNormal : Subgroup G' → Type ℓ
isNormal H = (g h : G) → h ∈ ⟪ H ⟫ → g · h · inv g ∈ ⟪ H ⟫
isPropIsNormal : (H : Subgroup G') → isProp (isNormal H)
isPropIsNormal H = isPropΠ3 λ g h _ → ∈-isProp ⟪ H ⟫ (g · h · inv g)
·CommNormalSubgroup : (H : Subgroup G') (Hnormal : isNormal H) {x y : G}
→ x · y ∈ ⟪ H ⟫ → y · x ∈ ⟪ H ⟫
·CommNormalSubgroup H Hnormal {x = x} {y = y} Hxy =
subst-∈ ⟪ H ⟫ rem (Hnormal (inv x) (x · y) Hxy)
where
rem : inv x · (x · y) · inv (inv x) ≡ y · x
rem = inv x · (x · y) · inv (inv x) ≡⟨ ·Assoc _ _ _ ⟩
(inv x · x · y) · inv (inv x) ≡⟨ (λ i → ·Assoc (inv x) x y i · invInv x i) ⟩
((inv x · x) · y) · x ≡⟨ cong (λ z → (z · y) · x) (·InvL x) ⟩
(1g · y) · x ≡⟨ cong (_· x) (·IdL y) ⟩
y · x ∎
groupSubset : ℙ G
groupSubset x = (x ≡ x) , is-set x x
isSubgroupGroup : isSubgroup G' groupSubset
id-closed isSubgroupGroup = refl
op-closed isSubgroupGroup _ _ = refl
inv-closed isSubgroupGroup _ = refl
groupSubgroup : Subgroup G'
groupSubgroup = groupSubset , isSubgroupGroup
trivialSubset : ℙ G
trivialSubset x = (x ≡ 1g) , is-set x 1g
isSubgroupTrivialGroup : isSubgroup G' trivialSubset
id-closed isSubgroupTrivialGroup = refl
op-closed isSubgroupTrivialGroup hx hy = cong (_· _) hx ∙∙ ·IdL _ ∙∙ hy
inv-closed isSubgroupTrivialGroup hx = cong inv hx ∙ inv1g
trivialSubgroup : Subgroup G'
trivialSubgroup = trivialSubset , isSubgroupTrivialGroup
isNormalTrivialSubgroup : isNormal trivialSubgroup
isNormalTrivialSubgroup g h h≡1 =
(g · h · inv g) ≡⟨ (λ i → g · h≡1 i · inv g) ⟩
(g · 1g · inv g) ≡⟨ ·Assoc _ _ _ ∙ cong (_· inv g) (·IdR g) ⟩
(g · inv g) ≡⟨ ·InvR g ⟩
1g ∎
NormalSubgroup : (G : Group ℓ) → Type _
NormalSubgroup G = Σ[ G ∈ Subgroup G ] isNormal G
module _ {G H : Group ℓ} (ϕ : GroupHom G H) where
open isSubgroup
open GroupTheory
private
module G = GroupStr (snd G)
module H = GroupStr (snd H)
f = ϕ .fst
module ϕ = IsGroupHom (ϕ .snd)
imSubset : ℙ ⟨ H ⟩
imSubset x = isInIm ϕ x , isPropIsInIm ϕ x
isSubgroupIm : isSubgroup H imSubset
id-closed isSubgroupIm = ∣ G.1g , ϕ.pres1 ∣₁
op-closed isSubgroupIm =
map2 λ { (x , hx) (y , hy) → x G.· y , ϕ.pres· x y ∙ λ i → hx i H.· hy i }
inv-closed isSubgroupIm = map λ { (x , hx) → G.inv x , ϕ.presinv x ∙ cong H.inv hx }
imSubgroup : Subgroup H
imSubgroup = imSubset , isSubgroupIm
imGroup : Group ℓ
imGroup = Subgroup→Group _ imSubgroup
isNormalIm : ((x y : ⟨ H ⟩) → x H.· y ≡ y H.· x)
→ isNormal imSubgroup
isNormalIm comm x y =
map λ {(g , p)
→ g ,
(ϕ .fst g ≡⟨ p ⟩
y ≡⟨ sym (H.·IdR y) ⟩
(y H.· H.1g) ≡⟨ cong (y H.·_) (sym (H.·InvR x)) ⟩
(y H.· (x H.· H.inv x)) ≡⟨ H.·Assoc y x (H.inv x) ⟩
((y H.· x) H.· H.inv x) ≡⟨ cong (H._· H.inv x) (comm y x) ⟩
((x H.· y) H.· H.inv x) ≡⟨ sym (H.·Assoc x y (H.inv x)) ⟩
x H.· y H.· H.inv x ∎ )}
kerSubset : ℙ ⟨ G ⟩
kerSubset x = isInKer ϕ x , isPropIsInKer ϕ x
isSubgroupKer : isSubgroup G kerSubset
id-closed isSubgroupKer = ϕ.pres1
op-closed isSubgroupKer {x} {y} hx hy =
ϕ.pres· x y ∙∙ (λ i → hx i H.· hy i) ∙∙ H.·IdR _
inv-closed isSubgroupKer hx = ϕ.presinv _ ∙∙ cong H.inv hx ∙∙ inv1g H
kerSubgroup : Subgroup G
kerSubgroup = kerSubset , isSubgroupKer
isNormalKer : isNormal kerSubgroup
isNormalKer x y hy =
f (x G.· y G.· G.inv x) ≡⟨ ϕ.pres· _ _ ⟩
f x H.· f (y G.· G.inv x) ≡⟨ cong (f x H.·_) (ϕ.pres· _ _) ⟩
f x H.· f y H.· f (G.inv x) ≡⟨ (λ i → f x H.· hy i H.· f (G.inv x)) ⟩
f x H.· (H.1g H.· f (G.inv x)) ≡⟨ cong (f x H.·_) (H.·IdL _) ⟩
f x H.· f (G.inv x) ≡⟨ cong (f x H.·_) (ϕ.presinv x) ⟩
f x H.· H.inv (f x) ≡⟨ H.·InvR _ ⟩
H.1g ∎
module _ {G H : Group ℓ} (ϕ : GroupHom G H) where
kerGroup : Group ℓ
kerGroup = Subgroup→Group G (kerSubgroup ϕ)
kerGroup≡ : {x y : ⟨ kerGroup ⟩} → x .fst ≡ y .fst → x ≡ y
kerGroup≡ = Σ≡Prop (isPropIsInKer ϕ)