feat(Mathlib/RingTheory/Ideal/Cotangent): dimension of cotangent spaces #33247
Conversation
github-actions
bot
added
the
new-contributor
PR summary ed813e9b04
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Ideal.Cotangent | 1297 | 1301 | +4 (+0.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.Nakayama |
-929 |
Mathlib.RingTheory.KrullDimension.Regular Mathlib.RingTheory.LocalProperties.Semilocal |
1 |
62 filesMathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.Ideal Mathlib.NumberTheory.NumberField.InfiniteAdeleRing Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus Mathlib.Topology.Algebra.Ring.Compact |
2 |
31 filesMathlib.Algebra.Module.Presentation.Differentials Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Extension.Presentation.Basic Mathlib.RingTheory.Extension.Presentation.Core Mathlib.RingTheory.Extension.Presentation.Submersive Mathlib.RingTheory.Flat.TorsionFree Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Flat Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi |
3 |
8 filesMathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.RingTheory.Extension.Basic Mathlib.RingTheory.Extension.Generators Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct |
4 |
Mathlib.RingTheory.Nakayama.Basic |
929 |
Mathlib.RingTheory.Nakayama.SpanRank (new file) |
1208 |
Declarations diff
+ cotangentEquivSubmodule
+ cotangentSubmodule
+ exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot
+ quotientIdealSubmoduleEquivMap
+ rank_cotangentSpace_eq_spanrank_maximalIdeal
+ spanFinrank_map_le_of_fg
+ spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot
+ spanRank_eq_spanRank_of_addEquiv
+ spanRank_eq_spanRank_of_equiv
+ spanRank_eq_spanRank_of_equiv'
+ spanRank_eq_spanRank_quotientIdealSubmodule
+ spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule
+ spanRank_le_spanRank_of_map_eq
+ spanRank_le_spanRank_of_range_eq
+ spanRank_le_spanRank_of_surjective
+ spanRank_map_le
+ span_eq_of_map_mkQ_span_eq_map_mkQ_of_le_jacobson_bot
+ span_eq_of_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot
- Submodule.spanFinrank_map_le_of_fg
- Submodule.spanRank_map_le
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
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
note: file Mathlib/RingTheory/Nakayama.lean` was renamed to `Mathlib/RingTheory/Nakayama/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
github-actions
bot
added
the
file-removed
grunweg
changed the title
sun123zxy
force-pushed
the
cotangent-spanrank
branch
from
40cee44 to
bcffea0
Compare
| lemma spanRank_eq_spanRank_of_addEquiv (σ : R →+* S) [RingHomSurjective σ] | ||
| (e : M₁ ≃+ N₁) (hm : ∀ (r : R) (m : M₁), e (r • m) = (σ r) • (e m)) : | ||
| M₁.spanRank = N₁.spanRank := by |
There was a problem hiding this comment.
Do you really need this generality?
There was a problem hiding this comment.
I feel like it is better to prove (M.restrictScalars R).spanRank = M.spanRank if M : Submodule S N and R -> S is surjective.
There was a problem hiding this comment.
(and then you can recover this easily if you really want to)
There was a problem hiding this comment.
Oh yes it is better. I was unaware of restrictScalars previously. Changes are applied in the split PR.
| theorem exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot | ||
| {I : Ideal R} {N : Submodule R M} (s : Set (M ⧸ (I • N))) | ||
| (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (hsspan : span R s = map (I • N).mkQ N) : | ||
| ∃ (t : Set M) (e : t ≃ s), (∀ x : t, e x = (I • N).mkQ x) ∧ span R t = N := by |
There was a problem hiding this comment.
This seems like a weird statement. Would it better to state t.injOn (I • N).mkQ and (I • N).mkQ '' t = s?
There was a problem hiding this comment.
Yes it is better! Resolved in the split PR.
erdOne
left a comment
erdOne
left a comment
There was a problem hiding this comment.
Also could you split this PR up? This PR is slightly too large to give a coherent review.
Perhaps you can move the functoriality of span rank to a separate PR, and the new statements of Nakayama lemma to another one etc.
erdOne
added
the
awaiting-author
|
Sure, then I'll first draft a new pull request for span rank functionalities once the related reviews are addressed. |
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
-awaiting-author |
github-actions
bot
added
WIP
4 participants
It is shown that the span rank of the maximal ideal of a local ring equals the dimension of the cotangent space
if the maximal ideal is finitely generated.
To avoid unnecessary imports, the original
Mathlib/RingTheory/Nakayamais now moved toMathlib/RingTheory/Nakayama/Basic.