Algebra.groupHom

-- GROUP HOMOMORPHISMS, the quotient map, and the universal property
-- of G/N.
--
-- IsHom is a CODE — the preservation law is stated with Id, exactly as
-- Algebra/monoid.nova/Algebra/group.nova state theirs, so a
-- homomorphism can be bundled into a Σ-code and passed around as data
-- (Natural.algebra.NatAlgHom is the pattern). The ≡-form of the law is
-- recovered once, in homLaw, and nothing below projects out of a Hom
-- again.
--
-- Every accessor here takes ALL of (G, g, H, h) even where it does not
-- need them. That is B-21 discipline, not decoration: a lemma whose two
-- sides are `p .π₁ a` binds only p and a, and the engine can then never
-- instantiate G, g, H or h. Going through homAp puts them in the sides.

import Core.id (Id, idToEq, eqToId)
import Core.prelude (funext)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Algebra.groupTheory (gop, ge, ginv, gAssoc, gUnitL, gUnitR, gInvL, gInvR, gCancelInner, gCancelInnerInv, gCancelOuter, gCancelOuterInv, gInvUniq, gInvInv, gInvUnit, gOpInv, gCancelL, gCancelR, gEqOfOpInvUnit)
import Algebra.subgroup (IsSubgroup, IsNormal, sgUnit, sgOp, sgInv, nmConj, nmConjInv, cosetRel, cosetRefl, cosetSymm, cosetTrans, cosetFlip, cosetSplice)
import Algebra.quotGroup (QGroup, qcls, qclsEq, qclsEffective, qMul, qMulCls, qInv, qInvCls, qUnit, qIsGroup, qFactor, qFactorCls, qFactorUnique)
import Core.equality (transportP, sym, trans, cong)

IsHom : {G : 𝕌} (g : IsGroup G) {H : 𝕌} (h : IsGroup H) → (G → H) → 𝕌
IsHom = λG g H h f. (x y : G) → Id _ (f (gop g x y)) (gop h (f x) (f y))

Hom : {G : 𝕌} (g : IsGroup G) {H : 𝕌} (h : IsGroup H) → 𝕌
Hom = λG g H h. (f : G → H) × IsHom g h f

homAp : {G : 𝕌} {g : IsGroup G} {H : 𝕌} {h : IsGroup H} → Hom g h → G → H using (Hom.unfold)
homAp = λG g H h p a. p .π₁ a

homIntro : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (f : G → H)
  → ((x y : G) → f (gop g x y) ≡ gop h (f x) (f y)) → Hom g h
  using (Hom.unfold, IsHom.unfold)
homIntro = λG g H h f e. f, λx y. eqToId _ _ (e x y)

homLaw : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (p : Hom g h)
  (x y : G)
  → homAp p (gop g x y) ≡ gop h (homAp p x) (homAp p y)
  using (Hom.unfold, IsHom.unfold, homAp.eq)
homLaw = λG g H h p x y. idToEq _ _ _ (p .π₂ x y)

homIntroAp : {G : 𝕌}
  (g : IsGroup G)
  {H : 𝕌}
  (h : IsGroup H)
  (f : G → H)
  (e : (x y : G) → f (gop g x y) ≡ gop h (f x) (f y))
  (a : G)
  → homAp (homIntro f e) a ≡ f a
  using (homAp.eq, homIntro.eq)
homIntroAp = λG g H h f e a. ⋆

-- ===== a homomorphism preserves the unit and inverses =====
--
-- Neither is a law of IsHom: both are consequences of the ONE law,
-- via cancellation. f e · f e = f (e·e) = f e = f e · e, cancel on the
-- left; and f x · f (x⁻¹) = f (x·x⁻¹) = f e = e identifies f (x⁻¹) as
-- the inverse of f x by uniqueness.
homUnit : {G : 𝕌} {g : IsGroup G} {H : 𝕌} {h : IsGroup H} (p : Hom g h) → homAp p (ge g) ≡ ge h
homUnit =
  λG g H h p. gCancelL
    h
    homAp p (ge g)
    gop h (homAp p (ge g)) (homAp p (ge g))
      ≡⟨ sym _ _ (homLaw p (ge g) (ge g)) ⟩ homAp p (gop g (ge g) (ge g))
      ≡⟨ cong (λw. H) (λw. homAp p w) (gUnitL g (ge g)) ⟩ homAp p (ge g)
      ≡⟨ sym _ _ (gUnitR h (homAp p (ge g))) ⟩ gop h (homAp p (ge g)) (ge h)

homInv : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (p : Hom g h)
  (x : G)
  → homAp p (ginv g x) ≡ ginv h (homAp p x)
