ModuleBasic.lean
Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.Basic
3 declarations indexed from sourceView source ↗ Module documentation
Higher local fields and finiteness of roots of unity
A zero-dimensional higher local field is a finite field. At each successor step we choose a complete discrete valuation whose actual residue field is one dimension lower. No Galois-theoretic or finite-extension permanence property is included in the definition.
Finiteness of all roots of unity is proved by induction on this actual residue tower, using the reduction map in each of the characteristic cases.
Declarations
ValuationTheory.IsHigherLocalField
DocumentationA finite residue tower of complete discretely valued fields ending in a finite field. The value groups of the chosen valuations lie in Type v.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory
open ValuationTheory.DiscreteValuationField
universe u v
ValuationTheory.IsHigherLocalField.finite_torsion
DocumentationEvery higher local field has finitely many roots of unity, in all characteristics and dimensions.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory
open ValuationTheory.DiscreteValuationField
universe u v
ValuationTheory.IsHigherLocalField.of_finiteExtension
DocumentationA finite field extension of an n-dimensional higher local field is again an n-dimensional higher local field. Its valuation and residue tower are produced by the conclusion.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory
open ValuationTheory.DiscreteValuationField
universe u v