[Merged by Bors] - feat: add some result on `IsFractionRing` and `fieldRange` by acmepjz · Pull Request #18984 · leanprover-community/mathlib4

acmepjz · 2024-11-13T16:49:25Z

In Mathlib/RingTheory/Localization/FractionRing.lean:

IsFractionRing.closure_range_algebraMap: if A is a ring with fraction field K, then the subfield of K generated by the image of algebraMap A K is equal to the whole field K.
IsFractionRing.ringHom_fieldRange_eq_of_comp_eq[_of_range_eq]: if A is a ring with fraction field K, L is a field, g : A →+* L lifts to f : K →+* L, then the image of f is the field generated by the image of g.

In Mathlib/FieldTheory/Adjoin.lean:

IsFractionRing.algHom_fieldRange_eq_of_comp_eq[_of_range_eq]: if F is a field, A is an F-algebra with fraction field K, L is a field, g : A →ₐ[F] L lifts to f : K →ₐ[F] L, s is a set such that the image of g is the subalgebra generated by s, then the image of f is the intermediate field generated by s. Note: this does not require IsScalarTower F A K.

github-actions · 2024-11-13T16:50:21Z

PR summary 3166ea683c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Localization.FractionRing	854	856	+2 (+0.23%)

Import changes for all files

Files	Import difference
176 files `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.PowerBasis` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct` `Mathlib.RingTheory.DedekindDomain.Ideal` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.RingTheory.Ideal.Over` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.RingTheory.ClassGroup` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.RingTheory.Polynomial.Dickson` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.RingTheory.Localization.Integral` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Module` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.Algebraic` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.Algebra.AlgebraicCard` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.RingTheory.Localization.Free` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.RingTheory.AlgebraicIndependent` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.RingTheory.Etale.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.Algebra.CharP.Algebra` `Mathlib.RingTheory.Localization.Module` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.NumberTheory.Bernoulli` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.RingTheory.MaximalSpectrum` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.RingTheory.IntegralDomain` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.LinearAlgebra.Matrix.FixedDetMatrices` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.Algebra.Module.LocalizedModule.Submodule`	2

Declarations diff

+ algHom_fieldRange_eq_of_comp_eq
+ algHom_fieldRange_eq_of_comp_eq_of_range_eq
+ closure_range_algebraMap
+ ringHom_fieldRange_eq_of_comp_eq
+ ringHom_fieldRange_eq_of_comp_eq_of_range_eq

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

Mathlib/RingTheory/Localization/FieldRange.lean

alreadydone · 2024-11-14T15:37:52Z

Thanks!
maintainer merge

github-actions · 2024-11-14T15:38:10Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

riccardobrasca · 2024-11-14T15:41:40Z

Mathlib/RingTheory/Localization/FractionRing.lean

 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.RingTheory.Localization.Basic
+import Mathlib.RingTheory.SimpleRing.Basic


I am a little concerned about this new import. Maybe we can create a new file?

See the comment here: #18868 (comment)

Note that the new import is Mathlib.Algebra.Field.Subfield.Basic. The Mathlib.RingTheory.SimpleRing.Basic is just reordered alphabetically.

riccardobrasca · 2024-11-14T18:04:51Z

Thanks!

bors merge

