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 11 commits intoleanprover-community:masterfrom
Conversation
PR summary 06a46dae32
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.FieldTheory.KrullTopology | 1866 | 1868 | +2 (+0.11%) |
| Mathlib.FieldTheory.Galois.Infinite | 1900 | 1902 | +2 (+0.11%) |
| Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter | 2049 | 2050 | +1 (+0.05%) |
| Mathlib.FieldTheory.Galois.Profinite | 2202 | 2203 | +1 (+0.05%) |
Import changes for all files
| Files | Import difference |
|---|---|
37 filesMathlib.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.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation 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.LucasLehmer Mathlib.NumberTheory.NumberField.CMField Mathlib.NumberTheory.NumberField.ClassNumber 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.Ideal.Asymptotics Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic |
1 |
8 filesMathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.Galois.Abelian Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.KrullTopology Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.NumberTheory.RamificationInertia.HilbertTheory Mathlib.RingTheory.Ideal.Norm.RelNorm |
2 |
Declarations diff
+ AlgEquiv.totallyBounded_univ
+ IntermediateField.isClosed_fixingSubgroup
+ IntermediateField.isOpen_fixingSubgroup
+ instance : IsUniformGroup Gal(L/K)
+ instance : UniformSpace Gal(L/K) := .ofCore
+ instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K)
+ instance [Algebra.IsIntegral K L] : TotallySeparatedSpace Gal(L/K) := by
+ krullTopology_mem_uniformity_iff
- instance (K L : Type*) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup Gal(L/K)
- instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.07)
| Current number | Change | Type |
|---|---|---|
| 6891 | 3 | backward.isDefEq |
| 14 | 1 | disabled deprecation lints |
Current commit b08bce4d5a
Reference commit 06a46dae32
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).
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?
| 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 <[email protected]>
Co-authored-by: Violeta Hernández Palacios <[email protected]>
| 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
3 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.