Modular arithmetic in terms of ideals #2729

Taneb · 2025-06-07T16:02:07Z

Opening this PR to share my WIP. I've got a messy proof of the Chinese remainder theorem for arbitrary rings, but in porting it from my standalone library to this I've somehow made some parameters not infer properly

JacquesCarette

The new Kernel file looks nice.

JacquesCarette · 2025-07-30T20:56:03Z

Would you want some help to get this further along?

Taneb · 2025-07-30T21:46:34Z

Yes, actually. I've been working on a module for the special case of ideals of the ring of integers, and I've been struggling to prove that (for a non-zero modulus) it's finite, which I think it important for the "yes this is modular arithmetic as you know it" feel. I'll post a WIP commit shortly

JacquesCarette · 2025-08-01T20:03:14Z

Ok, once my students make further progress on the ones they are currently working on, I'll get them to look at this.

jamesmckinna · 2025-08-02T14:07:45Z

And, ... having murdered my darlings #2257 #2292 I should turn my attention to helping with this!

src/Data/Integer/ModularArithmetic.agda

jamesmckinna · 2025-08-03T10:57:13Z

Some errors thrown up by checking with agda-v2.8.0 (beyond the failing tests above):

Data.Fin.Properties on this branch still has the now-erroneous --warn=noUserWarning which should be fixed after a rebase/merge with the current master?
Data.Integer.Properties now triggers a warning about a null rewrite step on L1417 (which I hadn't seen caught anywhere else? but the offending line doesn't appear any more on master, so...)

Taneb · 2025-08-03T21:03:51Z

@jamesmckinna I've merged in master, are those two errors fixed now?

jamesmckinna · 2025-08-04T11:40:39Z

src/Algebra/NormalSubgroup.agda

+    ι : RawGroup.Carrier N → Carrier
+    ι-monomorphism : IsGroupMonomorphism N rawGroup ι
+    -- every element of N commutes in G
+    normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′


So... I was a bit surprised that this was an 'easier' formulation than

Suggested change

normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′

normal : ∀ n g → ∃[ n′ ] g ∙ ι n ≈ ι n′ ∙ g

which I wondered as to whether

it would be easier/smoother to show gives rise to an equivalence relation on the quotient

it would generalise (better) to Loop, Quasigroup or even Magma/Semigroup?

Cf. comments elsewhere from @JacquesCarette about defining 'ideal' via 'sink'...

jamesmckinna · 2025-08-04T11:43:42Z

src/Algebra/Ideal/Construct/Principal.agda

+          x * r * a   ≈⟨ *-assoc x r a ⟩
+          x * (r * a) ≈⟨ *-congˡ (*-comm r a) ⟩
+          x * (a * r) ≈⟨ *-assoc x a r ⟨
+          x * a * r   ∎


This kind of argument occurs in Algebra.Properties.CommutativeSemigroup, and might usefully be re-used here?

jamesmckinna · 2025-08-04T11:44:08Z

src/Algebra/Ideal/Construct/Principal.agda

+          x * a * r   ∎
+        }
+      }
+    ; injective = λ p → p


Suggested change

; injective = λ p → p

; injective = id

???

jamesmckinna · 2025-08-04T11:51:04Z

src/Algebra/Construct/Quotient/Group.agda

+infix 0 _by_
+
+data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+  _by_ : ∀ g → x // y ≈ ι g → x ≋ y


Similarly to the type of NormalSubgroup.normal, is it 'easier' to write

Suggested change

_by_ : ∀ g → x // y ≈ ι g → x ≋ y

_by_ : ∀ g → x ≈ ι g ∙ y → x ≋ y

???

Yielding:

≋-refl : Reflexive _≋_ ≋-refl {x} = N.ε by begin x ≈⟨ identityˡ _ ⟨ ε ∙ x ≈⟨ ∙-congʳ (ι.ε-homo) ⟨ ι N.ε ∙ x ∎ ≋-sym : Symmetric _≋_ ≋-sym {x} {y} (g by x≈ιg∙y) = g N.⁻¹ by begin y ≈⟨ y≈x\\z _ _ _ (sym x≈ιg∙y) ⟩ ι g ⁻¹ ∙ x ≈⟨ ∙-congʳ (ι.⁻¹-homo g) ⟨ ι (g N.⁻¹) ∙ x ∎ ≋-trans : Transitive _≋_ ≋-trans {x} {y} {z} (g by x≈ιg∙y) (h by y≈ιh∙z) = g N.∙ h by begin x ≈⟨ x≈ιg∙y ⟩ ι g ∙ y ≈⟨ ∙-congˡ y≈ιh∙z ⟩ ι g ∙ (ι h ∙ z) ≈⟨ assoc _ _ _ ⟨ ι g ∙ ι h ∙ z ≈⟨ ∙-congʳ (ι.∙-homo g h) ⟨ ι (g N.∙ h) ∙ z ∎