homInv =
  λG g H h p x. sym
    _
    _
    gInvUniq
      gop h (homAp p x) (homAp p (ginv g x))
        ≡⟨ sym _ _ (homLaw p x (ginv g x)) ⟩ homAp p (gop g x (ginv g x))
        ≡⟨ cong (λw. H) (homAp p) (gInvR g x) ⟩ homAp p (ge g)
        ≡⟨ homUnit p ⟩ ge h

-- and the product of an element with the inverse of another, which is
-- the shape every coset argument is stated in
homOpInv : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (p : Hom g h)
  (x y : G)
  → homAp p (gop g x (ginv g y)) ≡ gop h (homAp p x) (ginv h (homAp p y))
homOpInv =
  λG g H h p x y. homAp p (gop g x (ginv g y))
    ≡⟨ homLaw p x (ginv g y) ⟩ gop h (homAp p x) (homAp p (ginv g y))
    ≡⟨ cong (λw. H) (λw. gop h (homAp p x) w) (homInv p y) ⟩ gop h (homAp p x) (ginv h (homAp p y))

-- ===== bridges: the quotient group's operations, as G/N knows them =====
--
-- qIsGroup packages qMul/qUnit/qInv into an IsGroup, and everything
-- stated against `gop`/`ge`/`ginv` reaches them through its
-- projections. Naming the three correspondences ONCE keeps the
-- projection spine out of every later conversion — the bridge-lemma
-- habit Real.metric.realDistCls established.
qopIsQMul : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (u v : QGroup _ g N)
  → gop (qIsGroup _ _ _ s nn) u v ≡ qMul _ _ _ nn u v
  using (Algebra.groupTheory.gop.eq, Algebra.quotGroup.qIsGroup.eq)
qopIsQMul = λG g N s nn u v. ⋆

qeIsQUnit : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  → ge (qIsGroup _ _ _ s nn) ≡ qUnit _ _ _
  using (Algebra.groupTheory.ge.eq, Algebra.quotGroup.qIsGroup.eq)
qeIsQUnit = λG g N s nn. ⋆

qinvIsQInv : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (u : QGroup _ g N)
  → ginv (qIsGroup _ _ _ s nn) u ≡ qInv _ _ _ s nn u
  using (Algebra.groupTheory.ginv.eq, Algebra.quotGroup.qIsGroup.eq)
qinvIsQInv = λG g N s nn u. ⋆

-- ===== the quotient homomorphism π : G → G/N =====
qProjLaw : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (x y : G)
  → qcls g N (gop g x y) ≡ gop (qIsGroup _ _ _ s nn) (qcls g N x) (qcls g N y)
  using (Algebra.quotGroup.qcls.eq)
qProjLaw =
  λG g N s nn x y. trans
    _
    _
    _
    sym (qMul _ _ _ nn (qcls g N x) (qcls g N y)) (qcls g N (gop g x y)) (qMulCls _ _ _ nn x y)
    sym _ _ (qopIsQMul _ _ _ s nn (qcls g N x) (qcls g N y))

qProj : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  {s : IsSubgroup g N}
  {nn : IsNormal g N}
  → Hom g (qIsGroup _ _ _ s nn)
qProj = λG g N s nn. homIntro (qcls g N) (qProjLaw _ _ _ s nn)

qProjAp : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  {s : IsSubgroup g N}
  {nn : IsNormal g N}
  {a : G}
  → homAp {} _ g _ (qIsGroup _ _ _ s nn) qProj a ≡ qcls _ _ a
  using (qProj.eq)
qProjAp = λG g N s nn a. homIntroAp _ _ (qcls g N) (qProjLaw _ _ _ s nn) a

-- ===== the universal property of G/N =====
--
-- "Any homomorphism killing N factors uniquely through π." The
-- factorisation is Algebra.quotGroup.qFactor — the map half needs no
-- group theory at all, only constancy on cosets — and the group theory
-- enters twice: once to prove that constancy (homKillConst), once to
-- prove that the factored map is again a homomorphism (homQuotLawQ).
--
-- Uniqueness is Algebra.quotGroup.qFactorUnique, which is natAlgebra's
-- natAlgHomUnique with the induction replaced by a quot-elim: agree on
-- every representative, hence on every element, hence — one funext
-- away — as functions.
homKillConst : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (N : G → Ω)
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  (a a' : G)
  → cosetRel g N a a' → homAp p a ≡ homAp p a'
  using (Algebra.subgroup.cosetRel.eq)
homKillConst =
  λG g H h N p kills a a' r. gEqOfOpInvUnit
    _
    trans _ _ _ (sym _ _ (homOpInv p a a')) (kills (gop g a (ginv g a')) r)

homQuotMap : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (N : G → Ω)
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  → QGroup _ g N → H
homQuotMap = λG g H h N p kills u. qFactor _ _ _ (homAp p) (homKillConst N _ kills) u

