Rings & fields — flashcards
Every card the map can derive about Rings & fields — definitions, statements, attribution, and the edges it sits on.
Definitions 2
Define: The absolute value axioms.
An absolute value on a field satisfies |x| = 0 exactly when x = 0, |xy| = |x||y|, and |x + y| ≤ |x| + |y|. Ostrowski's theorem is the statement that on ℚ these three conditions have far fewer solutions than one would guess.
derived from st/def-abs-axioms by the statement rule
Define: The p-adic integers.
ℤ_p = { x ∈ ℚ_p : |x|_p ≤ 1 }, equivalently the inverse limit of ℤ/pⁿℤ. A local ring with unique maximal ideal pℤ_p and residue field 𝔽_p.
derived from st/def-zp by the statement rule
Theorems 3
State: Bézout's identity.
For integers a, b there exist integers x, y with ax + by = gcd(a, b). The extended Euclidean algorithm computes them.
derived from st/bezout by the statement rule
State: Teichmüller lifts.
Each nonzero residue mod p lifts uniquely to a (p−1)st root of unity in ℤ_p, giving a canonical multiplicative section of ℤ_p× → 𝔽_p×. The residue field sits inside the ring, multiplicatively but not additively.
derived from st/teichmuller by the statement rule
State: Valued fields can be completed.
Any field carrying an absolute value has a completion, constructed exactly as ℝ is built from ℚ. This is what puts ℚ_p on the same footing as ℝ rather than treating it as an exotic construction.
derived from st/kurschak-completion by the statement rule
Names and dates 5
Bézout's identity — who, and when?
Claude Bachet, then Étienne Bézout, 1624 (Bachet), 1779 (Bézout).
derived from st/bezout by the attribution rule
The absolute value axioms — who, and when?
József Kürschák, 1912.
derived from st/def-abs-axioms by the attribution rule
Teichmüller lifts — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/teichmuller by the attribution rule
The p-adic integers — who, and when?
Kurt Hensel, 1897.
derived from st/def-zp by the attribution rule
Valued fields can be completed — who, and when?
József Kürschák, 1912.
derived from st/kurschak-completion by the attribution rule
Formalisation 2
What is Bézout's identity called in Mathlib?
Nat.gcd_eq_gcd_ab — Mathlib.Data.Int.GCD
derived from st/bezout by the binding rule
What is The p-adic integers called in Mathlib?
PadicInt — Mathlib.NumberTheory.Padics.PadicIntegers
derived from st/def-zp by the binding rule
Connections 8
Under the Degeneracy lens, how do Division algebra ladder and Rings & fields relate? [Degeneracy]
The commutative, associative, ordered case is one rung of a short ladder that provably stops at eight dimensions. It is the rung everybody starts on and the least general one.
derived from degeneracy:division-algebras→rings-fields by the connection rule
What is the correspondence between Rings & fields and Groups & symmetry? [Correspondences]
Subfields of a normal extension ↔ subgroups of its automorphism group, inclusion-reversing. Solvability of the group ↔ solvability of the equation by radicals.
derived from correspondences:rings-fields→group-theory by the connection rule
What is the correspondence between Coordinate geometry and Rings & fields? [Correspondences]
Affine algebraic sets ↔ radical ideals in a polynomial ring. Geometry of solutions ↔ algebra of the equations defining them.
derived from correspondences:coordinate-geometry→rings-fields by the connection rule
What is the correspondence between Generating functions and Rings & fields? [Correspondences]
Sequences ↔ elements of a power series ring; convolution of sequences ↔ multiplication. Counting arguments become ring computations.
derived from correspondences:generating-functions→rings-fields by the connection rule
What is the correspondence between Riemann surfaces and Rings & fields? [Correspondences]
Compact Riemann surfaces ↔ algebraic function fields of one variable, an equivalence of categories. A geometric object and an algebraic one carrying identical information.
derived from correspondences:riemann-surfaces→rings-fields by the connection rule
In Mathlib, what is the import relation between Euclidean algorithm and Rings & fields? [Dependency (Mathlib)]
`Mathlib.Data.Int.GCD` imports `Mathlib.Algebra.Divisibility.Basic`, `Mathlib.Algebra.GroupWithZero.Semiconj`, `Mathlib.Algebra.GroupWithZero.Divisibility`, `Mathlib.Algebra.GroupWithZero.Nat`. Read off Mathlib/Data/Int/GCD.html. No human asserted this edge.
derived from dependency:euclidean-algorithm→rings-fields by the connection rule
In Mathlib, what is the import relation between Continued fractions and Rings & fields? [Dependency (Mathlib)]
`Mathlib.Algebra.ContinuedFractions.Basic` imports `Mathlib.Algebra.Field.Defs`. Read off Mathlib/Algebra/ContinuedFractions/Basic.html. No human asserted this edge.
derived from dependency:continued-fractions→rings-fields by the connection rule
In Mathlib, what is the import relation between p-adic numbers and Rings & fields? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Padics.Hensel` imports `Mathlib.Algebra.Polynomial.Identities`. Read off Mathlib/NumberTheory/Padics/Hensel.html. No human asserted this edge.
derived from dependency:p-adic-numbers→rings-fields by the connection rule
Concepts 1
What is Rings & fields, in one sentence?
Abstract structures generalising arithmetic — sets with addition and multiplication obeying fixed axioms.
derived from rings-fields by the concept rule