[draft] Polynomial #2821
[draft] Polynomial #2821
Conversation
|
Zeroth thoughts:
First thoughts:
Second thought:
Third thought:
Fourth thoughts:
|
| x≈ε⇒x⁻¹≈ε {x} x≈ε = begin | ||
| x ⁻¹ ≈⟨ ⁻¹-cong x≈ε ⟩ | ||
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | ||
| ε ∎ |
There was a problem hiding this comment.
I wasn't sure if
- this lemma met the Fairbairn threshhold (moreover, it's used only once in this PR)
- this proof was the most 'efficient', compared to
x≈ε⇒x⁻¹≈ε = identityˡ-unique _ _ ∘ trans (inverseˡ _) ∘ sym
which uses only a Loop property beyond the basic IsGroup axiomatisation.
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | ||
| x ≈⟨ ⁻¹-involutive x ⟨ | ||
| x ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈ε ⟩ | ||
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | ||
| ε ∎ |
There was a problem hiding this comment.
Ditto, only more so:
x⁻¹≈ε⇒x≈ε = identityʳ-unique _ _ ∘ trans (inverseˡ _) ∘ symThere was a problem hiding this comment.
Alternatively, you could bootstrap
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | |
| x ≈⟨ ⁻¹-involutive x ⟨ | |
| x ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈ε ⟩ | |
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | |
| ε ∎ | |
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | |
| x ≈⟨ ⁻¹-involutive x ⟨ | |
| x ⁻¹ ⁻¹ ≈⟨ x≈ε⇒x⁻¹≈ε x⁻¹≈ε ⟩ | |
| ε ∎ |
which is 'just'
x⁻¹≈ε⇒x≈ε = trans (sym (¹-involutive _)) ∘ x≈ε⇒x⁻¹≈ε|
I've been working on a slightly different implementation of this. Let me find what I've done and compare - notably, I used lists rather than vectors, and didn't have a notion of degree |
I think you need commutativity of multiplication to show that polynomial evaluation preserves multiplication |
| data _≈_ : (Poly m) → (Poly n) → Set (ℓ₁ L.⊔ ℓ₂) where | ||
| []≈ : (q : Poly n) → IsZero q → [] ≈ q | ||
| ≈[] : (p : Poly m) → IsZero p → p ≈ [] | ||
| cons : (a ≈A b) → (p ≈ q) → (a ∷ p) ≈ (b ∷ q) |
There was a problem hiding this comment.
This particular definition has two separate proofs that [] is equal to []... not necessarily the end of the world, but it bothers me
Hmmm. https://math.stackexchange.com/questions/806119/do-polynomials-make-sense-over-non-commutative-rings Otherwise could we even speak about polynomials over rings such as square matrices (for the Cayley-Hamilton theorem, for example, even if that's usually only considered for matrices over commutative rings, such matrices don't enjoy commutative multiplication... while for any polynomial and its values, it is the case that powers of an element do commute...)? I think the real issue is making sure that multiplication is defined correctly... see also https://en.wikipedia.org/wiki/Monoid_ring |
|
Non-commutative polynomial rings certainly do make sense and are useful. See for examples the skew polynomials that arise when modeling various kinds of operators. Axiom does allow polynomials over coefficients rings like square matrices. |
|
For reference, here's my implementation of polynomials: https://gist.github.com/Taneb/3257f47436ec6b11de403d839d7c413b |
|
Thank you for the detailed feedback and the comments and I apologize for the delayed response. Although it will take some time, I will try implement the changes using the semiring instead of the commutative ring and eventually prove the universal property of polynomial rings. Since this is only a draft which I should have made it clear, any further comments or suggestions are welcome. |
This draft pull request introduces a new way to represent a polynomial over commutative ring -- as a vector over the commutative ring -- and a proof that polynomials themselves make up a commutative ring.