Algebra.subgroup

-- SUBGROUPS, NORMALITY, and the coset relation.
--
-- A subgroup of (G , g) is a PREDICATE N : G → Ω together with the
-- three closure proofs. Ω-valued is not a stylistic choice: ty-quot
-- quantifies over Ω-valued relations only, and the whole point of a
-- subgroup here is to be quotiented by. It also means membership is
-- PROOF-IRRELEVANT, so none of the closure witnesses can leak into the
-- quotient's data — which is what lets every well-definedness goal
-- below be discharged by supplying a witness and nothing else.
--
-- The closure conditions are themselves propositions of Ω, quantified
-- over G. That is only possible because Ω is IMPREDICATIVE: ∥·∥
-- squashes a Π out of an arbitrary type back into Ω (NovaFoundation,
-- Ω block). A 𝕌-coded subgroup structure would not have been available
-- — G → Ω is large — and would have been the wrong thing anyway.

import Core.prop (∧, andIntro, andFst, andSnd)
import Algebra.group (IsGroup)
import Algebra.groupTheory (gop, ge, ginv, gAssoc, gUnitL, gUnitR, gInvL, gInvR, gCancelInner, gCancelInnerInv, gCancelOuter, gInvUniq, gInvInv, gInvUnit, gOpInv, gCancelL, gCancelR)
import Core.equality (transportP, sym, trans, cong)

hasUnit : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → Ω
hasUnit = λG g N. N (ge g)

closedOp : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → Ω
closedOp = λG g N. ∥(x y : G) → N x → N y → N (gop g x y)∥

closedInv : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → Ω
closedInv = λG g N. ∥(x : G) → N x → N (ginv g x)∥

IsSubgroup : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → Ω
IsSubgroup = λG g N. hasUnit g N ∧ closedOp g N ∧ closedInv g N

-- ===== intro and the three eliminations =====
sgIntro : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → N (ge g)
    → ((x y : G) → N x → N y → N (gop g x y)) → ((x : G) → N x → N (ginv g x)) → IsSubgroup g N
  using (IsSubgroup.eq, hasUnit.eq, closedOp.eq, closedInv.eq)
sgIntro = λG g N u o i. andIntro u (andIntro {} (closedOp g N) (closedInv g N) (⋆ o) (⋆ i))

sgUnit : {G : 𝕌} {g : IsGroup G} {N : G → Ω} → IsSubgroup g N → N (ge g)
  using (IsSubgroup.eq, hasUnit.eq)
sgUnit = λG g N h. andFst h

sgOp : {G : 𝕌} {g : IsGroup G} {N : G → Ω} → IsSubgroup g N → (x y : G) → N x → N y → N (gop g x y)
  using (IsSubgroup.eq, closedOp.unfold)
sgOp = λG g N h x y hx hy. squash-elim (andFst (andSnd h)) (u. u x y hx hy)

sgInv : {G : 𝕌} {g : IsGroup G} {N : G → Ω} → IsSubgroup g N → (x : G) → N x → N (ginv g x)
  using (IsSubgroup.eq, closedInv.unfold)
sgInv = λG g N h x hx. squash-elim (andSnd (andSnd h)) (u. u x hx)

-- ===== normality =====
--
-- Stated as closure under CONJUGATION, x · n · x⁻¹ ∈ N for every x.
-- This is the form the quotient's inner well-definedness proof needs
-- verbatim, and (unlike "xN = Nx") it never mentions a coset.
IsNormal : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → Ω
IsNormal = λG g N. ∥(x n : G) → N n → N (gop g x (gop g n (ginv g x)))∥

nmIntro : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → ((x n : G) → N n → N (gop g x (gop g n (ginv g x)))) → IsNormal g N
  using (IsNormal.eq)
nmIntro = λG g N k. ⋆ k

nmConj : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsNormal g N → (x n : G) → N n → N (gop g x (gop g n (ginv g x)))
  using (IsNormal.unfold)
nmConj = λG g N h x n hn. squash-elim h (u. u x n hn)

