Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogImage

Module documentation

Nonzero character eigenvectors in an overfield's logarithm image

An eigenvector in a finite Galois extension remains in that field after multiplication by a power of the residue prime. In a complete mixed-characteristic overfield, a suitable such multiple is a principal-unit logarithm. No valuation or completeness assumption on the intermediate field is needed.

theorem

exists_nonzero_characterEigenvector_log_image

L25 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_nonzero_characterEigenvector_log_image

Documentation

A nonzero character eigenvector in L lies in the principal-unit log image of M.

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_nonzero_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)

Module documentation

Nonzero character eigenvectors in an overfield's logarithm image

Declarations

exists_nonzero_characterEigenvector_log_image