[Merged by Bors] - feat: the free locus of a (finitely presented) module#18691
[Merged by Bors] - feat: the free locus of a (finitely presented) module#18691
Conversation
erdOne
commented
Nov 6, 2024
PR summary f8e167d0b9Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.LocalProperties.Projective | 1209 | 1265 | +56 (+4.63%) |
| Mathlib.Algebra.Module.FinitePresentation | 1086 | 1103 | +17 (+1.57%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.RingTheory.Localization.Free Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.LocalRing.Module |
2 |
Mathlib.Algebra.Module.Presentation.Finite |
16 |
Mathlib.Algebra.Module.FinitePresentation |
17 |
Mathlib.RingTheory.LocalProperties.Projective |
56 |
Mathlib.Algebra.Module.FreeLocus (new file) |
1783 |
Declarations diff
+ FG.of_restrictScalars
+ FinitePresentation.of_isBaseChange
+ IsLocalizedModule.of_exists_mul_mem
+ IsLocalizedModule.of_linearEquiv_right
+ IsLocalizedModule.of_restrictScalars
+ Module.finrank_of_isLocalizedModule_of_free
+ Module.free_of_isLocalizedModule
+ Module.lift_rank_of_isLocalizedModule_of_free
+ basicOpen_subset_freeLocus_iff
+ comap_freeLocus_le
+ freeLocus
+ freeLocus_congr
+ freeLocus_eq_univ
+ freeLocus_eq_univ_iff
+ freeLocus_localization
+ iff_of_ringEquiv
+ instance (S : Submonoid R) [Module.FinitePresentation R M] :
+ instance {A} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] :
+ isLocallyConstant_rankAtStalk
+ isLocallyConstant_rankAtStalk_freeLocus
+ isOpen_freeLocus
+ mem_freeLocus
+ mem_freeLocus_iff_tensor
+ mem_freeLocus_of_isLocalization
+ of_ringEquiv
+ rankAtStalk
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
|
Regarding the large-import: |
…lib4 into erd1/freeLocus
…lib4 into erd1/freeLocus
b6dd4ea to
dc0f207
Compare
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Andrew Yang | ||
| -/ | ||
| import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic |
There was a problem hiding this comment.
Should this new file also be in the AG directory?
There was a problem hiding this comment.
I'm not sure. Does AlgebraicGeometry/CommutativeAlgebra/FreeLocus make sense?
There was a problem hiding this comment.
Yeah, I'm also not sure. Let's leave it as is, but make a mental note.
|
Very nice! |
Co-authored-by: Johan Commelin <johan@commelin.net>
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Andrew Yang | ||
| -/ | ||
| import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic |
There was a problem hiding this comment.
Yeah, I'm also not sure. Let's leave it as is, but make a mental note.
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |