{-# OPTIONS --without-K --rewriting #-}
open import lib.Basics
open import lib.Equivalence2
open import lib.Function2
open import lib.NType2
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Subtype
open import lib.types.Truncation
open import lib.groups.SubgroupProp
module lib.groups.Homomorphism where
preserves-comp : ∀ {i j} {A : Type i} {B : Type j}
(A-comp : A → A → A) (B-comp : B → B → B) (f : A → B)
→ Type (lmax i j)
preserves-comp Ac Bc f = ∀ a₁ a₂ → f (Ac a₁ a₂) == Bc (f a₁) (f a₂)
preserves-comp-is-prop : ∀ {i j} {A : Type i} {B : Type j}
(pB : is-set B) (A-comp : A → A → A) (B-comp : B → B → B)
→ (f : A → B) → is-prop (preserves-comp A-comp B-comp f)
preserves-comp-is-prop pB Ac Bc f = Π-is-prop λ _ → Π-is-prop λ _ → pB _ _
preserves-comp-prop : ∀ {i j} {A : Type i} {B : Type j}
(pB : is-set B) (A-comp : A → A → A) (B-comp : B → B → B)
→ SubtypeProp (A → B) (lmax i j)
preserves-comp-prop pB Ac Bc =
preserves-comp Ac Bc , preserves-comp-is-prop pB Ac Bc
record GroupStructureHom {i j} {GEl : Type i} {HEl : Type j}
(GS : GroupStructure GEl) (HS : GroupStructure HEl) : Type (lmax i j) where
constructor group-structure-hom
private
module G = GroupStructure GS
module H = GroupStructure HS
field
f : GEl → HEl
pres-comp : preserves-comp G.comp H.comp f
abstract
pres-ident : f G.ident == H.ident
pres-ident = H.cancel-l (f G.ident) $
H.comp (f G.ident) (f G.ident)
=⟨ ! (pres-comp G.ident G.ident) ⟩
f (G.comp G.ident G.ident)
=⟨ ap f (G.unit-l G.ident) ⟩
f G.ident
=⟨ ! (H.unit-r (f G.ident)) ⟩
H.comp (f G.ident) H.ident =∎
pres-inv : ∀ g → f (G.inv g) == H.inv (f g)
pres-inv g = ! $ H.inv-unique-l _ _ $
H.comp (f (G.inv g)) (f g)
=⟨ ! (pres-comp (G.inv g) g) ⟩
f (G.comp (G.inv g) g)
=⟨ ap f (G.inv-l g) ⟩
f G.ident
=⟨ pres-ident ⟩
H.ident
=∎
pres-conj : ∀ g h → f (G.conj g h) == H.conj (f g) (f h)
pres-conj g h = pres-comp (G.comp g h) (G.inv g) ∙ ap2 H.comp (pres-comp g h) (pres-inv g)
pres-diff : ∀ g h → f (G.diff g h) == H.diff (f g) (f h)
pres-diff g h = pres-comp g (G.inv h) ∙ ap (H.comp (f g)) (pres-inv h)
⊙f : ⊙[ GEl , G.ident ] ⊙→ ⊙[ HEl , H.ident ]
⊙f = f , pres-ident
infix 0 _→ᴳˢ_
_→ᴳˢ_ = GroupStructureHom
record GroupHom {i j} (G : Group i) (H : Group j) : Type (lmax i j) where
constructor group-hom
private
module G = Group G
module H = Group H
field
f : G.El → H.El
pres-comp : ∀ g₁ g₂ → f (G.comp g₁ g₂) == H.comp (f g₁) (f g₂)
open GroupStructureHom {GS = G.group-struct} {HS = H.group-struct}
record {f = f ; pres-comp = pres-comp} hiding (f ; pres-comp) public
infix 0 _→ᴳ_
_→ᴳ_ = GroupHom
→ᴳˢ-to-→ᴳ : ∀ {i j} {G : Group i} {H : Group j}
→ (Group.group-struct G →ᴳˢ Group.group-struct H) → (G →ᴳ H)
→ᴳˢ-to-→ᴳ (group-structure-hom f pres-comp) = group-hom f pres-comp
idhom : ∀ {i} (G : Group i) → (G →ᴳ G)
idhom G = group-hom (idf _) (λ _ _ → idp)
module _ where
cst-hom : ∀ {i j} {G : Group i} {H : Group j} → (G →ᴳ H)
cst-hom {H = H} = group-hom (cst (Group.ident H)) (λ _ _ → ! (Group.unit-l H _))
inv-hom : ∀ {i} (G : AbGroup i) → GroupHom (AbGroup.grp G) (AbGroup.grp G)
inv-hom G = group-hom G.inv inv-pres-comp where
module G = AbGroup G
abstract
inv-pres-comp : (g₁ g₂ : G.El) → G.inv (G.comp g₁ g₂) == G.comp (G.inv g₁) (G.inv g₂)
inv-pres-comp g₁ g₂ = G.inv-comp g₁ g₂ ∙ G.comm (G.inv g₂) (G.inv g₁)
abstract
group-hom= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G →ᴳ H}
→ GroupHom.f φ == GroupHom.f ψ → φ == ψ
group-hom= {G = G} {H = H} p = ap (uncurry group-hom) $
Subtype=-out (preserves-comp-prop (Group.El-level H) (Group.comp G) (Group.comp H)) p
group-hom=-↓ : ∀ {i j k} {A : Type i} {G : A → Group j} {H : A → Group k} {x y : A}
{p : x == y} {φ : G x →ᴳ H x} {ψ : G y →ᴳ H y}
→ GroupHom.f φ == GroupHom.f ψ
[ (λ a → Group.El (G a) → Group.El (H a)) ↓ p ]
→ φ == ψ [ (λ a → G a →ᴳ H a) ↓ p ]
group-hom=-↓ {p = idp} = group-hom=
abstract
GroupHom-level : ∀ {i j} {G : Group i} {H : Group j} → is-set (G →ᴳ H)
GroupHom-level {G = G} {H = H} = equiv-preserves-level
(equiv (uncurry group-hom) (λ x → GroupHom.f x , GroupHom.pres-comp x)
(λ _ → idp) (λ _ → idp))
(Subtype-level
(preserves-comp-prop (Group.El-level H) (Group.comp G) (Group.comp H))
(→-level (Group.El-is-set H)))
→ᴳ-level = GroupHom-level
infixr 80 _∘ᴳ_
abstract
∘-pres-comp : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k} (ψ : H →ᴳ K) (φ : G →ᴳ H)
→ preserves-comp (Group.comp G) (Group.comp K) (GroupHom.f ψ ∘ GroupHom.f φ)
∘-pres-comp ψ φ g₁ g₂ = ap (GroupHom.f ψ) (GroupHom.pres-comp φ g₁ g₂)
∙ GroupHom.pres-comp ψ (GroupHom.f φ g₁) (GroupHom.f φ g₂)
_∘ᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
→ (H →ᴳ K) → (G →ᴳ H) → (G →ᴳ K)
ψ ∘ᴳ φ = group-hom (GroupHom.f ψ ∘ GroupHom.f φ) (∘-pres-comp ψ φ)
∘ᴳ-unit-r : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
→ φ ∘ᴳ idhom G == φ
∘ᴳ-unit-r φ = group-hom= idp
∘ᴳ-unit-l : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
→ idhom H ∘ᴳ φ == φ
∘ᴳ-unit-l φ = group-hom= idp
∘ᴳ-assoc : ∀ {i j k l} {G : Group i} {H : Group j} {K : Group k} {L : Group l}
(χ : K →ᴳ L) (ψ : H →ᴳ K) (φ : G →ᴳ H)
→ (χ ∘ᴳ ψ) ∘ᴳ φ == χ ∘ᴳ ψ ∘ᴳ φ
∘ᴳ-assoc χ ψ φ = group-hom= idp
is-injᴳ : ∀ {i j} {G : Group i} {H : Group j}
→ (G →ᴳ H) → Type (lmax i j)
is-injᴳ hom = is-inj (GroupHom.f hom)
is-surjᴳ : ∀ {i j} {G : Group i} {H : Group j}
→ (G →ᴳ H) → Type (lmax i j)
is-surjᴳ hom = is-surj (GroupHom.f hom)
infix 80 _∘subᴳ_
_∘subᴳ_ : ∀ {i j k} {G : Group i} {H : Group j}
→ SubgroupProp H k → (G →ᴳ H) → SubgroupProp G k
_∘subᴳ_ {k = k} {G = G} P φ = record {M} where
module G = Group G
module P = SubgroupProp P
module φ = GroupHom φ
module M where
prop : G.El → Type k
prop = P.prop ∘ φ.f
level : ∀ g → is-prop (prop g)
level = P.level ∘ φ.f
abstract
ident : prop G.ident
ident = transport! P.prop φ.pres-ident P.ident
diff : {g₁ g₂ : G.El} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)
diff {g₁} {g₂} pφg₁ pφg₂ = transport! P.prop
(φ.pres-diff g₁ g₂)
(P.diff pφg₁ pφg₂)
infix 80 _∘nsubᴳ_
_∘nsubᴳ_ : ∀ {i j k} {G : Group i} {H : Group j}
→ NormalSubgroupProp H k → (G →ᴳ H) → NormalSubgroupProp G k
_∘nsubᴳ_ {G = G} {H} P φ = P.propᴳ ∘subᴳ φ , P-φ-is-normal
where module P = NormalSubgroupProp P
module φ = GroupHom φ
abstract
P-φ-is-normal : is-normal (P.propᴳ ∘subᴳ φ)
P-φ-is-normal g₁ {g₂} pφg₂ = transport! P.prop
(φ.pres-conj g₁ g₂)
(P.conj (φ.f g₁) pφg₂)
module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where
private
module G = Group G
module H = Group H
module φ = GroupHom φ
ker-propᴳ : SubgroupProp G j
ker-propᴳ = record {M} where
module M where
prop : G.El → Type j
prop g = φ.f g == H.ident
abstract
level : (g : G.El) → is-prop (prop g)
level g = H.El-level _ _
ident : prop G.ident
ident = φ.pres-ident
diff : {g₁ g₂ : G.El} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)
diff {g₁} {g₂} p₁ p₂ = φ.pres-diff g₁ g₂ ∙ ap2 H.diff p₁ p₂ ∙ H.inv-r H.ident
ker-npropᴳ : NormalSubgroupProp G j
ker-npropᴳ = ker-propᴳ , ker-is-normal where
abstract
ker-is-normal : is-normal ker-propᴳ
ker-is-normal g₁ {g₂} pg₂ =
φ.pres-conj g₁ g₂
∙ ap (H.conj (φ.f g₁)) pg₂
∙ H.conj-ident-r (φ.f g₁)
im-propᴳ : SubgroupProp H (lmax i j)
im-propᴳ = record {M} where
module M where
prop : H.El → Type (lmax i j)
prop h = Trunc -1 (hfiber φ.f h)
level : (h : H.El) → is-prop (prop h)
level h = Trunc-level
abstract
ident : prop H.ident
ident = [ G.ident , φ.pres-ident ]
diff : {h₁ h₂ : H.El} → prop h₁ → prop h₂ → prop (H.diff h₁ h₂)
diff = Trunc-fmap2 λ {(g₁ , p₁) (g₂ , p₂)
→ G.diff g₁ g₂ , φ.pres-diff g₁ g₂ ∙ ap2 H.diff p₁ p₂}
im-npropᴳ : is-abelian H → NormalSubgroupProp H (lmax i j)
im-npropᴳ H-is-abelian = sub-abelian-normal H-is-abelian im-propᴳ
has-trivial-kerᴳ : Type (lmax i j)
has-trivial-kerᴳ = is-trivial-propᴳ ker-propᴳ
abstract
has-trivial-ker-is-injᴳ : has-trivial-kerᴳ → is-injᴳ φ
has-trivial-ker-is-injᴳ tk g₁ g₂ p =
G.zero-diff-same g₁ g₂ $ tk (G.diff g₁ g₂) $
φ.pres-diff g₁ g₂ ∙ ap (λ h → H.diff h (φ.f g₂)) p ∙ H.inv-r (φ.f g₂)
ker-cst-hom-is-full : ∀ {i j} (G : Group i) (H : Group j)
→ is-fullᴳ (ker-propᴳ (cst-hom {G = G} {H}))
ker-cst-hom-is-full G H g = idp
module _ {i j k} {G : Group i} {H : Group j} {K : Group k}
(φ : G →ᴳ H) (ψ : H →ᴳ K) where
private
module G = Group G
module H = Group H
module K = Group K
module φ = GroupHom φ
module ψ = GroupHom ψ
record is-exact : Type (lmax k (lmax j i)) where
field
im-sub-ker : im-propᴳ φ ⊆ᴳ ker-propᴳ ψ
ker-sub-im : ker-propᴳ ψ ⊆ᴳ im-propᴳ φ
open is-exact public
abstract
im-sub-ker-in : is-fullᴳ (ker-propᴳ (ψ ∘ᴳ φ)) → im-propᴳ φ ⊆ᴳ ker-propᴳ ψ
im-sub-ker-in r h = Trunc-rec (K.El-level _ _) (λ {(g , p) → ap ψ.f (! p) ∙ r g})
im-sub-ker-out : im-propᴳ φ ⊆ᴳ ker-propᴳ ψ → is-fullᴳ (ker-propᴳ (ψ ∘ᴳ φ))
im-sub-ker-out s g = s (φ.f g) [ g , idp ]
module _ {i j} (G : Group i) (H : AbGroup j)
where
private
module G = Group G
module H = AbGroup H
hom-comp : (G →ᴳ H.grp) → (G →ᴳ H.grp) → (G →ᴳ H.grp)
hom-comp φ ψ = group-hom (λ g → H.comp (φ.f g) (ψ.f g)) hom-comp-pres-comp where
module φ = GroupHom φ
module ψ = GroupHom ψ
abstract
hom-comp-pres-comp : ∀ g₁ g₂
→ H.comp (φ.f (G.comp g₁ g₂)) (ψ.f (G.comp g₁ g₂))
== H.comp (H.comp (φ.f g₁) (ψ.f g₁)) (H.comp (φ.f g₂) (ψ.f g₂))
hom-comp-pres-comp g₁ g₂ =
H.comp (φ.f (G.comp g₁ g₂)) (ψ.f (G.comp g₁ g₂))
=⟨ ap2 H.comp (φ.pres-comp g₁ g₂) (ψ.pres-comp g₁ g₂) ⟩
H.comp (H.comp (φ.f g₁) (φ.f g₂)) (H.comp (ψ.f g₁) (ψ.f g₂))
=⟨ H.interchange (φ.f g₁) (φ.f g₂) (ψ.f g₁) (ψ.f g₂) ⟩
H.comp (H.comp (φ.f g₁) (ψ.f g₁)) (H.comp (φ.f g₂) (ψ.f g₂)) =∎
hom-group-structure : GroupStructure (G →ᴳ H.grp)
hom-group-structure = record {M} where
module M where
ident : G →ᴳ H.grp
ident = cst-hom
comp : (G →ᴳ H.grp) → (G →ᴳ H.grp) → (G →ᴳ H.grp)
comp = hom-comp
inv : (G →ᴳ H.grp) → (G →ᴳ H.grp)
inv φ = inv-hom H ∘ᴳ φ
abstract
unit-l : ∀ φ → comp ident φ == φ
unit-l φ = group-hom= $ λ= λ _ → H.unit-l _
assoc : ∀ φ ψ ξ → comp (comp φ ψ) ξ == comp φ (comp ψ ξ)
assoc φ ψ ξ = group-hom= $ λ= λ _ → H.assoc _ _ _
inv-l : ∀ φ → comp (inv φ) φ == ident
inv-l φ = group-hom= $ λ= λ _ → H.inv-l _
hom-group : Group (lmax i j)
hom-group = group (G →ᴳ H.grp) GroupHom-level hom-group-structure
abstract
hom-group-is-abelian : is-abelian hom-group
hom-group-is-abelian φ ψ = group-hom= $ λ= λ g → H.comm _ _
hom-abgroup : AbGroup (lmax i j)
hom-abgroup = hom-group , hom-group-is-abelian
pre∘ᴳ-hom : ∀ {i j k} {G : Group i} {H : Group j} (K : AbGroup k)
→ (G →ᴳ H) → (hom-group H K →ᴳ hom-group G K)
pre∘ᴳ-hom K φ = record { f = _∘ᴳ φ ; pres-comp = lemma}
where abstract lemma = λ _ _ → group-hom= $ λ= λ _ → idp