Universal property of list-based polynomials #917
Conversation
|
Don't we already have that the list polynomials are equivalent to some of the other polynomials? Then this could just be transported over? |
|
As far as I know, only the CommAlgebra.FreeCommAlgebra has the universal property. And the aim of #781 is to show that the definitions in Algebra.Polynomials are equivalent to FreeCommAlgebra. @thomas-lamiaux suggested, that it is probably easier to construct directly an equivalence of types, which I also tried, but ultimately realized I need the parts of the universal property I formalized now here anyway. |
|
I grepped for 'universal' in the algebra part of the library and didn't find a universal property for any of the definitions of polynomials (except the FreeCommAlgebra). Let me know, if you think there is one I missed. |
felixwellen
force-pushed
the
ump_list_polynomials
branch
from
688dce3
to
7ca7ca8
Compare
|
Done, but depends on #916 -> still draft |
…omials # Conflicts: # Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda
# Conflicts: # Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda # Cubical/Algebra/Polynomials/UnivariateList/Properties.agda
|
Thought this might be something for @MatthiasHu , if you agree, please assign the PR to yourself. |
|
|
||
| ListPolyCommAlgebra : CommAlgebra R ℓ | ||
| ListPolyCommAlgebra = | ||
| Iso.inv (CommAlgChar.CommAlgIso R) | ||
| (ListPoly , | ||
| constantPolynomialHom R) | ||
|
|
||
| {- Universal Property -} | ||
| module _ (A : Algebra (CommRing→Ring R) ℓ') where |
There was a problem hiding this comment.
It is a bit strange to me that we're in Algebra.CommAlgebra but actually consider not-necessarily commutative algebras...
There was a problem hiding this comment.
Yes, I feel with you ;-)
But: We are proving the universal property of an CommAlgebra, which happens to quantify over Algebras. An analogous example where this is completely okay, would be the universal property of the abelianisation of a group. There it feels completely natural, that the ump quantifies over something more general. I think the ump of the CommAlgebra of Polynomials should also naturally quantify over something more general (e.g. Algebras), the situation is just more complex.
| @@ -0,0 +1,8 @@ | |||
| {-# OPTIONS --safe #-} | |||
| module Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty where | |||
There was a problem hiding this comment.
Is there a reason why you didn't want to prove the universal property here? That would resolve the issue about having a statement about Algebras in CommAlgebras.
There was a problem hiding this comment.
I think my reasoning was, that it would be good to be consistent about where things are. So 'Polynomials' could just contain a lot of pointers to Instances of CommRings and CommAlgebras and their Properties and theorems on the relations between different implementations of polynomials. But we are actually far away from that now, so I could move the ump as well.
There was a problem hiding this comment.
Fair enough, I hadn't looked at the Polynomials/ too much but that seems to be more or less the standard, so let's try to keep it that way.
There was a problem hiding this comment.
A notable exception seems to be the UnivariateList polynomials, which have their ring structure defined in Polynomials.UniveriateList.Properties. I'll make an issue with the suggestion to move that.
|
@mzeuner : Do you think it can be merged? |
|
Yeah, I think I can live with the |
The aim of this PR, is to show that the UnivariatePolyList - polynomials have the correct universal property.
This is a missing piece, connecting all definitions of polynomials in the library (see #781).