ModuleTeichmuller.lean
Nyll.ValuedFieldTheory.LocalField.Padic.Teichmuller
7 declarations indexed from sourceView source ↗ Module documentation
Teichmüller representatives in the p-adic units
Hensel lifting in the concrete complete discrete valuation field ℚ_[p] gives a multiplicative section of reduction to (ZMod p)ˣ. Its values are (p - 1)-st roots of unity, including when p = 2.
Declarations
LocalFieldTheory.DiscreteValuationField.Examples.Qp.teichmullerIntegerEquiv
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.teichmullerResidueEquiv
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.toZMod_valuationSubring_symm
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.teichmullerRoots
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.teichmullerUnits
DocumentationThe multiplicative Teichmüller section from residue units to p-adic units.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.toZMod_teichmullerUnits
DocumentationReducing a Teichmüller representative recovers the original residue unit.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite
LocalFieldTheory.DiscreteValuationField.Examples.Qp.teichmullerUnits_pow
DocumentationEvery Teichmüller representative is a (p - 1)-st root of unity.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.Examples.Qp
open CompleteDVF.higherPrincipalUnitGroup
variable (p : ℕ) [Fact p.Prime]
-- The only additional instance is the existing finiteness proof for Qp's residue field.
attribute [local instance] padicCompleteDVF_residueField_finite