feat(FieldTheory/KrullTopology): define uniform group structure on galois group - #36239
feat(FieldTheory/KrullTopology): define uniform group structure on galois group#36239plp127 wants to merge 44 commits into
Conversation
PR summary 00b209d4e8
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.FieldTheory.KrullTopology | 1953 | 1970 | +17 (+0.87%) |
| Mathlib.FieldTheory.Galois.Infinite | 1956 | 1973 | +17 (+0.87%) |
| Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter | 2173 | 2175 | +2 (+0.09%) |
| Mathlib.FieldTheory.Galois.Profinite | 2281 | 2283 | +2 (+0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
59 filesMathlib.Algebra.Module.Torsion.PrimaryComponent Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.FieldTheory.Galois.Profinite Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Complex Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings Mathlib.NumberTheory.NumberField.Cyclotomic.Galois Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.ExistsRamified Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.Localization.AtPrime.Extension Mathlib.RingTheory.RamificationInertia.Basic Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Ring.Compact |
2 |
5 filesMathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.Galois.Abelian Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.KrullTopology |
17 |
Mathlib.FieldTheory.FinTrdeg (new file) |
1756 |
Declarations diff (regex)
+ AlgEquiv.isComplete_fixingSubgroup
+ AlgEquiv.totallyBounded_fixingSubgroup
+ AlgEquiv.totallyBounded_univ
+ FinTrdeg
+ FinTrdeg.of_isTranscendenceBasis
+ FinTrdeg.of_trdeg
+ FinTrdeg.trans
+ IntermediateField.isClosed_fixingSubgroup
+ IntermediateField.isOpen_fixingSubgroup
+ coe_fixingSubgroupEquiv_apply
+ coe_fixingSubgroupEquiv_symm_apply
+ coe_subgroupEquivAlgEquiv_apply
+ coe_subgroupEquivAlgEquiv_symm_apply
+ completeSpace_of_weaklyLocallyCompactSpace
+ exists_finset_isTranscendenceBasis
+ finTrdeg_iff_trdeg
+ finite_of_algebraicIndependent
+ finite_of_isTranscendenceBasis
+ instance : Algebra.IsAlgebraic (⊤ : IntermediateField K L) L
+ instance : Algebra.IsAlgebraic K (⊥ : IntermediateField K L)
+ instance : IsLeftUniformGroup Gal(L/K)
+ instance : TotallySeparatedSpace Gal(L/K) := by
+ instance : UniformSpace Gal(L/K) := .ofCore
+ instance [Algebra.EssFiniteType K L] : FinTrdeg K L
+ instance [Algebra.IsAlgebraic K L] : FinTrdeg K L
+ instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K)
+ instance [Algebra.IsIntegral R A] (S : Set A) : Algebra.IsIntegral R (Algebra.adjoin R S)
+ instance [Algebra.IsIntegral R A] (S : Set A) [Finite S] : Module.Finite R (Algebra.adjoin R S)
+ instance [FinTrdeg K L] : CompleteSpace Gal(L/K)
+ instance [FinTrdeg K L] : LocallyCompactSpace Gal(L/K) := sorry
+ instance [Finite S] : Algebra.EssFiniteType F (adjoin F S)
+ instance {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} [Finite t] :
+ instance {S : Set L} [Finite S] [Algebra.IsIntegral K L] :
+ isComplete_univ
+ krullTopology_discreteUniformity_of_essFiniteType
+ krullTopology_mem_nhds_one_iff'
+ krullTopology_mem_uniformity_iff
+ krullTopology_mem_uniformity_iff_fg
+ krullTopology_uniformity_def
+ trdeg_lt_aleph0_of_finiteType
- instance (K L : Type*) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup Gal(L/K)
- instance [IsGalois k K] : CompactSpace Gal(K/k)
- instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :
- krullTopology_discreteTopology_of_finiteDimensional
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean -- pending)
Computed after the build finishes.
No changes to strong technical debt.
Decrease in weak tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 5021 | -1 | exposed public sections |
Current commit 00b209d4e8
Reference commit d732046e27
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).
plp127
added
the
awaiting-CI
| ⟨fun _ _ _ h₁ h₂ => h₁.trans h₂⟩)) } | ||
|
|
||
| open SetRel in | ||
| theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} : |
There was a problem hiding this comment.
There's nothing called krullTopology in this statement. Maybe mem_uniformity_gal_iff?
There was a problem hiding this comment.
There's also nothing called gal in this statement. Maybe mem_uniformity_algEquiv_self_iff?
There was a problem hiding this comment.
Maybe we have convention that call this gal otherwise algEquiv_self is too long?
| instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] : | ||
| TopologicalSpace Gal(L/K) := | ||
| GroupFilterBasis.topology (galGroupBasis K L) | ||
| instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance |
There was a problem hiding this comment.
a) You should probably update the docstring.
b) Do we still need this? Maybe we should remove this and instead add some blurb about the Krull topology on the uniformity instance.
| open scoped Topology in | ||
| lemma krullTopology_mem_nhds_one_iff (K L : Type*) [Field K] [Field L] [Algebra K L] | ||
| (s : Set Gal(L/K)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, | ||
| lemma krullTopology_mem_nhds_one_iff {s : Set Gal(L/K)} : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, |
There was a problem hiding this comment.
Again, not sure if you want krullTopology in the names of these statements. Maybe the correct fix is to put all of this in a KrullTopology namespace?
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
| module | ||
|
|
||
| public import Mathlib.FieldTheory.Galois.Basic | ||
| public import Mathlib.Topology.Algebra.FilterBasis |
There was a problem hiding this comment.
Note this import is now only used in this file by the deprecated things. If I delete the deprecations I can delete the import.
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
plp127
changed the title
github-actions
Bot
removed
merge-conflict
dagurtomas
added
the
awaiting-author
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
6 participants
Endow the galois group of a field extension
Gal(L/K)with the structure of a uniform group. Use this to prove some properties of the galois group earlier, for example, that the galois group is compact is immediate, and in more generality than the version proved inFieldTheory/Galois/Profinite. Deprecate some material which used to be used to define the krull topology, but is now unused since the krull topology comes out of the uniform structure.adjoin#42154fixingSubgroupEquivandsubgroupEquivAlgEquiv#42141complete_univtoisComplete_univ#42163