LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnit_log_eigen_lift
Every character eigenvector in the actual log image lifts to a character eigenvector in the actual principal-unit group.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable {Δ : Type w} [Group Δ] [Fintype Δ]
open CompleteDVF.higherPrincipalUnitGroupLean source · statement
theorem exists_principalUnit_log_eigen_lift
(v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
(σ : Δ →* (K ≃+* K)) (hval : ∀ (g : Δ) (x : K), v (σ g x) = v x)
(hcard : p.Coprime (Fintype.card Δ)) (χ : Δ →* ℤ_[p]ˣ) (b : K)
(himage : ∃ x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
(principalUnitLogOfMixedChar v p x).toAdd = b)
(heigen : ∀ g : Δ, σ g b = padicIntToFieldOfMixedChar v p (χ g : ℤ_[p]) * b) :
∃ x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
(principalUnitLogOfMixedChar v p x).toAdd = b ∧
∀ g : Δ,
σ g (((x : (completeDVFOfWithZeroValuation v).valuationSubringˣ) :
(completeDVFOfWithZeroValuation v).valuationSubring) : K) =
(((principalUnitPadicPowOfMixedChar v p (χ g : ℤ_[p]) x :
(completeDVFOfWithZeroValuation v).valuationSubringˣ) :
(completeDVFOfWithZeroValuation v).valuationSubring) : K)