ModuleFieldUnitFactors.lean
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldUnitFactors
10 declarations indexed from sourceView source ↗ Module documentation
Finite and uniformizer factors of the field-unit group
This file isolates the two factors of the field-unit structure theorem which do not depend on the structure theorem for first principal units. The Teichmuller factor is the cyclic group of order q - 1, with its (necessarily discrete) topology.
Declarations
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuousMulEquivOfCompactToT2
DocumentationA continuous algebraic equivalence from a compact group to a Hausdorff group is automatically a topological group equivalence.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuousAddEquivOfCompactToT2
DocumentationAdditive version of continuousMulEquivOfCompactToT2.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuousMulEquivProdCongr
DocumentationProduct of two topological multiplicative equivalences.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuousMulEquivProdComm
DocumentationSwapping two factors is a topological multiplicative equivalence.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityContinuousMulEquivZMod
DocumentationThe Teichmuller roots form, algebraically and topologically, the cyclic group of order q - 1, where q is the residue-field cardinality.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsContinuousMulEquivCyclicRootsPrincipalUnitsUniformizer
DocumentationThe field-unit structure theorem with the still-to-be-classified first-principal-unit factor left visible: the other two factors are already the standard cyclic factors appearing in the decomposition.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsContinuousMulEquivRootsPrincipalUnitsUniformizerOfWithZeroValuation
DocumentationThe uniformizer–residue–principal-unit decomposition in the topology carried directly by a standard ℤᵐ⁰-valued valuation. This is the decomposition used to assemble the two cases of the field-unit structure theorem.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityContinuousMulEquivZModOfWithZeroValuation
DocumentationThe Teichmuller root factor in the direct topology of a standard ℤᵐ⁰-valued valuation.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsContinuousMulEquivCyclicRootsPrincipalUnitsUniformizerOfWithZeroValuation
DocumentationThe field-unit structure theorem with the principal-unit factor left visible, now in the direct standard valuation topology.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsContinuousMulEquivUniformizerRootsPrincipalUnitsOfWithZeroValuation
DocumentationAssemble the field-unit structure theorem from a topological classification of U^1, with the factors ordered canonically as: uniformizer, Teichmuller roots, then principal units.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
variable {K : Type u} [Field K]