Skip to content

feat: add multivariate polynomial modules#13573

Open
Shamrock-Frost wants to merge 6 commits intomasterfrom
MvPolynomialModule
Open

feat: add multivariate polynomial modules#13573
Shamrock-Frost wants to merge 6 commits intomasterfrom
MvPolynomialModule

Conversation

@Shamrock-Frost
Copy link
Copy Markdown
Contributor

@Shamrock-Frost Shamrock-Frost commented Jun 6, 2024

Add a type synonym for multivariate polynomials with coefficients in a module.

Multivariate polynomials with module coefficients are sort of silly, but they sometimes show up in commutative algebra (eg in the definition of a quasi regular sequence). Writing this code involved a lot of copy and pasting from PolynomialModule and MvPolynomial. The API is definitely lacking at this stage but it's a start.

Open in Gitpod

@Shamrock-Frost Shamrock-Frost added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jun 6, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 7, 2024

I don't think MvAEVal should live in the same file as MvPolynomialModule, and 600+ lines are a bit too long both for a PR and a file that will grow.

@Shamrock-Frost
Copy link
Copy Markdown
Contributor Author

Shamrock-Frost commented Jun 7, 2024

That makes sense. Should AEval be split out of Mathlib/Algebra/Polynomial/Module /Basic.lean first?

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 7, 2024

It isn't a prerequisite, but feel free to do it separately. I agree that it's a good idea.

@Shamrock-Frost Shamrock-Frost mentioned this pull request Jun 7, 2024
Closed
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024 •
edited
Loading

PR summary

Import changes

No significant changes to the import graph

Diff of declarations

+ C
+ C_smul
+ MvAEval
+ MvAEval'.auxRing
+ MvAEval.instAddCommGroup
+ MvPolynomialModule
+ X_pow_smul_C_eq_monomial
+ X_smul_C_eq_monomial
+ _root_.LinearMap.ofMvAEval
+ annihilator_eq_ker_aeval
+ annihilator_top_eq_ker_aeval
+ as_sum
+ coeff
+ coeff_C
+ coeff_monomial
+ coeff_monomial_smul
+ coeff_smul
+ coeff_smul_monomial
+ coeff_zero_C
+ comapSubmodule
+ comapSubmodule_le_comap
+ comapSubmodule_mapSubmodule
+ comp
+ comp_eval
+ comp_monomial
+ comp_smul
+ equivPolynomial
+ equivPolynomialSelf
+ eval
+ eval_C
+ eval_apply'
+ eval_map
+ eval_map'
+ eval_monomial
+ eval_smul
+ ext
+ ext_iff
+ in
+ induction_linear
+ injective_comapSubmodule
+ instAddCommMonoid
+ instFiniteOrig
+ instFinitePolynomial
+ instIsScalarTowerOrigPolynomial
+ instModuleOrig
+ instModulePolynomial
+ instance (R M : Type*) [CommSemiring R] [AddCommGroup M] [Module R M] :
+ instance (σ R M : Type*) [CommSemiring R] [AddCommGroup M] [Module R M] :
+ instance : AddCommMonoid (MvPolynomialModule σ R M)
+ instance : AddCommMonoid (PolynomialModule R M)
+ instance : CommSemiring (MvAEval'.auxRing Φ h)
+ instance : Inhabited (MvPolynomialModule σ R M)
+ instance : Module S (MvPolynomialModule σ R M)
+ map
+ mapSubmodule
+ mapSubmodule_comapSubmodule
+ map_monomial
+ map_smul
+ may
+ mem_comapSubmodule
+ mem_mapSubmodule
+ mem_support_iff
+ monomial
+ monomial_eq
+ monomial_eq_zero
+ monomial_single_add
+ monomial_smul_C
+ monomial_smul_monomial
+ monomial_zero
+ monomial_zero'
+ of
+ of_aeval_smul
+ of_symm_smul
+ polynomialModule
+ prod_X_pow_smul_eq_monomial
+ range_comapSubmodule
+ span_C_over_poly_eq_span_monomials_over_base
+ support
+ support_add
+ support_monomial
+ support_monomial_subset
+ support_sum
+ support_sum_monomial_coeff
+ support_zero
+ top_eq_span_base_monomials
++ X_smul_of
++ instance (M : Type u) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower S R M] :
++ of_symm_X_smul
- instance (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S R M] :
- instance : AddCommGroup (PolynomialModule R M)
-++ isScalarTower'

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@Shamrock-Frost Shamrock-Frost force-pushed the MvPolynomialModule branch 3 times, most recently from 6760b49 to a9df059 Compare June 7, 2024 19:00
erdOne
erdOne reviewed Jul 16, 2024
View reviewed changes
Mathlib/Algebra/MvPolynomial/Module/Basic.lean

namespace MvPolynomialModule

@[semireducible]
Copy link
Copy Markdown
Member

@erdOne erdOne Jul 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this semireducible?

erdOne
erdOne reviewed Jul 16, 2024
View reviewed changes
Mathlib/Algebra/MvPolynomial/Module/Basic.lean

variable {R}

theorem induction_linear {P : MvPolynomialModule σ R M → Prop}
Copy link
Copy Markdown
Member

@erdOne erdOne Jul 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
theorem induction_linear {P : MvPolynomialModule σ R M → Prop}
@[elab_as_elim]
theorem induction_linear {P : MvPolynomialModule σ R M → Prop}

erdOne
erdOne reviewed Jul 16, 2024
View reviewed changes
Mathlib/Algebra/MvPolynomial/Module/Basic.lean
variable (σ R)

open Submodule in
lemma span_C_over_poly_eq_span_monomials_over_base (s : Set M) :
Copy link
Copy Markdown
Member

@erdOne erdOne Jul 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the naming convention suggests restrictScalars_span_mvPolynomial_image_C instead.

erdOne
erdOne reviewed Jul 16, 2024
View reviewed changes
Mathlib/Algebra/MvPolynomial/Module/Basic.lean

variable (M)

lemma top_eq_span_base_monomials :
Copy link
Copy Markdown
Member

@erdOne erdOne Jul 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly this is maybe iSup_range_monomial_eq_top, and the direction of the lemma should be reversed.

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jul 16, 2024

Again, as indicated before, this PR is too big and has multiple goals. If you can split out Mathlib/Algebra/MvPolynomial/Module/Basic.lean into a separate PR, I'll happily maintainer merge the rest.

@erdOne erdOne added awaiting-author A reviewer has asked the author a question or requested changes. and removed t-algebra Algebra (groups, rings, fields, etc) labels Jul 16, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2024
@grunweg grunweg added the t-algebra Algebra (groups, rings, fields, etc) label Aug 15, 2024
@grunweg grunweg changed the title Feat: Add multivariate polynomial module feat: add multivariate polynomial modules Aug 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Shamrock-Frost @erdOne @kim-em @grunweg