Algebra.quotGroup

-- THE QUOTIENT GROUP G/N — carrier and operation.
--
-- The carrier is the plain quotient of G by the coset relation. What
-- takes work is the OPERATION, and this module is where the corpus's
-- quotient machinery is finally exercised on a NON-COMMUTATIVE
-- structure.
--
-- A binary operation on a quotient descends by a NESTED quot-elim and
-- so owes TWO well-definedness proofs: an inner one (the second
-- argument moves) and an outer one (the first argument moves). Every
-- other instance in this corpus — realAdd, realMul, realLattice,
-- realSeq, rationalQ — discharges the outer one by COMMUTING, through
-- Real.seq.wdOuterOfComm or its ℚ-level twin: prove the inner case,
-- then swap. A group has no commutativity to swap with, so both halves
-- are proved here directly, and the two turn out to be genuinely
-- different statements:
--
--   INNER   b ~ b' ⟹ a·b ~ a·b'   is   (a·b)·(a·b')⁻¹ = a·(b·b'⁻¹)·a⁻¹,
--           the hypothesis CONJUGATED by a. It holds exactly because N
--           is NORMAL, and this is the only place normality is used.
--
--   OUTER   a ~ a' ⟹ a·b ~ a'·b   is   (a·b)·(a'·b)⁻¹ = a·a'⁻¹,
--           the hypothesis UNCHANGED — b and b⁻¹ annihilate in the
--           middle. It needs no normality at all, and would hold for
--           any subgroup.
--
-- So the half the rest of the corpus gets for free is here the half
-- that is free for a different reason, and the half that looks routine
-- is the one carrying the mathematical content. Commuting had been
-- hiding the asymmetry, not exploiting it.

import Core.id (Id, eqToId)
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)
import Algebra.subgroup (IsSubgroup, IsNormal, sgUnit, sgOp, sgInv, nmConj, nmConjInv, cosetRel, cosetRefl, cosetSymm, cosetTrans, cosetFlip, cosetSplice)
import Core.quotEffective (classEqOfRel, effectiveAtEquiv)
import Core.equality (transportP, sym, trans, cong)

QGroup : (G : 𝕌) (g : IsGroup G) (N : G → Ω) → 𝕌
QGroup = λG g N. G / (x y. cosetRel g N x y)

