ModuleCoefficientEquation.lean
Nyll.ClassFieldTheory.LubinTate.FormalModule.CoefficientEquation
6 declarations indexed from sourceView source ↗ Module documentation
Coefficient equations for a fixed uniformizer
For a positive degree, the scalar factor 1 - π ^ r is a unit whenever π is a uniformizer. Consequently the corresponding scalar coefficient equation has a unique solution in the valuation ring.
Declarations
LubinTate.SameUniformizer.residueMap_uniformizer_eq_zero
DocumentationA chosen uniformizer reduces to zero in the residue field.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
LubinTate.SameUniformizer.uniformizer_dvd_of_residueMap_eq_zero
DocumentationAn element reducing to zero is divisible by the chosen uniformizer.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
LubinTate.SameUniformizer.residueMap_uniformizer_pow_eq_zero
DocumentationEvery positive power of a uniformizer reduces to zero.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
LubinTate.SameUniformizer.isUnit_one_sub_uniformizer_pow
DocumentationFor positive r, the factor 1 - pi ^ r is a unit of O_K.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
LubinTate.SameUniformizer.existsUnique_mul_eq_of_isUnit
DocumentationLeft multiplication by a unit has a unique preimage for every right-hand side.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
LubinTate.SameUniformizer.existsUnique_one_sub_uniformizer_pow_mul_eq
DocumentationThe scalar coefficient equation in positive total degree has a unique solution in the valuation ring.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}