homQuotMapCls : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  (N : G → Ω)
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  (a : G)
  → homQuotMap N _ kills (class a) ≡ homAp p a
  using (Algebra.quotGroup.QGroup.unfold, homQuotMap.eq)
homQuotMapCls = λG g H h N p kills a. qFactorCls _ _ _ _ (homAp p) (homKillConst N _ kills) a

homQuotLawQ : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {N : G → Ω}
  {nn : IsNormal g N}
  {p : Hom g h}
  {kills : (x : G) → N x → homAp p x ≡ ge h}
  {u v : QGroup _ g N}
  → homQuotMap _ p kills (qMul _ _ _ nn u v)
    ≡ gop h (homQuotMap _ p kills u) (homQuotMap _ p kills v)
  using (Algebra.quotGroup.QGroup.unfold)
homQuotLawQ =
  λG g H h N nn p kills u v. quot-elim
    a. quot-elim
      b. homQuotMap _ p kills (qMul _ _ _ nn (class a) (class b))
        ≡⟨ cong (λw. H) (λw. homQuotMap {} _ _ H _ _ p kills w) (qMulCls _ _ _ nn a b) ⟩
          homQuotMap N _ kills (class (gop g a b))
        ≡⟨ homQuotMapCls N _ kills (gop g a b) ⟩ homAp p (gop g a b)
        ≡⟨ homLaw p a b ⟩ gop h (homAp p a) (homAp p b)
        ≡⟨ cong (λw. H) (λw. gop h w (homAp p b)) (sym _ _ (homQuotMapCls N _ kills a)) ⟩
          gop h (homQuotMap N _ kills (class a)) (homAp p b)
        ≡⟨ cong
          λw. H
          λw. gop h (homQuotMap N _ kills (class a)) w
          sym _ _ (homQuotMapCls N _ kills b) ⟩
          gop h (homQuotMap N _ kills (class a)) (homQuotMap N _ kills (class b))
      v
    u

homQuotLaw : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {N : G → Ω}
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  (u v : QGroup _ g N)
  → homQuotMap _ p kills (gop (qIsGroup _ _ _ s nn) u v)
    ≡ gop h (homQuotMap _ p kills u) (homQuotMap _ p kills v)
homQuotLaw =
  λG g H h N s nn p kills u v. trans
    _
    _
    _
    cong (λw. H) (λw. homQuotMap {} _ _ H _ _ p kills w) (qopIsQMul _ _ _ s nn u v)
    homQuotLawQ

-- EXISTENCE: the factored map, as a homomorphism out of G/N
homQuot : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {N : G → Ω}
  {s : IsSubgroup g N}
  {nn : IsNormal g N}
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  → Hom (qIsGroup _ _ _ s nn) h
homQuot = λG g H h N s nn p kills. homIntro (homQuotMap N _ kills) (homQuotLaw s nn p kills)

-- ...and it factors p through π, on the nose
homQuotFactors : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (p : Hom g h)
  (kills : (x : G) → N x → homAp p x ≡ ge h)
  (a : G)
  → homAp {} (QGroup _ g N) (qIsGroup _ _ _ s nn) H h (homQuot p kills) (qcls g N a) ≡ homAp p a
  using (Algebra.quotGroup.qcls.eq, homQuot.eq)
homQuotFactors =
  λG g H h N s nn p kills a. trans
    _
    homQuotMap _ p kills (qcls g N a)
    _
    homIntroAp {} _ _ _ _ (homQuotMap N _ kills) (homQuotLaw s nn p kills) (qcls g N a)
    homQuotMapCls N _ kills a

-- UNIQUENESS: two homomorphisms out of G/N agreeing after π agree
homQuotUnique : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {N : G → Ω}
  {s : IsSubgroup g N}
  {nn : IsNormal g N}
  {ph ps : Hom (qIsGroup _ _ _ s nn) h}
  → ((a : G) → homAp ph (qcls g N a) ≡ homAp ps (qcls g N a))
    → (u : QGroup _ g N) → homAp ph u ≡ homAp ps u
  using (Algebra.quotGroup.qcls.eq)
homQuotUnique = λG g H h N s nn ph ps e. qFactorUnique _ _ _ _ (homAp ph) (homAp ps) e

-- ...and at FUNCTION level, one funext away
-- (Natural.algebra.natAlgHomUniqueFun)
homQuotUniqueFun : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (ph ps : Hom (qIsGroup _ _ _ s nn) h)
  → ((a : G) → homAp ph (qcls g N a) ≡ homAp ps (qcls g N a)) → homAp ph ≡ homAp ps
homQuotUniqueFun = λG g H h N s nn ph ps e. funext (homQuotUnique e)