feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop'#36421
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop'#36421ROTARTSI82 wants to merge 7 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
github-actions
bot
added
the
large-import
PR summary 034c50cbf6Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.FieldTheory.Minpoly.Basic | 1354 | 1567 | +213 (+15.73%) |
Import changes for all files
| Files | Import difference |
|---|---|
42 filesMathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Normed.Field.WithAbs Mathlib.FieldTheory.Minpoly.Field Mathlib.FieldTheory.Normal.Defs Mathlib.FieldTheory.Separable Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.NumberTheory.Ostrowski Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Finiteness.Descent Mathlib.RingTheory.Finiteness.FinitePresentationLocal Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Locus Mathlib.RingTheory.Unramified.Pi |
1 |
Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral |
7 |
Mathlib.FieldTheory.Minpoly.Basic |
213 |
Declarations diff
+ mkOfAdjoinEqTop'
+ natDegree_le'
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/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).
|
t-algebra For the large import changes, we are a bit unsure about the placement of the |
Alternative hypothesis to existing theorem: prove the result from a Module.Free hypothesis instead of IsIntegrallyClosed. If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. Co-authored-by: George Peykanu <[email protected]> Co-authored-by: Bryan Boehnke <[email protected]> Co-authored-by: Bianca Viray <[email protected]>
Formalization of lemma 3.2 from https://arxiv.org/abs/2503.07846: Given a local finite ring extension R -> S, if the algebraMap is etale, then there exists a β ∈ S such that R[β] = S. Furthermore, if f(z) ∈ R[z] is the minimal polynomial of β, then f′(β) ∈ S×.
This reverts commit cc73956.
ROTARTSI82
force-pushed
the
grant/monogenic-extensions
branch
from
2704aea to
19a085a
Compare
|
t-ring-theory |
|
Haven't had time to review yet but IIRC the proof duplicates existing material in Mathlib. Will come back to this as soon as I can and look into it properly. |
5 participants
Alternative hypothesis to existing theorem: prove the result from a
Module.Freehypothesis instead ofIsIntegrallyClosed. IfαgeneratesSas an algebra, thenSis given by adjoining a root ofminpoly R α.Hello, we are the Algebraic Geometry group from the UW Math AI lab, and this is our first PR! This definition of
mkOfAdjoinEqTop'generalizes the existingmkOfAdjoinEqTopand shows the result fromModule.Freeinstead ofIsIntegrallyClosed. It is used in future results that we would like to upstream at https://github.com/uw-math-ai/monogenic-extensions, which is a project to formalize lemmas 3.1 and 3.2 from https://arxiv.org/abs/2503.07846.Co-authored-by: George Peykanu [email protected]
Co-authored-by: Bryan Boehnke [email protected]
Co-authored-by: Bianca Viray [email protected]
-->