-- conjugation by the INVERSE, the shape the quotient's inverse descent
-- wants: x⁻¹ · n · x ∈ N. One gInvInv away from nmConj
nmConjInv : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsNormal g N → (x n : G) → N n → N (gop g (ginv g x) (gop g n x))
nmConjInv =
  λG g N h x n hn. transportP
    N
    cong (λw. G) (λw. gop g (ginv g x) (gop g n w)) (gInvInv g x)
    nmConj _ _ _ h (ginv g x) n hn

-- In an ABELIAN group conjugation is the identity, so normality is
-- automatic — the single most common way a normal subgroup arises, and
-- the reason the corpus's numerical quotients never had to mention it.
abelianConj : {G : 𝕌}
  {g : IsGroup G}
  → ((x y : G) → gop g x y ≡ gop g y x) → (x n : G) → gop g x (gop g n (ginv g x)) ≡ n
abelianConj =
  λG g comm x n. gop g x (gop g n (ginv g x))
    ≡⟨ cong (λw. G) (λw. gop g x w) (comm n (ginv g x)) ⟩ gop g x (gop g (ginv g x) n)
    ≡⟨ gCancelInner g x n ⟩ n

abelianNormal : {G : 𝕌}
  {g : IsGroup G}
  → ((x y : G) → gop g x y ≡ gop g y x) → {N : G → Ω} → IsNormal g N
abelianNormal = λG g comm N. nmIntro (λx n hn. transportP N (sym _ _ (abelianConj comm x n)) hn)

-- ===== the coset relation =====
--
--   x ~ y  ≜  x · y⁻¹ ∈ N
--
-- Ω-valued by construction, since N is. The three equivalence proofs
-- need only that N is a SUBGROUP — normality is what makes the group
-- operation descend, not what makes the relation an equivalence.
cosetRel : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → G → G → Ω
cosetRel = λG g N x y. N (gop g x (ginv g y))

cosetRefl : {G : 𝕌} {g : IsGroup G} {N : G → Ω} → IsSubgroup g N → (x : G) → cosetRel g N x x
  using (cosetRel.eq)
cosetRefl = λG g N s x. transportP N (sym _ _ (gInvR g x)) (sgUnit s)

-- (x · y⁻¹)⁻¹ = y · x⁻¹ — the algebra behind symmetry
cosetFlip : {G : 𝕌} {g : IsGroup G} {x y : G} → ginv g (gop g x (ginv g y)) ≡ gop g y (ginv g x)
cosetFlip =
  λG g x y. ginv g (gop g x (ginv g y))
    ≡⟨ gOpInv g x (ginv g y) ⟩ gop g (ginv g (ginv g y)) (ginv g x)
    ≡⟨ cong (λw. G) (λw. gop g w (ginv g x)) (gInvInv g y) ⟩ gop g y (ginv g x)

cosetSymm : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → IsSubgroup g N → (x y : G) → cosetRel g N x y → cosetRel g N y x
  using (cosetRel.eq)
cosetSymm = λG g N s x y h. transportP N cosetFlip (sgInv s (gop g x (ginv g y)) h)

-- (x · y⁻¹) · (y · z⁻¹) = x · z⁻¹ — the algebra behind transitivity
cosetSplice : {G : 𝕌}
  {g : IsGroup G}
  {x y z : G}
  → gop g (gop g x (ginv g y)) (gop g y (ginv g z)) ≡ gop g x (ginv g z)
cosetSplice =
  λG g x y z. gop g (gop g x (ginv g y)) (gop g y (ginv g z))
    ≡⟨ gAssoc g x (ginv g y) (gop g y (ginv g z)) ⟩ gop g x (gop g (ginv g y) (gop g y (ginv g z)))
    ≡⟨ cong (λw. G) (λw. gop g x w) (gCancelInnerInv g y (ginv g z)) ⟩ gop g x (ginv g z)

cosetTrans : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → IsSubgroup g N → (x y z : G) → cosetRel g N x y → cosetRel g N y z → cosetRel g N x z
  using (cosetRel.eq)
cosetTrans =
  λG g N s x y z hxy hyz. transportP
    N
    cosetSplice
    sgOp s (gop g x (ginv g y)) (gop g y (ginv g z)) hxy hyz