In `Mathlib/RingTheory/Localization/FractionRing.lean`: - `IsFractionRing.closure_range_algebraMap`: if `A` is a ring with fraction field `K`, then the subfield of `K` generated by the image of `algebraMap A K` is equal to the whole field `K`. - `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq[_of_range_eq]`: if `A` is a ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to `f : K →+* L`, then the image of `f` is the field generated by the image of `g`. In `Mathlib/FieldTheory/Adjoin.lean`: - `IsFractionRing.algHom_fieldRange_eq_of_comp_eq[_of_range_eq]`: if `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field, `g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`, `s` is a set such that the image of `g` is the subalgebra generated by `s`, then the image of `f` is the intermediate field generated by `s`. Note: this does not require `IsScalarTower F A K`.

mathlib-bors · 2024-11-14T18:27:30Z

Pull request successfully merged into master.

Build succeeded:

In `Mathlib/RingTheory/Localization/FractionRing.lean`: - `IsFractionRing.closure_range_algebraMap`: if `A` is a ring with fraction field `K`, then the subfield of `K` generated by the image of `algebraMap A K` is equal to the whole field `K`. - `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq[_of_range_eq]`: if `A` is a ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to `f : K →+* L`, then the image of `f` is the field generated by the image of `g`. In `Mathlib/FieldTheory/Adjoin.lean`: - `IsFractionRing.algHom_fieldRange_eq_of_comp_eq[_of_range_eq]`: if `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field, `g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`, `s` is a set such that the image of `g` is the subalgebra generated by `s`, then the image of `f` is the intermediate field generated by `s`. Note: this does not require `IsScalarTower F A K`.

add some result on IsFractionRing and fieldRange

b352754

acmepjz added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Nov 13, 2024

acmepjz mentioned this pull request Nov 13, 2024

[Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results #18648

Closed

2 tasks

alreadydone reviewed Nov 13, 2024

View reviewed changes

Mathlib/RingTheory/Localization/FieldRange.lean Outdated Show resolved Hide resolved

acmepjz added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 13, 2024

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2024

acmepjz added 2 commits November 14, 2024 01:46

add IsFractionRing.closure_range_algebraMap and golf

186d798

make variable explicit and golf

498415b

alreadydone reviewed Nov 13, 2024

View reviewed changes

Mathlib/RingTheory/Localization/FieldRange.lean Outdated Show resolved Hide resolved

alreadydone approved these changes Nov 13, 2024

View reviewed changes

acmepjz added 3 commits November 14, 2024 15:26

Merge branch 'master' into acmepjz_loc_field_range

177dc3e

move 3 results to earlier file

3ce1b54

move results to Adjoin

e683782

acmepjz changed the title ~~feat(RingTheory/Localization/FieldRange): add some result on IsFractionRing and fieldRange~~ feat: add some result on IsFractionRing and fieldRange Nov 14, 2024

fix typo

3166ea6

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 14, 2024

riccardobrasca reviewed Nov 14, 2024

View reviewed changes

github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 14, 2024

mathlib-bors bot changed the title ~~feat: add some result on IsFractionRing and fieldRange~~ [Merged by Bors] - feat: add some result on IsFractionRing and fieldRange Nov 14, 2024

mathlib-bors bot closed this Nov 14, 2024

mathlib-bors bot deleted the acmepjz_loc_field_range branch November 14, 2024 18:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: add some result on `IsFractionRing` and `fieldRange`#18984

[Merged by Bors] - feat: add some result on `IsFractionRing` and `fieldRange`#18984
acmepjz wants to merge 7 commits intomasterfrom
acmepjz_loc_field_range

acmepjz commented Nov 13, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 13, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

alreadydone commented Nov 14, 2024

Uh oh!

github-actions bot commented Nov 14, 2024

Uh oh!

riccardobrasca Nov 14, 2024

Uh oh!

alreadydone Nov 14, 2024

Uh oh!

acmepjz Nov 14, 2024

Uh oh!

riccardobrasca Nov 14, 2024

Uh oh!

riccardobrasca commented Nov 14, 2024

Uh oh!

mathlib-bors bot commented Nov 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

acmepjz commented Nov 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3166ea683c

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

alreadydone commented Nov 14, 2024

Uh oh!

github-actions bot commented Nov 14, 2024

Uh oh!

riccardobrasca Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

alreadydone Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

acmepjz Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

riccardobrasca Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

riccardobrasca commented Nov 14, 2024

Uh oh!

mathlib-bors bot commented Nov 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

acmepjz commented Nov 13, 2024 •

edited

Loading

github-actions bot commented Nov 13, 2024 •

edited

Loading