--------------------------------------------------------------------------------
Ettore Aldrovandi ealdrovandi@fsu.edu
Keri D'Angelo kd349@cornell.edu
June 2022
--------------------------------------------------------------------------------
This only exists to use the subgroups code from UF-SIP-Examples with
Groups interface. The code is almost literally imported from the
subgroup module in UF-SIP-Examples with minor adaptations, since the
interface defined by Groups is different. This relies on the proof
that the group axioms, as defined in Groups, form a proposition.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan
open import UF.Base hiding (_≈_)
open import UF.Classifiers
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Powerset
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence
open import Groups.Type renaming (_≅_ to _≣_)
module Groups.Subgroups
(𝓤 : Universe)
(ua : Univalence) where
fe : ∀ {𝓥} {𝓦} → funext 𝓥 𝓦
fe {𝓥} {𝓦} = univalence-gives-funext' 𝓥 𝓦 (ua 𝓥) (ua (𝓥 ⊔ 𝓦))
module _ (G : Group 𝓤) where
private
_·_ : ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
_·_ = multiplication G
e : ⟨ G ⟩
e = unit G
infixl 42 _·_
group-closed : (⟨ G ⟩ → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
group-closed 𝓐 = 𝓐 (unit G)
× ((x y : ⟨ G ⟩) → 𝓐 x → 𝓐 y → 𝓐 (x · y))
× ((x : ⟨ G ⟩) → 𝓐 x → 𝓐 (inv G x))
Subgroup : 𝓤 ⁺ ̇
Subgroup = Σ A ꞉ 𝓟 ⟨ G ⟩ , group-closed (_∈ A)
⟪_⟫ : Subgroup → 𝓟 ⟨ G ⟩
⟪ A , u , c , ι ⟫ = A
being-group-closed-subset-is-prop : (A : 𝓟 ⟨ G ⟩)
→ is-prop (group-closed (_∈ A))
being-group-closed-subset-is-prop A = ×-is-prop
(∈-is-prop A (unit G))
(×-is-prop
(Π-is-prop fe
(λ x → Π-is-prop fe
(λ y → Π-is-prop fe
(λ _ → Π-is-prop fe
(λ _ → ∈-is-prop A (x · y))))))
(Π-is-prop fe
(λ x → Π-is-prop fe
(λ _ → ∈-is-prop A (inv G x)))))
⟪⟫-is-embedding : is-embedding ⟪_⟫
⟪⟫-is-embedding = pr₁-is-embedding being-group-closed-subset-is-prop
ap-⟪⟫ : (S T : Subgroup) → S ＝ T → ⟪ S ⟫ ＝ ⟪ T ⟫
ap-⟪⟫ S T = ap ⟪_⟫
ap-⟪⟫-is-equiv : (S T : Subgroup) → is-equiv (ap-⟪⟫ S T)
ap-⟪⟫-is-equiv = embedding-gives-embedding' ⟪_⟫ ⟪⟫-is-embedding
subgroups-form-a-set : is-set Subgroup
subgroups-form-a-set {S} {T} = equiv-to-prop
(ap-⟪⟫ S T , ap-⟪⟫-is-equiv S T)
(𝓟-is-set ua)
subgroup-equality : (S T : Subgroup)
→ (S ＝ T)
≃ ((x : ⟨ G ⟩) → (x ∈ ⟪ S ⟫) ↔ (x ∈ ⟪ T ⟫))
subgroup-equality S T = γ
where
f : S ＝ T → (x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ↔ x ∈ ⟪ T ⟫
f p x = transport (λ - → x ∈ ⟪ - ⟫) p , transport (λ - → x ∈ ⟪ - ⟫) (p ⁻¹)
h : ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ↔ x ∈ ⟪ T ⟫) → ⟪ S ⟫ ＝ ⟪ T ⟫
h φ = subset-extensionality' ua α β
where
α : ⟪ S ⟫ ⊆ ⟪ T ⟫
α x = lr-implication (φ x)
β : ⟪ T ⟫ ⊆ ⟪ S ⟫
β x = rl-implication (φ x)
g : ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ↔ x ∈ ⟪ T ⟫) → S ＝ T
g = inverse (ap-⟪⟫ S T) (ap-⟪⟫-is-equiv S T) ∘ h
γ : (S ＝ T) ≃ ((x : ⟨ G ⟩) → x ∈ ⟪ S ⟫ ↔ x ∈ ⟪ T ⟫)
γ = logically-equivalent-props-are-equivalent
subgroups-form-a-set
(Π-is-prop fe
(λ x → ×-is-prop
(Π-is-prop fe (λ _ → ∈-is-prop ⟪ T ⟫ x))
(Π-is-prop fe (λ _ → ∈-is-prop ⟪ S ⟫ x)))) f g
T : 𝓤 ̇ → 𝓤 ̇
T X = Σ _·_ ꞉ group-structure X , group-axioms X _·_
module _ {X : 𝓤 ̇ } (h : X → ⟨ G ⟩) (e : is-embedding h) where
private
h-lc : left-cancellable h
h-lc = embeddings-are-lc h e
having-group-closed-fiber-is-prop : is-prop (group-closed (fiber h))
having-group-closed-fiber-is-prop = being-group-closed-subset-is-prop
(λ x → (fiber h x , e x))
at-most-one-homomorphic-structure : is-prop (Σ τ ꞉ T X , is-hom (X , τ) G h)
at-most-one-homomorphic-structure ((_*_ , gaxiom) , pmult) ((_*'_ , gaxiom') , pmult')
= to-subtype-＝ (λ τ → being-hom-is-prop fe ((X , τ)) G h) δ
where
τ τ' : T X
τ = _*_ , gaxiom
τ' = _*'_ , gaxiom'
p : _*_ ＝ _*'_
p = dfunext fe (λ x → dfunext fe (λ y → h-lc ( h (x * y) ＝⟨ pmult ⟩
h x · h y ＝⟨ pmult' ⁻¹ ⟩
h (x *' y) ∎)))
δ : τ ＝ τ'
δ = to-subtype-＝ (λ _ → group-axioms-is-prop fe X _) p
group-closed-fiber-gives-homomorphic-structure : funext 𝓤 𝓤
→ group-closed (fiber h)
→ (Σ τ ꞉ T X , is-hom (X , τ) G h)
group-closed-fiber-gives-homomorphic-structure fe (unitc , mulc , invc) = τ , i
where
φ : (x : X) → fiber h (h x)
φ x = (x , 𝓻𝓮𝒻𝓵 (h x))
unitH : X
unitH = fiber-point unitc
_*_ : X → X → X
x * y = fiber-point (mulc (h x) (h y) (φ x) (φ y))
invH : X → X
invH x = fiber-point (invc (h x) (φ x))
pmul : (x y : X) → h (x * y) ＝ h x · h y
pmul x y = fiber-identification (mulc (h x) (h y) (φ x) (φ y))
punit : h unitH ＝ unit G
punit = fiber-identification unitc
pinv : (x : X) → h (invH x) ＝ inv G (h x)
pinv x = fiber-identification (invc (h x) (φ x))
unitH-left : (x : X) → unitH * x ＝ x
unitH-left x = h-lc (h (unitH * x) ＝⟨ pmul unitH x ⟩
h unitH · h x ＝⟨ ap (_· h x) punit ⟩
unit G · h x ＝⟨ unit-left G (h x) ⟩
h x ∎)
unitH-right : (x : X) → x * unitH ＝ x
unitH-right x = h-lc (h (x * unitH) ＝⟨ pmul x unitH ⟩
h x · h unitH ＝⟨ ap (h x ·_) punit ⟩
h x · unit G ＝⟨ unit-right G (h x) ⟩
h x ∎)
assocH : (x y z : X) → ((x * y) * z) ＝ (x * (y * z))
assocH x y z = h-lc (h ((x * y) * z) ＝⟨ pmul (x * y) z ⟩
h (x * y) · h z ＝⟨ ap (_· h z) (pmul x y) ⟩
(h x · h y) · h z ＝⟨ assoc G (h x) (h y) (h z) ⟩
h x · (h y · h z) ＝⟨ (ap (h x ·_) (pmul y z))⁻¹ ⟩
h x · h (y * z) ＝⟨ (pmul x (y * z))⁻¹ ⟩
h (x * (y * z)) ∎)
group-axiomH : (x : X) → Σ x' ꞉ X , (x' * x ＝ unitH) × (x * x' ＝ unitH)
group-axiomH x = invH x , h-lc (h (invH x * x) ＝⟨ pmul (invH x) x ⟩
h (invH x) · h x ＝⟨ ap (_· h x) (pinv x) ⟩
inv G (h x) · h x ＝⟨ inv-left G (h x) ⟩
unit G ＝⟨ punit ⁻¹ ⟩
h unitH ∎) ,
h-lc (h (x * invH x) ＝⟨ pmul x (invH x) ⟩
h x · h (invH x) ＝⟨ ap (h x ·_) (pinv x) ⟩
h x · inv G (h x) ＝⟨ inv-right G (h x) ⟩
unit G ＝⟨ punit ⁻¹ ⟩
h unitH ∎)
j : is-set X
j = subtypes-of-sets-are-sets' h h-lc (groups-are-sets G)
τ : T X
τ = _*_ , (j , (assocH , unitH , (unitH-left , (unitH-right , group-axiomH))))
i : is-hom (X , τ) G h
i {x} {y} = pmul x y
homomorphic-structure-gives-group-closed-fiber : (Σ τ ꞉ T X , is-hom (X , τ) G h)
→ group-closed (fiber h)
homomorphic-structure-gives-group-closed-fiber ((_*_ , gaxiom) , pmult) = (unitc , mulc , invc)
where
H : Group 𝓤
H = X , (_*_ , gaxiom)
unitH : X
unitH = pr₁ (pr₂ (pr₂ gaxiom))
unitc : fiber h (unit G)
unitc = unitH , (homs-preserve-unit H G h pmult)
mulc : ((x y : ⟨ G ⟩) → fiber h x → fiber h y → fiber h (x · y))
mulc x y (a , p) (b , q) = (a * b) ,
(h (a * b) ＝⟨ pmult {a} {b} ⟩
h a · h b ＝⟨ ap₂ (λ - -' → - · -') p q ⟩
x · y ∎)
invc : ((x : ⟨ G ⟩) → fiber h x → fiber h (inv G x))
invc x (a , p) = inv H a ,
(h (inv H a) ＝⟨ homs-preserve-invs H G h pmult a ⟩
inv G (h a) ＝⟨ ap (inv G) p ⟩
inv G x ∎)
fiber-structure-lemma : funext 𝓤 𝓤
→ group-closed (fiber h)
≃ (Σ τ ꞉ T X , is-hom (X , τ) G h)
fiber-structure-lemma fe = logically-equivalent-props-are-equivalent
having-group-closed-fiber-is-prop
at-most-one-homomorphic-structure
(group-closed-fiber-gives-homomorphic-structure fe)
homomorphic-structure-gives-group-closed-fiber
characterization-of-the-type-of-subgroups : Subgroup ≃ (Σ H ꞉ Group 𝓤
, Σ h ꞉ (⟨ H ⟩ → ⟨ G ⟩)
, is-embedding h
× is-hom H G h)
characterization-of-the-type-of-subgroups =
Subgroup ≃⟨ i ⟩
(Σ A ꞉ 𝓟 ⟨ G ⟩ , group-closed (_∈ A)) ≃⟨ ii ⟩
(Σ (X , h , e) ꞉ Subtype ⟨ G ⟩ , group-closed (fiber h)) ≃⟨ iii ⟩
(Σ X ꞉ 𝓤 ̇ , Σ (h , e) ꞉ X ↪ ⟨ G ⟩ , group-closed (fiber h)) ≃⟨ iv ⟩
(Σ X ꞉ 𝓤 ̇ , Σ (h , e) ꞉ X ↪ ⟨ G ⟩ , Σ τ ꞉ T X , is-hom (X , τ) G h) ≃⟨ v ⟩
(Σ X ꞉ 𝓤 ̇ , Σ h ꞉ (X → ⟨ G ⟩) , Σ e ꞉ is-embedding h , Σ τ ꞉ T X , is-hom (X , τ) G h) ≃⟨ vi ⟩
(Σ X ꞉ 𝓤 ̇ , Σ h ꞉ (X → ⟨ G ⟩) , Σ τ ꞉ T X , Σ e ꞉ is-embedding h , is-hom (X , τ) G h) ≃⟨ vii ⟩
(Σ X ꞉ 𝓤 ̇ , Σ τ ꞉ T X , Σ h ꞉ (X → ⟨ G ⟩) , is-embedding h × is-hom (X , τ) G h) ≃⟨ viii ⟩
(Σ H ꞉ Group 𝓤 , Σ h ꞉ (⟨ H ⟩ → ⟨ G ⟩) , is-embedding h × is-hom H G h) ■
where
open special-classifier-single-universe 𝓤
φ : Subtype ⟨ G ⟩ → 𝓟 ⟨ G ⟩
φ = χ-special is-prop ⟨ G ⟩
j : is-equiv φ
j = χ-special-is-equiv (ua 𝓤) fe is-prop ⟨ G ⟩
i = ≃-refl Subgroup
ii = ≃-sym (Σ-change-of-variable (λ (A : 𝓟 ⟨ G ⟩) → group-closed (_∈ A)) φ j)
iii = Σ-assoc
iv = Σ-cong (λ X → Σ-cong (λ (h , e) → fiber-structure-lemma h e fe))
v = Σ-cong (λ X → Σ-assoc)
vi = Σ-cong (λ X → Σ-cong (λ h → Σ-flip))
vii = Σ-cong (λ X → Σ-flip)
viii = ≃-sym Σ-assoc
induced-group : Subgroup → Group 𝓤
induced-group S = pr₁ (⌜ characterization-of-the-type-of-subgroups ⌝ S)
\end{code}