feat(ring_theory/mv_polynomial/homogeneous): Multivariate polynomials permit a nat-grading #8913
Conversation
… eric-wieser/homogenous-direct_sum-phase-2 # Conflicts: # src/ring_theory/polynomial/homogeneous.lean
…sum_graded.algebra
…ct_sum/algebra.lean
…sum_graded.algebra
…/homogenous-direct_sum-phase-2 # Conflicts: # src/ring_theory/polynomial/homogeneous.lean
…/homogenous-direct_sum-phase-2 # Conflicts: # src/algebra/direct_sum/ring.lean
github-actions
bot
added
the
blocked-by-other-PR
…ous-direct_sum-phase-2
github-actions
bot
removed
the
merge-conflict
|
I have mixed feelings about this PR. We certainly want to show that We definitely need the externally-graded-direct-sum version of graded rings: it is the most important construction of graded rings. But I think most of the API should be developed in terms of something that comes as close as possible to a characteristic predicate. Of course we can't use an actual predicate, since there is data involved. I think @kbuzzard had some mockup for this internal approach. |
github-actions
bot
removed
the
blocked-by-other-PR
| lemma is_homogeneous_C_iff (r : R) (i : ℕ) : | ||
| is_homogeneous (C r : mv_polynomial σ R) i ↔ i = 0 ∨ r = 0 := | ||
| begin | ||
| by_cases hi : i = 0, | ||
| { simp [hi] }, | ||
| by_cases hr : r = 0, | ||
| { simp [hi, hr] }, | ||
| simp only [iff_false, hi, hr, false_or], | ||
| refine mt (λ hC, _) hi, | ||
| have : coeff 0 (C r : mv_polynomial σ R) ≠ 0 := by rwa [coeff_zero_C], | ||
| simpa [eq_comm] using hC this, | ||
| end | ||
|
|
There was a problem hiding this comment.
I didn't end up needing this lemma, but it felt vaguely worth keeping.
| /-- A version of `homogeneous_component` that maps into `homogeneous_submodule σ R n`. -/ | ||
| def homogeneous_component' [comm_semiring R] (n : ℕ) : | ||
| mv_polynomial σ R →ₗ[R] homogeneous_submodule σ R n := | ||
| let f := finsupp.restrict_dom R R {d : σ →₀ ℕ | ∑ i in d.support, d i = n} in | ||
| (submodule.of_le $ (homogeneous_submodule_eq_finsupp_supported _ _ _).symm.le).comp f |
There was a problem hiding this comment.
This is a remnant of an old approach. Can any reviewer see how to generalize it to produce the alg_hom below?
There was a problem hiding this comment.
I'm not sure I understand the question. Can you please elaborate?
There was a problem hiding this comment.
homogeneous_component' is (propositionally but probably not definitionally) the same map as to_homogeneous_components immediately below, but the latter is more bundled.
However, the latter is built up from scratch, without using any of the existing finsupp machinery. This suggests either:
- There is some existing machinery I've missed
- There's a generalization here replacing
finsuppwithadd_monoid_algebrathat produces the stronger maps.
There was a problem hiding this comment.
My approach would be to define to_homogeneous_components first and then derive homogeneous_component' from that. My general approach to defining any morphisms is that you should almost never define a morphism by defining a function and then proving map_mul etc. You should pretty much always use things like aeval. I think to_homogeneous_components can be defined with aeval. I would probably also prove a different version of aeval_monomial that used the UMP of finsupp on the rhs instead of finset.prod. It's good practice to almost always use various hom-ext lemmas to prove equality of morphisms as well. Having said all that, I do agree with Johan that it would be better to define a characteristic predicate say that mv_polynomial is a direct_sum, than to define an isomorphism with a direct_sum, although you could of course use the isomorphism to define the direct_sum structure on polynomials.
|
I'm just looking at it now. I'll make a PR. The big question I had about all this was whether it all needed doing for monoids or whether we could skip straight to semirings |
…ous-direct_sum-phase-2
This reverts commit 669e1a7.
…ous-direct_sum-phase-2
| alg_equiv.of_alg_hom _ _ to_of_homogeneous_components of_to_homogeneous_components | ||
|
|
||
| lemma homogeneous_components_is_internal [comm_semiring R] : | ||
| direct_sum.submodule_is_internal (homogeneous_submodule σ R) := |
There was a problem hiding this comment.
Minor comment: would it be helpful to make the ambient ring explicit? I think this can be a lot more recognizable if it would be written as
| direct_sum.submodule_is_internal (homogeneous_submodule σ R) := | |
| is_graded_algebra (mv_polynomial σ R) (homogeneous_submodule σ R) := |
Same definitions, different names and binders.
There was a problem hiding this comment.
There are two separate things we might want to say about a "decomposition" of a module:
- The decomposition is actually faithful (this is
direct_sum.submodule_is_internal, which we state here) - It preserves multiplication and one in a graded manner (this is
set_like.graded_monoid, which we state much further up)
The first is true and the second is not in the case where we decompose a module into the submodules corresponding to elements of a basis (with submodules equal to to_span_singleton.range or similar).
The second is true and the first is not when the submodules are all just top. Maybe that's not so interesting.
We could add something like
abbreviation is_graded_algebra (A) [set_like.graded_monoid A] := direct_sum.submodule_is_internalThere was a problem hiding this comment.
Aah of course, thanks for clarifying.
There was a problem hiding this comment.
Thanks to some discussion with @jjaassoonn, we now have graded_algebra as a data-carrying typeclass. I've updated this PR to use it, but I'm not sure that's enough to make this merge-ready.
…ous-direct_sum-phase-2
|
This PR/issue depends on: |
jcommelin
added
the
awaiting-author
leanprover-community-bot-assistant
added
the
merge-conflict
…ous-direct_sum-phase-2
leanprover-community-bot-assistant
removed
the
merge-conflict
semorrison
added
the
too-late
This duplicates some of the existing API, and likely could be golfed by merging strategies between the two.
This should be compared with the newer #10119.
homogeneous#8914only the changes in
homogeneous.leanare part of this PR