and thus being admissible in any Quasigroup? (Well, refl and trans at least...)

Indeed, these are properties (modulo ι) of the abstract Divisibility relations on Magma and their properties... as structure is successively enriched to Semigroup (for trans) and Monoid (for refl)! So we should add Group divisibility to inherit those, with sym becoming provable...?

jamesmckinna · 2025-08-04T11:52:43Z

src/Algebra/Construct/Quotient/Group.agda

+  x // z              ≈⟨ ∙-congʳ (identityʳ x) ⟨
+  x ∙ ε // z          ≈⟨ ∙-congʳ (∙-congˡ (inverseˡ y)) ⟨
+  x ∙ (y \\ y) // z   ≈⟨ ∙-congʳ (assoc x (y ⁻¹) y) ⟨
+  (x // y) ∙ y // z   ≈⟨ assoc (x // y) y (z ⁻¹) ⟩
+  (x // y) ∙ (y // z) ≈⟨ ∙-cong x//y≈ιg y//z≈ιh ⟩


Already covered (in part) by Algebra.Properties.Monoid...? And if not, could/should be added?
Or: see above!

jamesmckinna · 2025-08-04T11:59:44Z

src/Data/Integer/ModularArithmetic.agda

+module _ .{{_ : NonZero m}} where
+
+  from-% : ∀ {x y} → x % m ≡ y % m → x ≋ y
+  from-% {x} {y} x%m≡y%m = x / m - y / m by begin


How much of this argument recapitulates concretely reasoning steps already used abstractly in CRT?

jamesmckinna · 2025-08-04T12:43:04Z

src/Algebra/Construct/Quotient/Group.agda

+≈⇒≋ {x} {y} x≈y = N.ε by begin
+  x // y ≈⟨ x≈y⇒x∙y⁻¹≈ε x≈y ⟩
+  ε      ≈⟨ ι.ε-homo ⟨
+  ι N.ε  ∎


Similarly

≈⇒≋ {x} {y} x≈y = N.ε by begin x ≈⟨ x≈y ⟩ y ≈⟨ identityˡ _ ⟨ ε ∙ y ≈⟨ ∙-congʳ (ι.ε-homo) ⟨ ι N.ε ∙ y ∎

jamesmckinna · 2025-08-04T12:48:56Z

Have suggested some possible refactorings to make the constructions/lemmas more reusable, and to be able to reuse Divisibility for abstract algebra...

jamesmckinna · 2025-08-04T15:44:47Z

So for the 'ALT' version of NormalSubgroup, I ended up with:

open import Algebra.Bundles using (Group; RawGroup)

module Algebra.NormalSubgroupALT {c ℓ} (G : Group c ℓ)  where

open import Algebra.Structures using (IsGroup)
open import Algebra.Morphism.Structures
import Algebra.Morphism.GroupMonomorphism as GM
open import Data.Product.Base
open import Level using (suc; _⊔_)

private
  module G = Group G
  open G using (_≈_; _∙_)


record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
-- firstly: N is a subgroup of G
  field
    N : RawGroup c′ ℓ′

  module N = RawGroup N

  field
    ι : N.Carrier → G.Carrier
    ι-monomorphism : IsGroupMonomorphism N G.rawGroup ι

  module ι = IsGroupMonomorphism ι-monomorphism

  isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹
  isGroup = GM.isGroup ι-monomorphism G.isGroup

  group : Group _ _
  group = record { isGroup = isGroup }

-- secondly: every element of N commutes in G
  field
    normal : ∀ n g → ∃[ n′ ] g ∙ ι n ≈ ι n′ ∙ g

jamesmckinna · 2025-08-04T15:46:18Z

... and for Algebra.Construct.Quotient.Group I obtained

open import Algebra.Bundles using (Group; RawGroup)
open import Algebra.NormalSubgroupALT using (NormalSubgroup)

module Algebra.Construct.Quotient.GroupALT
  {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where

open import Algebra.Morphism.Structures
open import Algebra.Structures using (IsGroup)
open import Data.Product.Base
open import Level using (_⊔_)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Structures using (IsEquivalence)

import Algebra.Definitions as AlgDefs
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

open import Algebra.Properties.Group G

private
  module G = Group G
  open G using (_≈_; _∙_; ε;  _⁻¹)
  open import Algebra.Properties.Monoid G.monoid
  module N = NormalSubgroup N
  open N using (ι; normal; module N)
  open ≈-Reasoning G.setoid

infix 0 _by_

data _≋_ (x y : G.Carrier) : Set (c ⊔ ℓ ⊔ c′) where
  _by_ : ∀ n → x ≈ ι n ∙ y → x ≋ y

quotientRawGroup : RawGroup _ _
quotientRawGroup = record { _≈_ = _≋_ ; _∙_ = _∙_ ; ε = ε ; _⁻¹ = _⁻¹ }

≈⇒≋ : _≈_ ⇒ _≋_
≈⇒≋ {x} {y} x≈y = N.ε by begin
  x         ≈⟨ x≈y ⟩
  y         ≈⟨ G.identityˡ _ ⟨
  ε ∙ y     ≈⟨ G.∙-congʳ (ι.ε-homo) ⟨
  ι N.ε ∙ y ∎

≋-refl : Reflexive _≋_
≋-refl {x} = ≈⇒≋ G.refl

≋-sym : Symmetric _≋_
≋-sym {x} {y} (g by x≈ιg∙y) = g N.⁻¹ by begin
  y              ≈⟨ y≈x\\z _ _ _ (G.sym x≈ιg∙y) ⟩
  ι g ⁻¹ ∙ x     ≈⟨ G.∙-congʳ (ι.⁻¹-homo g) ⟨
  ι (g N.⁻¹) ∙ x ∎

≋-trans : Transitive _≋_
≋-trans {x} {y} {z} (g by x≈ιg∙y) (h by y≈ιh∙z) = g N.∙ h by begin
  x               ≈⟨ x≈ιg∙y ⟩
  ι g ∙ y         ≈⟨ G.∙-congˡ y≈ιh∙z ⟩
  ι g ∙ (ι h ∙ z) ≈⟨ G.assoc _ _ _ ⟨
  ι g ∙ ι h ∙ z   ≈⟨ G.∙-congʳ (ι.∙-homo g h) ⟨
  ι (g N.∙ h) ∙ z ∎

≋-isEquivalence : IsEquivalence _≋_
≋-isEquivalence = record
  { refl = ≋-refl
  ; sym = ≋-sym
  ; trans = ≋-trans
  }

open AlgDefs _≋_

≋-∙-cong : Congruent₂ _∙_
≋-∙-cong {x} {y} {u} {v} (g by x≈ιg∙y) (h by u≈ιh∙v) =
  let k , y∙ιh≈ιk∙y = normal h y in g N.∙ k by begin
  x ∙ u                 ≈⟨ G.∙-cong x≈ιg∙y u≈ιh∙v ⟩
  (ι g ∙ y) ∙ (ι h ∙ v) ≈⟨ uv≈w⇒xu∙vy≈x∙wy y∙ιh≈ιk∙y _ _ ⟩
  ι g ∙ ((ι k ∙ y) ∙ v) ≈⟨ G.assoc _ _ _ ⟨
  ι g ∙ (ι k ∙ y) ∙ v   ≈⟨ G.∙-congʳ (G.assoc _ _ _) ⟨
  ι g ∙ ι k ∙ y ∙ v     ≈⟨ G.assoc _ _ _ ⟩
  (ι g ∙ ι k) ∙ (y ∙ v) ≈⟨ G.∙-congʳ (ι.∙-homo g k) ⟨
  ι (g N.∙ k) ∙ (y ∙ v) ∎

≋-⁻¹-cong : Congruent₁ _⁻¹
≋-⁻¹-cong {x} {y} (g by x≈ιg∙y) =
  let h , y⁻¹∙ιg⁻¹≈ιh∙y⁻¹ = normal (g N.⁻¹) (y ⁻¹)
  in h by begin
  x ⁻¹              ≈⟨ G.⁻¹-cong x≈ιg∙y ⟩
  (ι g ∙ y) ⁻¹      ≈⟨ ⁻¹-anti-homo-∙ _ _ ⟩
  y ⁻¹ ∙ ι g ⁻¹     ≈⟨ G.∙-congˡ (ι.⁻¹-homo _) ⟨
  y ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ y⁻¹∙ιg⁻¹≈ιh∙y⁻¹ ⟩
  ι h ∙ y ⁻¹        ∎

quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹
quotientIsGroup = record
  { isMonoid = record
    { isSemigroup = record
      { isMagma = record
        { isEquivalence = ≋-isEquivalence
        ; ∙-cong = ≋-∙-cong
        }
      ; assoc = λ x y z → ≈⇒≋ (G.assoc x y z)
      }
    ; identity = record
      { fst = λ x → ≈⇒≋ (G.identityˡ x)
      ; snd = λ x → ≈⇒≋ (G.identityʳ x)
      }
    }
  ; inverse = record
    { fst = λ x → ≈⇒≋ (G.inverseˡ x)
    ; snd = λ x → ≈⇒≋ (G.inverseʳ x)
    }
  ; ⁻¹-cong = ≋-⁻¹-cong
  }

quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
quotientGroup = record { isGroup = quotientIsGroup }

module _/_ = Group quotientGroup

η : G.Carrier → _/_.Carrier
η x = x -- because we do all the work in the relation

η-isHomomorphism : IsGroupHomomorphism G.rawGroup quotientRawGroup η
η-isHomomorphism = record
  { isMonoidHomomorphism = record
    { isMagmaHomomorphism = record
      { isRelHomomorphism = record
        { cong = ≈⇒≋
        }
      ; homo = λ _ _ → ≋-refl
      }
    ; ε-homo = ≋-refl
    }
  ; ⁻¹-homo = λ _ → ≋-refl
  }

In each case, feel free to adapt as you see fit. (I'm almost tempted to inline η = id in the definition of η-isGroupHomomorphism, for example, and dispense with a redundant definition, which might in any case be want to be called π or proj?

Also: IsGroupEpimorphism? cf. your #2037 ...

jamesmckinna · 2025-08-04T17:40:49Z

src/Algebra/NormalSubgroup.agda

+  N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹
+  N-isGroup = GM.isGroup ι-monomorphism isGroup


Should there also be a Group defined?

Suggested change

N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹

N-isGroup = GM.isGroup ι-monomorphism isGroup

N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹

N-isGroup = GM.isGroup ι-monomorphism isGroup

N-group : Group _ _

N-group = record { isGroup = N-isgroup }

plus: what should be exported publicly from this module?

Taneb added 8 commits June 7, 2025 15:19

Add notion of quotient groups

ca23f3d

Quotient rings

886bbae

Intersection of ideals

880933d

Add coprimality of ideals

c15d31d

Add missing options pragma from ring quotient module

851001d

Chinese remainder theorem

441d612

Minor fixes

b7099bd

Principal ideals

94cefa6

Taneb force-pushed the modular-arithmetic branch from 8617e07 to 94cefa6 Compare June 8, 2025 11:04

JacquesCarette reviewed Jun 26, 2025

View reviewed changes

Taneb mentioned this pull request Jul 11, 2025

[ definition ] characteristic of a Ring (etc.) #2760

Open

WIP integer special case module

7e6fc80

jamesmckinna mentioned this pull request Aug 2, 2025

Add Data.Nat.Bounded #2257

Closed

jamesmckinna reviewed Aug 3, 2025

View reviewed changes

src/Data/Integer/ModularArithmetic.agda Show resolved Hide resolved

Merge branch 'master' into modular-arithmetic

5d31747

jamesmckinna reviewed Aug 4, 2025

View reviewed changes

jamesmckinna mentioned this pull request Aug 4, 2025

Implementation of consequences and lemmas for Groups #2695

Open

jamesmckinna reviewed Aug 4, 2025

View reviewed changes

	normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′
	normal : ∀ n g → ∃[ n′ ] g ∙ ι n ≈ ι n′ ∙ g

	_by_ : ∀ g → x // y ≈ ι g → x ≋ y
	_by_ : ∀ g → x ≈ ι g ∙ y → x ≋ y

		N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹
		N-isGroup = GM.isGroup ι-monomorphism isGroup

Modular arithmetic in terms of ideals #2729

Are you sure you want to change the base?

Modular arithmetic in terms of ideals #2729

Uh oh!

Conversation

Taneb commented Jun 7, 2025

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

JacquesCarette commented Jul 30, 2025

Uh oh!

Taneb commented Jul 30, 2025

Uh oh!

JacquesCarette commented Aug 1, 2025

Uh oh!

jamesmckinna commented Aug 2, 2025

Uh oh!

Uh oh!

jamesmckinna commented Aug 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Taneb commented Aug 3, 2025

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Aug 4, 2025

Uh oh!

jamesmckinna commented Aug 4, 2025

Uh oh!

jamesmckinna commented Aug 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna Aug 4, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jamesmckinna commented Aug 3, 2025 •

edited

Loading

jamesmckinna Aug 4, 2025 •

edited

Loading

jamesmckinna Aug 4, 2025 •

edited

Loading

jamesmckinna commented Aug 4, 2025 •

edited

Loading