fix(Topology/Algebra/Valued): repair definition of Valued#14752
fix(Topology/Algebra/Valued): repair definition of Valued#14752AntoineChambert-Loir wants to merge 66 commits intomasterfrom
Conversation
--- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. For details on the "pull request lifecycle" in mathlib, please see: https://leanprover-community.github.io/contribute/index.html In particular, note that most reviewers will only notice your PR if it passes the continuous integration checks. Please ask for help on https://leanprover.zulipchat.com if needed. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> If you are moving or deleting declarations, please include these lines at the bottom of the commit message (that is, before the `---`) using the following format: Moves: - Vector.* -> Mathlib.Vector.* - ... Deletions: - Nat.bit1_add_bit1 - ... Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer
PR summary 583a789b3a
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Valuation.Basic | 1055 | 1057 | +2 (+0.19%) |
| Mathlib.RingTheory.Valuation.RankOne | 1092 | 1094 | +2 (+0.18%) |
| Mathlib.RingTheory.LaurentSeries | 1902 | 1905 | +3 (+0.16%) |
| Mathlib.Topology.Algebra.Valued.ValuationTopology | 1438 | 1440 | +2 (+0.14%) |
| Mathlib.Topology.Algebra.Valued.ValuedField | 1471 | 1473 | +2 (+0.14%) |
| Mathlib.Topology.Algebra.Valued.NormedValued | 1581 | 1583 | +2 (+0.13%) |
| Mathlib.Topology.Algebra.Valued.LocallyCompact | 1666 | 1668 | +2 (+0.12%) |
| Mathlib.NumberTheory.NumberField.FinitePlaces | 2683 | 2685 | +2 (+0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
118 filesMathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.NumberField.AdeleRing 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.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.Ideal Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.ZetaValues Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.PowerSeries.WeierstrassPreparation Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.Quotient Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Ring.Compact Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithVal |
2 |
Mathlib.RingTheory.LaurentSeries |
3 |
Mathlib.Algebra.GroupWithZero.Range (new file) |
257 |
Declarations diff
+ RankLeOne
+ Valued.continuous_valuation_of_rangeGroup₀_eq_top
+ Valued.subtype_continuous_of_rangeGroup₀_eq_top
+ ball_eq_center_vadd_ball
+ ball_subset_ball
+ closedBall_eq_center_vadd_closedBall
+ coe_comp_rangeGroup₀_restrict
+ coe_max
+ coe_min
+ coe_mk_rangeGroup₀_unit
+ coe_rangeGroup₀
+ coe_rangeGroup₀_restrict
+ coe_unit_mem_rangeGroup₀
+ coe_unit_mem_rangeGroup₀_units
+ compare_comp_eq_compare_apply
+ continuous_extension_of_rangeGroup₀_eq_top
+ continuous_rangeGroup₀_extension
+ exists_iff_exists
+ exists_mem_ne_zero_and_lt_one
+ exists_val_lt'
+ extensionValuation_extends
+ extension_eq_of_rangeGroup₀_eq_top
+ hom_rangeGroup₀
+ instance (priority := 100) Valued.topologicalDivisionRing [Valued K Γ₀] :
+ instance : CommGroupWithZero (range₀ f)
+ instance : CommGroupWithZero v.rangeGroup₀ := by
+ instance : LinearOrder v.rangeGroup₀ := inferInstance
+ instance : LinearOrderedCommGroupWithZero v.rangeGroup₀
+ instance : LinearOrderedCommMonoidWithZero v.rangeGroup₀
+ instance : RankLeOne (v.rangeGroup₀_restrict)
+ instance : RankLeOne (valuation (K := K))
+ instance : RankOne (v.rangeGroup₀_restrict)
+ instance {M : Type*} [Monoid M] [LT M]
+ instance {M : Type*} [Monoid M] {r : M → M → Prop}
+ inv_mem_range₀
+ inv_mem_range₀_iff
+ isClopen_ball'
+ isClopen_closedBall'
+ isClopen_sphere'
+ isClosed_ball'
+ isClosed_closedBall'
+ isClosed_sphere'
+ isNontrivial_iff
+ isOpen_ball'
+ isOpen_closedball'
+ isOpen_sphere'
+ ltAddSubgroup_min
+ ltAddSubgroup_monotone
+ mem_ltAddSubgroup_iff
+ mem_rangeGroup₀
+ mem_rangeGroup₀_iff
+ mem_range₀
+ mem_range₀_iff
+ mk_rangeGroup₀_unit
+ nontrivial_range₀
+ rangeGroup₀
+ rangeGroup₀_eq_top
+ rangeGroup₀_eq_top'
+ rangeGroup₀_extension
+ rangeGroup₀_extensionValuation
+ rangeGroup₀_extension_extends
+ rangeGroup₀_restrict
+ range₀
+ range₀_coe_one
+ range₀_coe_zero
+ rankOne_of_exists
+ rankOne_of_nontrivial
+ sphere_eq_center_vadd_sphere
+ strictMono_rangeGroup₀
+ unit_lt_one
+ units_max_eq
+ units_min_eq
+ zero_mem_range₀
++ exists_val_lt
- continuous_extension
- instance (priority := 100) Valued.isTopologicalDivisionRing [Valued K Γ₀] :
- instance : UniformSpace (RatFuncAdicCompl K) := inferInstance
- instance : UniformSpace K⸨X⸩ := inferInstance
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).
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
|
(not quite…) |
|
|
||
| open Set | ||
|
|
||
| /-- The range of a morphism of monoids with codomain a `CommGroupWithZero`, |
There was a problem hiding this comment.
I was very confused by this definition until I realised that actually the codomain is a monoid with zero, not just a monoid. Maybe this should say something like "the group with zero generated by the range of a morphism from a monoid with zero to a group with zero"? or "the smallest group with zero containing the range of a morphism from a monoid with zero to a group with zero" or something?
There was a problem hiding this comment.
I agree, I was also a little confused by the docstring.
Also, you say "as a CommGroupWithZero" but here it is only a Submonoid B, so please mention that the actual instnace of CommGroupWithZero is added later.
|
@AntoineChambert-Loir is this really WIP? |
|
No, it was an old label put while we were struggling with other things: removed. |
riccardobrasca
left a comment
There was a problem hiding this comment.
The diff is quite hard to inspect. Can you split the PR? At least the new file can go to a separate PR.
| /-! # The range of a `MonoidHomWithZero`, | ||
| when the codomain is a `GroupWithZero` | ||
|
|
||
| If `f : A →* B` be a monoid hom, where `B` is a `CommGroupWithZero`, |
There was a problem hiding this comment.
| If `f : A →* B` be a monoid hom, where `B` is a `CommGroupWithZero`, | |
| If `f : A →* B` is a monoid hom, where `B` is a `CommGroupWithZero`, |
| If `f : A →* B` be a monoid hom, where `B` is a `CommGroupWithZero`, | ||
| then `f.range₀` is the smallest submonoid of `B` | ||
| containing the image of `f` which is a `CommGroupWithZero`. | ||
| carrier := { b | ∃ a c, f a ≠ 0 ∧ (f a * b = f c)} |
There was a problem hiding this comment.
This line is probably missing some words...
|
|
||
| open Set | ||
|
|
||
| /-- The range of a morphism of monoids with codomain a `CommGroupWithZero`, |
There was a problem hiding this comment.
I agree, I was also a little confused by the docstring.
Also, you say "as a CommGroupWithZero" but here it is only a Submonoid B, so please mention that the actual instnace of CommGroupWithZero is added later.
|
|
||
| /-- `MonoidHom.range₀ f` is a `CommGroupWithZero` -/ | ||
| instance : CommGroupWithZero (range₀ f) where | ||
| toCommMonoid := inferInstance |
There was a problem hiding this comment.
| toCommMonoid := inferInstance |
| let _ := pkg.uniformStruct | ||
| intro h | ||
| [T3Space γ] {f : α → γ} (cont_f : Continuous f) | ||
| (h : ∀ a : pkg.space, |
There was a problem hiding this comment.
Why are you adding a new assumption here?
| /- The two instances below make `comparePkg` and `comparePkg_eq_extension` slightly faster. -/ | ||
| instance : UniformSpace (RatFuncAdicCompl K) := inferInstance | ||
| instance : UniformSpace K⸨X⸩ := inferInstance | ||
| -- instance : UniformSpace (RatFuncAdicCompl K) := inferInstance |
| theorem valuation_LaurentSeries_equal_extension : | ||
| (LaurentSeriesPkg K).isDenseInducing.extend Valued.v = (Valued.v : K⸨X⸩ → ℤₘ₀) := by | ||
| apply IsDenseInducing.extend_unique | ||
| apply @IsDenseInducing.extend_unique _ _ _ _ _ _ _ |
There was a problem hiding this comment.
Do you really need the @?
| rw [← Valued.extension_extends, ← val_y, ← diff_b_y] | ||
| congr | ||
|
|
||
| example : Valued (RatFuncAdicCompl K) ℤₘ₀ := by |
There was a problem hiding this comment.
Can you add a comment explaining the point of these examples?
|
This pull request has conflicts, please merge |
|
This PR/issue depends on: |
Following a discussion on Zulip, we modify the definition of the field$\gamma$ showing up there is in the subgroup generated by the image of the valuation map.
is_topological_valuationofValuedinsisting that the elementCo-authored-by: @faenuccio