LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_minimal_characterEigenvector_log_image
The character eigenvectors in L that are logarithms in M have a least valuation.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
variable {K L M : Type*} [Field K] [Field L] [Field M]
[Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Algebra L M] [CharZero M]Lean source · statement
theorem exists_minimal_characterEigenvector_log_image
(v : _root_.Valuation M (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
(χ : (L ≃ₐ[K] L) →* Kˣ) :
∃ b : Lˣ,
(∀ σ : L ≃ₐ[K] L, σ (b : L) = (χ σ : K) • (b : L)) ∧
(∃ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
(principalUnitLogOfMixedChar v p u).toAdd = algebraMap L M (b : L)) ∧
∀ c : Lˣ,
(∀ σ : L ≃ₐ[K] L, σ (c : L) = (χ σ : K) • (c : L)) →
(∃ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
(principalUnitLogOfMixedChar v p u).toAdd = algebraMap L M (c : L)) →
(ofWithZeroValuation v).val (Units.map (algebraMap L M).toMonoidHom b) ≤
(ofWithZeroValuation v).val (Units.map (algebraMap L M).toMonoidHom c)