Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharSubgroupCharacterLogVector

Module documentation

Restricted-character vectors in the actual logarithm image

A subgroup-supported normal-basis vector is an eigenvector for the subgroup and fails the prescribed character relation at an automorphism outside it. Multiplying by a power of the residue prime puts the vector in the principal-unit logarithm image and preserves both properties.

The p-adic coefficients in the base and extension fields are compared by the actual valued-extension map. The base residue characteristic is deduced from the extension. No normality of the subgroup, group-order condition, or valuation-preservation assumption is used.

theorem

exists_principalUnit_log_subgroupCharacter_eigen_not_eigen

L36 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_subgroupCharacter_eigen_not_eigen

Documentation

There is a nonzero actual principal-unit logarithm which is a character eigenvector on Δ and fails the same character relation at any prescribed automorphism outside Δ.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] [IsGalois F E] [CharZero E]

Lean source · statement

theorem exists_principalUnit_log_subgroupCharacter_eigen_not_eigen
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vF]
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    [vF.HasExtension vE]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    (Δ : Subgroup Gal(E/F)) (χ : Gal(E/F) →* ℤ_[p]ˣ)
    (g : Gal(E/F)) (hg : g ∉ Δ) :
    ∃ u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1,
      (principalUnitLogOfMixedChar vE p u).toAdd ≠ 0 ∧
      (∀ δ : Δ, (δ : Gal(E/F)) (principalUnitLogOfMixedChar vE p u).toAdd =
        padicIntToFieldOfMixedChar vE p (χ (δ : Gal(E/F)) : ℤ_[p]) *
          (principalUnitLogOfMixedChar vE p u).toAdd) ∧
      g (principalUnitLogOfMixedChar vE p u).toAdd ≠
        padicIntToFieldOfMixedChar vE p (χ g : ℤ_[p]) *
          (principalUnitLogOfMixedChar vE p u).toAdd

Module documentation

Restricted-character vectors in the actual logarithm image

Declarations

exists_principalUnit_log_subgroupCharacter_eigen_not_eigen