Modular arithmetic in terms of ideals #2729
Conversation
|
Would you want some help to get this further along? |
|
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 |
|
Ok, once my students make further progress on the ones they are currently working on, I'll get them to look at this. |
|
Some errors thrown up by checking with
|
|
@jamesmckinna I've merged in master, are those two errors fixed now? |
| infix 0 _by_ | ||
|
|
||
| data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where | ||
| _by_ : ∀ g → x // y ≈ ι g → x ≋ y |
There was a problem hiding this comment.
Similarly to the type of NormalSubgroup.normal, is it 'easier' to write
| _by_ : ∀ g → x // y ≈ ι g → x ≋ y | |
| _by_ : ∀ g → x ≈ ι g ∙ y → x ≋ y |
???
There was a problem hiding this comment.
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 QuasigroupMonoid (an associative Loop is a group)? (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...?
There was a problem hiding this comment.
It's a shame that the iota means I can't reuse the divisibility machinery...
There was a problem hiding this comment.
Yes, and I'm not sure we're quite ready to embrace the least common generalisation of the two... but one day perhaps!?
There was a problem hiding this comment.
Code duplication with divisibility shouldn't be a blocker - I think your suggestion is a good one and I'll modify the code accordingly.
There was a problem hiding this comment.
If there is a rationale for that class of decisions I'd love to learn it
There was a problem hiding this comment.
Hmmm... let's see if I can at least rationalise it post hoc, although given the number of people who make/have made such suggestions to me at AIM, perhaps there are real reasons:
pro
- 'eta for free' so no (real) overhead to pattern matching on the record (debatable?); but maybe this is also a 'contra'?
- projections/copatterns are 'better' (are they?) if you don't need access to all the substructure of a given expression (is this correct?)
- informal subtyping via the signature of the associated
module
contra
- the main one I see is having, in this example, to give
na name as afield, whereas in thedataversion, it's 'just an argument in a telescope' defining a function, so 'less' namespace pollution (but that can be controlled by how much you exposefieldnames byopening
Er... that's all I've got? Anyone else care to offer a suggestion?
There was a problem hiding this comment.
There are also differences in how goals are displayed, Agda's ability to infer things, and how much evaluation happens, at least between direct / one-field-record / one-item-data.
There was a problem hiding this comment.
Well, there is also the problem/issue: records can't be used if you have a GADT-/inductive-family-style definition, or rather they can, at the cost of a suitable additional field defining the 'equation' (usually in terms of _≡_) which holds between the (arbitrary) parameters to the record, and the (possibly) green slime occurring in the conclusion of the constructor.
What's interesting about these definitions is that the equations defining the concepts in the data versions are the specialisations of such 'green slime', but to the underlying Setoid equality, rather than _≡_... so would be some more work to do to ensure that any inductive family-style definition enjoyed suitable closure/'respects' properties wrt that equality, on the model of subst ... so it might end up being more painful in the end? UPDATED: or indeed, impossible. How do we show that the _by_ decomposition is unique? If we can't, then an inductive family version isn't going to fly, I think :-(
We're not especially good in stdlib at doing 'Red team'/'Blue team' adversarial design in order to determine which choice is better, but I wonder sometimes (if we had a larger developer pool!) if it might be worthwhile? And indeed, if my reviewing style is evolving in such a direction... ;-)
There was a problem hiding this comment.
Agreed: I'd say we're still figuring out how to do modeling in dependent type theory (i.e. the whole community, not just stdlib developers).
|
Have suggested some possible refactorings to make the constructions/lemmas more reusable, and to be able to reuse |
|
So for the 'ALT' version of 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 |
|
... and for 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 Also: |
| N-isGroup : IsGroup N._≈_ N._∙_ N.ε N._⁻¹ | ||
| N-isGroup = GM.isGroup ι-monomorphism isGroup |
There was a problem hiding this comment.
Should there also be a Group defined?
| 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?
|
And for ≋-*-cong : Congruent₂ _*_
≋-*-cong {x} {y} {u} {v} (j by x≈ιj+y) (k by u≈ιk+v) = j I.*ᵣ u I.+ᴹ y I.*ₗ k by begin
x * u ≈⟨ *-congʳ x≈ιj+y ⟩
(ι j + y) * u ≈⟨ distribʳ _ _ _ ⟩
ι j * u + y * u ≈⟨ +-congˡ (*-congˡ u≈ιk+v) ⟩
ι j * u + y * (ι k + v) ≈⟨ +-congˡ (distribˡ _ _ _) ⟩
ι j * u + (y * ι k + y * v) ≈⟨ +-assoc _ _ _ ⟨
(ι j * u + y * ι k) + y * v ≈⟨ +-congʳ (+-cong (ι.*ᵣ-homo u j) (ι.*ₗ-homo y k)) ⟨
ι (j I.*ᵣ u) + ι (y I.*ₗ k) + y * v ≈⟨ +-congʳ (ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k)) ⟨
ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k) + y * v ∎ |
|
Suggested refactoring for
|
| ; 0# = 0# | ||
| ; 1# = 1# | ||
| } | ||
|
|
There was a problem hiding this comment.
Should insert here that the quotient map on the underlying additive subgroup of the module in fact extends to a ring homomorphism from R to R / I...
... which given that the underlying map is id is pretty easy by hand.
|
I think (while travelling) this should be generalized to ideals over modules, rather than just rings. This shouldn't need much change to the code. |
I had the chance to give this a go, and ran into an obstacle. For |
|
Not sure you need the generalisations at this stage? |
| _≋?_ with ℕ.nonZero? ∣ m ∣ | ||
| ... | yes p = _≋?′_ {{p}} | ||
| ... | no ¬p = {!!} |
There was a problem hiding this comment.
... with the modified definition of _≋_:
| _≋?_ with ℕ.nonZero? ∣ m ∣ | |
| ... | yes p = _≋?′_ {{p}} | |
| ... | no ¬p = {!!} | |
| _≋?_ : Decidable _≋_ | |
| _≋?_ with ∣ m ∣ ℕ.≟ 0 | |
| ... | yes |m|≡0 = λ x y → map′ ≡⇒≋ ≋⇒≡ (x ≟ y) | |
| where | |
| open ≡-Reasoning | |
| ≡⇒≋ : _≡_ ⇒ _≋_ | |
| ≡⇒≋ {x = x} {y = y} x≡y = +0 by begin | |
| x ≡⟨ x≡y ⟩ | |
| y ≡⟨ +-identityˡ y ⟨ | |
| +0 + y ≡⟨⟩ | |
| +0 * +0 + y ∎ | |
| ≋⇒≡ : _≋_ ⇒ _≡_ | |
| ≋⇒≡ {x = x} {y = y} (k by x≡k0+y) = begin | |
| x ≡⟨ x≡k0+y ⟩ | |
| k * m + y ≡⟨ ≡.cong (λ m → k * m + y) (∣i∣≡0⇒i≡0 |m|≡0) ⟩ | |
| k * +0 + y ≡⟨ ≡.cong (_+ y) (*-comm k +0) ⟩ | |
| +0 * k + y ≡⟨ +-identityˡ y ⟩ | |
| y ∎ | |
| ... | no m≢0 = _≋?′_ {{ℕ.≢-nonZero m≢0}} |
There was a problem hiding this comment.
... where the argument for the case m≡0 could/should be generalised for arbitrary Ring, with the machinery (∣i∣≡0⇒i≡0 |m|≡0) being all that's then needed to aplly it for the Integer case...
| to-% {x} {y} (k by x-y≡km) = {!!} | ||
| where | ||
| open ≡-Reasoning | ||
| lemma : x % m ⊖ y % m ≡ (k - (x / m) + (y / m)) * m | ||
| lemma = begin | ||
| x % m ⊖ y % m ≡⟨ m-n≡m⊖n (x % m) (y % m) ⟨ | ||
| + (x % m) - + (y % m) ≡⟨ {!!} ⟩ | ||
| (k - (x / m) + (y / m)) * m ∎ | ||
|
|
||
| bound : ∣ x % m ⊖ y % m ∣ ℕ.< ∣ m ∣ | ||
| bound = {!!} |
There was a problem hiding this comment.
| to-% {x} {y} (k by x-y≡km) = {!!} | |
| where | |
| open ≡-Reasoning | |
| lemma : x % m ⊖ y % m ≡ (k - (x / m) + (y / m)) * m | |
| lemma = begin | |
| x % m ⊖ y % m ≡⟨ m-n≡m⊖n (x % m) (y % m) ⟨ | |
| + (x % m) - + (y % m) ≡⟨ {!!} ⟩ | |
| (k - (x / m) + (y / m)) * m ∎ | |
| bound : ∣ x % m ⊖ y % m ∣ ℕ.< ∣ m ∣ | |
| bound = {!!} | |
| to-% {x} {y} x≋y | |
| using x%m ← x % m | |
| using y%m ← y % m | |
| with k by x%m≡km+y%m ← (let open ≈-Reasoning ℤ/mℤ.setoid in begin | |
| + x%m ≈⟨ z≋z%m x ⟨ | |
| x ≈⟨ x≋y ⟩ | |
| y ≈⟨ z≋z%m y ⟩ | |
| + y%m ∎) | |
| = begin | |
| x%m ≡⟨ ℕ.m<n⇒m%n≡m (n%d<d x m) ⟨ | |
| x%m ℕ.% ∣ m ∣ ≡⟨⟩ | |
| (+ x%m) % m ≡⟨ ≡.cong (_% m) x%m≡km+y%m ⟩ | |
| (k * m + (+ y%m)) % m ≡⟨ [km+n]%m≡n%m k (+ y%m) ⟩ | |
| (+ y%m) % m ≡⟨⟩ | |
| y%m ℕ.% ∣ m ∣ ≡⟨ ℕ.m<n⇒m%n≡m (n%d<d y m) ⟩ | |
| y%m ∎ | |
| where | |
| open ≡-Reasoning | |
| [km+n]%m≡n%m : ∀ k n → (k * m + n) % m ≡ n % m | |
| [km+n]%m≡n%m k n = {!!} |
where this last lemma is the 'obvious' extension of Data.Nat.DivMod.[m+kn]%n≡m%n to Integer... but is still ... irritating to have to prove directly from first principles.
There was a problem hiding this comment.
I'd hoped I could simplify this further, but ran out of energy! Hopefully your holiday has re-energised you!
|
Yet another alternative definition of data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) wherenamely, to symmetrise wrt multiplication by elements of the normal subgroup, ie record _≋_ (x y : G.Carrier) : Set (c ⊔ ℓ ⊔ c′) where
field
{l} {r} : _
[ιl]x≈[ιr]y : ι l ∙ x G.≈ ι r ∙ yon the basis that this mirrors the revised ('symmetrised') definition of Transitivity is a bit harder to prove, but I wonder if this might overall enjoy a smoother development? Or else refactor as a lemma/view expressing the decomposition? |
This was one of Nagata's original motivation (see 'Local Rings' for details) for introducing the 'ring of dual numbers' construction now in
|
Taneb
force-pushed
the
modular-arithmetic
branch
from
5d31747 to
9f7db10
Compare
|
I've |
3 participants
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
Closes #2076