{-# OPTIONS --without-K #-} open import lib.Basics open import lib.NType2 open import lib.types.Group open import lib.types.Sigma open import lib.types.Truncation open import lib.groups.Homomorphisms module lib.groups.PropSubgroup where module _ {i} (G : Group i) where private module G = Group G module PropSubgroup {j} (P : G.El → Type j) (P-level : ∀ g → has-level ⟨-1⟩ (P g)) (P-ident : P G.ident) (P-inv : ∀ {g} → P g → P (G.inv g)) (P-comp : ∀ {g₁ g₂} → P g₁ → P g₂ → P (G.comp g₁ g₂)) where struct : GroupStructure (Σ G.El P) struct = record { ident = (G.ident , P-ident); inv = λ {(g , p) → (G.inv g , P-inv p)}; comp = λ {(g₁ , p₁) (g₂ , p₂) → (G.comp g₁ g₂ , P-comp p₁ p₂)}; unitl = λ {(g , _) → pair= (G.unitl g) (prop-has-all-paths-↓ (P-level _))}; unitr = λ {(g , _) → pair= (G.unitr g) (prop-has-all-paths-↓ (P-level _))}; assoc = λ {(g₁ , _) (g₂ , _) (g₃ , _) → pair= (G.assoc g₁ g₂ g₃) (prop-has-all-paths-↓ (P-level _))}; invl = λ {(g , _) → pair= (G.invl g) (prop-has-all-paths-↓ (P-level _))}; invr = λ {(g , _) → pair= (G.invr g) (prop-has-all-paths-↓ (P-level _))}} Subgroup : Group (lmax i j) Subgroup = group _ (Σ-level G.El-level (raise-level _ ∘ P-level)) struct inj : Subgroup →ᴳ G inj = record { f = λ {(g , _) → g}; pres-comp = λ _ _ → idp} module _ {j} {H : Group j} (φ : H →ᴳ G) where private module H = Group H module φ = GroupHom φ prop-hom : Π H.El (P ∘ φ.f) → (H →ᴳ Subgroup) prop-hom p = record { f = λ g → (φ.f g , p g); pres-comp = λ g₁ g₂ → pair= (φ.pres-comp g₁ g₂) (prop-has-all-paths-↓ (P-level _))} module _ {i} {j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where private module G = Group G module H = Group H module φ = GroupHom φ module Ker = PropSubgroup G (λ g → φ.f g == H.ident) (λ g → H.El-level _ _) φ.pres-ident (λ p → φ.pres-inv _ ∙ ap H.inv p ∙ group-inv-ident H) (λ p₁ p₂ → φ.pres-comp _ _ ∙ ap2 H.comp p₁ p₂ ∙ H.unitl _) module Im = PropSubgroup H (λ h → Trunc ⟨-1⟩ (Σ G.El (λ g → φ.f g == h))) (λ h → Trunc-level) ([ G.ident , φ.pres-ident ]) (Trunc-fmap (λ {(g , p) → (G.inv g , φ.pres-inv g ∙ ap H.inv p)})) (Trunc-fmap2 (λ {(g₁ , p₁) (g₂ , p₂) → (G.comp g₁ g₂ , φ.pres-comp g₁ g₂ ∙ ap2 H.comp p₁ p₂)})) open Ker public renaming (struct to ker-struct; Subgroup to Ker; inj to ker-inj; prop-hom to ker-hom) open Im public renaming (struct to im-struct; Subgroup to Im; inj to im-inj; prop-hom to im-out-hom) im-in-hom : G →ᴳ Im im-in-hom = record { f = λ g → (φ.f g , [ g , idp ]); pres-comp = λ g₁ g₂ → pair= (φ.pres-comp g₁ g₂) (prop-has-all-paths-↓ Trunc-level)} im-in-surj : (h : Group.El Im) → Trunc ⟨-1⟩ (Σ G.El (λ g → GroupHom.f im-in-hom g == h)) im-in-surj (_ , s) = Trunc-fmap (λ {(g , p) → (g , pair= p (prop-has-all-paths-↓ Trunc-level))}) s