-- The class map, NAMED. It is `class` and nothing else, and one could
-- write `class` everywhere instead — except in the well-definedness
-- lemmas below, where the name is load-bearing.
--
-- A discharge candidate binds its parameters by matching its two
-- SIDES; the equation's type is not matched (there is no type slot on
-- a candidate). A lemma stated as
--
--   class (gop G g a b) ≡ class (gop G g a b') ∈ (QGroup G g N)
--
-- therefore binds G, g, a, b, b' — and never N, which occurs only in
-- the type. An unbound parameter that is not ≡-, 𝟙- or prop-typed
-- cannot be completed, so the candidate is unusable and the descent's
-- well-definedness obligation is reported with no hint. Routing the
-- two sides through `qcls G g N` puts N back where the matcher can
-- see it, and the same lemma then fires.
--
-- The mirror image holds one step later: a quot-elim substitutes the
-- BARE `class a` for its method binder, so the lemmas that say what
-- the descended operations DO on classes (qMulCls, qInvCls) have to be
-- stated with bare `class`. Both spellings are needed, for opposite
-- reasons.
qcls : {G : 𝕌} (g : IsGroup G) (N : G → Ω) → G → QGroup _ g N using (QGroup.unfold)
qcls = λG g N a. class a

-- EFFECTIVITY. Core/quotEffective.nova's point is that class equality
-- gives back the equivalence CLOSURE of the relation, not the relation
-- — unless the relation already is an equivalence.
-- Algebra/subgroup.nova proved that the coset relation is one, so here
-- effectivity holds on the nose and the quotient's equality IS "differ
-- by an element of N".
qclsEq : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → IsSubgroup g N → (a b : G) → cosetRel g N a b → qcls g N a ≡ qcls _ _ b
  using (qcls.eq)
qclsEq = λG g N s a b h. classEqOfRel (cosetRel g N) _ _ h

qclsEffective : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsSubgroup g N → (a b : G) → (qcls g N a ≡ qcls _ _ b) → cosetRel g N a b
  using (qcls.eq)
qclsEffective = λG g N s. effectiveAtEquiv (cosetRel g N) (cosetRefl s) (cosetTrans s) (cosetSymm s)

-- ===== the algebra behind the two halves =====
-- INNER:  (a·b)·(a·b')⁻¹  =  a · ((b·b'⁻¹) · a⁻¹)
qMulInnerAlg : {G : 𝕌}
  {g : IsGroup G}
  {a b b' : G}
  → gop g a (gop g (gop g b (ginv g b')) (ginv g a)) ≡ gop g (gop g a b) (ginv g (gop g a b'))
qMulInnerAlg =
  λG g a b b'. gop g a (gop g (gop g b (ginv g b')) (ginv g a))
    ≡⟨ cong (λw. G) (λw. gop g a w) (gAssoc g b (ginv g b') (ginv g a)) ⟩
      gop g a (gop g b (gop g (ginv g b') (ginv g a)))
    ≡⟨ sym _ _ (gAssoc g a b (gop g (ginv g b') (ginv g a))) ⟩
      gop g (gop g a b) (gop g (ginv g b') (ginv g a))
    ≡⟨ cong (λw. G) (λw. gop g (gop g a b) w) (sym _ _ (gOpInv g a b')) ⟩
      gop g (gop g a b) (ginv g (gop g a b'))

-- OUTER:  (a·b)·(a'·b)⁻¹  =  a·a'⁻¹
qMulOuterAlg : (G : 𝕌)
  (g : IsGroup G)
  (a a' b : G)
  → gop g (gop g a b) (ginv g (gop g a' b)) ≡ gop g a (ginv g a')
qMulOuterAlg =
  λG g a a' b. gop g (gop g a b) (ginv g (gop g a' b))
    ≡⟨ cong (λw. G) (λw. gop g (gop g a b) w) (gOpInv g a' b) ⟩
      gop g (gop g a b) (gop g (ginv g b) (ginv g a'))
    ≡⟨ gAssoc g a b (gop g (ginv g b) (ginv g a')) ⟩
      gop g a (gop g b (gop g (ginv g b) (ginv g a')))
    ≡⟨ cong (λw. G) (λw. gop g a w) (gCancelInner g b (ginv g a')) ⟩ gop g a (ginv g a')

-- ===== the two well-definedness proofs, at relation level =====
qMulWDInner : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → IsNormal g N → {a b b' : G} → cosetRel g N b b' → cosetRel g N (gop g a b) (gop g a b')
  using (cosetRel.eq)
qMulWDInner =
  λG g N nn a b b' h. transportP
    N
    {gop g a (gop g (gop g b (ginv g b')) (ginv g a))}
    {gop g (gop g a b) (ginv g (gop g a b'))}
    qMulInnerAlg
    nmConj _ _ _ nn a (gop g b (ginv g b')) h

qMulWDOuter : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  {a a' b : G}
  → cosetRel g N a a' → cosetRel g N (gop g a b) (gop g a' b)
  using (cosetRel.eq)
qMulWDOuter = λG g N a a' b h. transportP N (sym _ _ (qMulOuterAlg _ g a a' b)) h

-- ===== the same two, at class level =====
qMulWDInnerCls : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsNormal g N → (a b b' : G) → cosetRel g N b b' → qcls g N (gop g a b) ≡ qcls _ _ (gop g a b')
  using (qcls.eq)
qMulWDInnerCls =
  λG g N nn a b b' h. classEqOfRel (cosetRel g N) (gop g a b) (gop g a b') (qMulWDInner nn h)

qMulWDOuterCls : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  {a a' b : G}
  → cosetRel g N a a' → qcls g N (gop g a b) ≡ qcls _ _ (gop g a' b)
  using (qcls.eq)
qMulWDOuterCls =
  λG g N a a' b h. classEqOfRel (cosetRel g N) (gop g a b) (gop g a' b) (qMulWDOuter h)

-- the outer half as the descent itself asks for it: the two inner
-- eliminations agree on every element of the quotient. Where realMul
-- writes `wdOuterOfComm rMul rMulComm rMulWDInnerCls`, this is the
-- honest version — a quot-elim at an ≡-motive whose method is the
-- class-level outer proof
qMulWDOuterElim : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsNormal g N
    → (x x' : G)
      → cosetRel g N x x'
        → (v : QGroup _ g N)
          → quot-elim (w. QGroup _ g N) (q. qcls _ _ (gop g x q)) v
            ≡ quot-elim (q. qcls _ _ (gop g x' q)) v
  using (QGroup.unfold, qMulWDInnerCls)
qMulWDOuterElim =
  λG g N nn x x' h v. quot-elim
    w. quot-elim (z. QGroup _ g N) (q. qcls _ _ (gop g x q)) w
      ≡ quot-elim (q. qcls _ _ (gop g x' q)) w
    c. qMulWDOuterCls h
    v

-- ===== the descended operation =====
qMul : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsNormal g N → QGroup _ g N → QGroup _ g N → QGroup _ g N
  using (QGroup.unfold, qMulWDInnerCls, qMulWDOuterElim)
qMul = λG g N nn u v. quot-elim (p. quot-elim (q. qcls _ _ (gop g p q)) v) u

-- β on classes. Stated with the BARE `class`, not with qcls: a
-- quot-elim substitutes `class a` for its method binder, so this is
-- the spelling every goal below is actually in. (The well-definedness
-- lemmas above must go the other way — see the note at qcls.)
qMulCls : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (nn : IsNormal g N)
  (a b : G)
  → qMul _ _ _ nn (class a) (class b) ≡ class (gop g a b)
  using (QGroup.unfold, qcls.eq, qMul.eq)
qMulCls = λG g N nn a b. ⋆

-- ===== the inverse descends =====
--
-- The relation-level statement is  a ~ a' ⟹ a⁻¹ ~ a'⁻¹,  i.e.
-- a·a'⁻¹ ∈ N ⟹ a⁻¹·a' ∈ N. Read the second as the FIRST turned round
-- (a'·a⁻¹ ∈ N, by symmetry of the coset relation) and then conjugated
-- by a⁻¹: normality again, in nmConjInv's inverse-side spelling.
qInvAlg : {G : 𝕌}
  {g : IsGroup G}
  {a a' : G}
  → gop g (ginv g a) (gop g (gop g a' (ginv g a)) a) ≡ gop g (ginv g a) (ginv g (ginv g a'))
qInvAlg =
  λG g a a'. gop g (ginv g a) (gop g (gop g a' (ginv g a)) a)
    ≡⟨ cong (λw. G) (λw. gop g (ginv g a) w) (gCancelOuterInv g a a') ⟩ gop g (ginv g a) a'
    ≡⟨ cong (λw. G) (λw. gop g (ginv g a) w) (sym _ _ (gInvInv g a')) ⟩
      gop g (ginv g a) (ginv g (ginv g a'))

qInvWD : {G : 𝕌}
  {g : IsGroup G}
  {N : G → Ω}
  → IsSubgroup g N
    → IsNormal g N → {a a' : G} → cosetRel g N a a' → cosetRel g N (ginv g a) (ginv g a')
  using (cosetRel.eq)
qInvWD =
  λG g N s nn a a' h. transportP
    N
    {gop g (ginv g a) (gop g (gop g a' (ginv g a)) a)}
    {gop g (ginv g a) (ginv g (ginv g a'))}
    qInvAlg
    nmConjInv _ _ _ nn a (gop g a' (ginv g a)) (cosetSymm s _ _ h)

qInvWDCls : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsSubgroup g N
    → IsNormal g N → (a a' : G) → cosetRel g N a a' → qcls g N (ginv g a) ≡ qcls _ _ (ginv g a')
  using (qcls.eq)
qInvWDCls = λG g N s nn a a' h. classEqOfRel (cosetRel g N) _ _ (qInvWD s nn h)

qInv : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsSubgroup g N → IsNormal g N → QGroup _ g N → QGroup _ g N
  using (QGroup.unfold, qInvWDCls)
qInv = λG g N s nn u. quot-elim (a. qcls _ _ (ginv g a)) u

qInvCls : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (a : G)
  → qInv _ _ _ s nn (class a) ≡ class (ginv g a)
  using (QGroup.unfold, qcls.eq, qInv.eq)
qInvCls = λG g N s nn a. ⋆

qUnit : (G : 𝕌) (g : IsGroup G) (N : G → Ω) → QGroup _ g N using (QGroup.unfold)
qUnit = λG g N. class (ge g)

-- ===== the group laws, each a descent into an Ω-valued motive =====
--
-- These are the corpus's first uses of the `<lemma>.rw` license. The
-- discharge engine does NOT rewrite with store lemmas by default: a
-- cited lemma is available for WHOLE-EQUATION match and for hops, and
-- rwNfElem only runs at all when the site cites `hyp.rw` or some
-- `<lemma>.rw`. Everything in Algebra/groupTheory.nova and
-- Algebra/subgroup.nova gets by on whole-equation match plus congruence
-- descent, which is why no .rw appears before this point. Here it is
-- unavoidable: the base case of every law has qMul applied to two
-- classes NESTED inside another qMul, and only a rewrite reaches the
-- inner one. `qMulCls.rw` does exactly that and nothing else.
--
-- The last step of each base case is an explicit `cong` rather than a
-- ⋆. Class-congruence in the engine (spCongC) accepts only STEP-FREE
-- evidence — pure computation — because the component's type is not
-- known there, so `class X ≐ class Y` never closes by a lemma about
-- X and Y. Naming the congruence is the whole fix, and it is the same
-- move Algebra/groupTheory.nova needed against gAssoc.
--
-- Every law below is an EQUATION, hence Ω-valued, hence its quot-elim
-- owes no well-definedness proof at all: proof irrelevance closes the
-- coherence outright (el-prf-prop). That is the whole difference
-- between milestone 2 and this one — descending DATA costs two honest
-- proofs, descending a PROPOSITION costs nothing, and the corpus's
-- Ω/𝕌 split is what makes the second half free.
qAssoc : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (nn : IsNormal g N)
  (u v w : QGroup _ g N)
  → qMul _ _ _ nn (qMul _ _ _ nn u v) w ≡ qMul _ _ _ nn u (qMul _ _ _ nn v w)
  using (QGroup.unfold, qMulCls.rw)
qAssoc =
  λG g N nn u v w. quot-elim
    a. quot-elim
      b. quot-elim
        c. trans
          _
          _
          _
          ⋆
          trans
            _
            _
            qMul _ _ _ nn (class a) (qMul _ _ _ nn (class b) (class c))
            cong (λw. QGroup _ g N) (λw. class w) (gAssoc g a b c)
            ⋆
        w
      v
    u

qUnitL : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (nn : IsNormal g N)
  (u : QGroup _ g N)
  → qMul _ _ _ nn (qUnit _ g N) u ≡ u
  using (QGroup.unfold, qUnit.eq, qMulCls.rw)
qUnitL =
  λG g N nn u. quot-elim (a. trans _ _ _ ⋆ (cong (λw. QGroup _ g N) (λw. class w) (gUnitL g a))) u

qUnitR : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (nn : IsNormal g N)
  (u : QGroup _ g N)
  → qMul _ _ _ nn u (qUnit _ g N) ≡ u
  using (QGroup.unfold, qUnit.eq, qMulCls.rw)
qUnitR =
  λG g N nn u. quot-elim (a. trans _ _ _ ⋆ (cong (λw. QGroup _ g N) (λw. class w) (gUnitR g a))) u

qInvLaw : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (u : QGroup _ g N)
  → qMul _ _ _ nn (qInv _ _ _ s nn u) u ≡ qUnit _ _ _
  using (QGroup.unfold, qUnit.eq, qInvCls.rw, qMulCls.rw)
qInvLaw =
  λG g N s nn u. quot-elim (a. trans _ _ _ ⋆ (cong (λw. QGroup _ g N) (λw. class w) (gInvL g a))) u

qInvLawR : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (s : IsSubgroup g N)
  (nn : IsNormal g N)
  (u : QGroup _ g N)
  → qMul _ _ _ nn u (qInv _ _ _ s nn u) ≡ qUnit _ _ _
  using (QGroup.unfold, qUnit.eq, qInvCls.rw, qMulCls.rw)
qInvLawR =
  λG g N s nn u. quot-elim (a. trans _ _ _ ⋆ (cong (λw. QGroup _ g N) (λw. class w) (gInvR g a))) u

-- ===== G/N is a group =====
qIsGroup : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsSubgroup g N → IsNormal g N → IsGroup (QGroup _ g N)
  using (Algebra.group.IsGroup.unfold, Algebra.monoid.IsMonoid.unfold)
qIsGroup =
  λG g N s nn. (,)
    (,)
      qMul _ _ _ nn
      qUnit _ _ _
      λx y z. eqToId _ _ (qAssoc _ _ _ nn x y z)
      λx. eqToId _ _ (qUnitL _ _ _ nn x)
      λx. eqToId _ _ (qUnitR _ _ _ nn x)
    qInv _ _ _ s nn
    λx. eqToId _ _ (qInvLaw _ _ _ s nn x)
    λx. eqToId _ _ (qInvLawR _ _ _ s nn x)

qMonoid : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  → IsSubgroup g N → IsNormal g N → IsMonoid (QGroup _ g N)
  using (Algebra.group.IsGroup.unfold)
qMonoid = λG g N s nn. qIsGroup _ _ _ s nn .π₁

-- ===== the quotient's universal property, at FUNCTION level =====
--
-- Before any homomorphism: a map out of G/N is exactly a map out of G
-- that is constant on cosets. This is Core/bracket.nova's brElim with a
-- non-trivial relation in place of ∥𝟙∥, and it is stated here because
-- it is where the constancy proof is CHEAPEST to discharge — `c` is a
-- context hypothesis of the very shape the quot-elim's well-definedness
-- goal has, so the engine finds it without any of B-21's parameter
-- bookkeeping. Every later factorisation goes through this one and
-- never writes a quot-elim of its own.
qFactor : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  {H : 𝕌}
  (k : G → H)
  (c : (a a' : G) → cosetRel g N a a' → k a ≡ k a')
  (u : QGroup _ g N)
  → H
  using (QGroup.unfold)
qFactor = λG g N H k c u. quot-elim (a. k a) u

qFactorCls : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (H : 𝕌)
  (k : G → H)
  (c : (a a' : G) → cosetRel g N a a' → k a ≡ k a')
  (a : G)
  → qFactor _ _ _ k c (class a) ≡ k a
  using (QGroup.unfold, qFactor.eq)
qFactorCls = λG g N H k c a. ⋆

-- UNIQUENESS: qFactor is the ONLY map agreeing with k on classes.
-- Stated as an η-rule, exactly as Core.bracket.brEta is: any phi out of
-- the quotient is recovered from its own restriction along the class
-- map.
qFactorEta : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (H : 𝕌)
  (phi : QGroup _ g N → H)
  (c : (a a' : G) → cosetRel g N a a' → phi (class a) ≡ phi (class a'))
  (u : QGroup _ g N)
  → qFactor _ _ _ (λa. phi (class a)) c u ≡ phi u
  using (QGroup.unfold, qFactor.eq)
qFactorEta = λG g N H phi c u. quot-elim (a. ⋆) u

-- and the form uniqueness is usually wanted in: two maps out of G/N
-- that agree on every class are equal
qFactorUnique : (G : 𝕌)
  (g : IsGroup G)
  (N : G → Ω)
  (H : 𝕌)
  (phi psi : QGroup _ g N → H)
  → ((a : G) → phi (class a) ≡ psi (class a)) → (u : QGroup _ g N) → phi u ≡ psi u
  using (QGroup.unfold)
qFactorUnique = λG g N H phi psi e u. quot-elim (a. e a) u