Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCyclotomicEigenUnit

theorem

valuation_algEquiv_eq_of_complete

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_algEquiv_eq_of_complete

Source context 1 command

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation

Lean source · statement

theorem valuation_algEquiv_eq_of_complete
    {F E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vF]
    [vE.IsRankOneDiscrete] [vF.HasExtension vE]
    (σ : E ≃ₐ[F] E) (x : E) : vE (σ x) = vE x

theorem

exists_minimal_cyclotomic_log_eigenunit

L46 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_minimal_cyclotomic_log_eigenunit

Documentation

The actual upper cyclotomic action admits an eigenunit whose nonzero logarithm is a lower-field eigenvector of minimal valuation in the log image.

Source context 2 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
variable {F K L E : Type*} [Field F] [Field K] [Field L] [Field E]
  [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
  [IsScalarTower F K E] [IsScalarTower F L E]
  [FiniteDimensional F E] [CharZero E]

Lean source · statement

theorem exists_minimal_cyclotomic_log_eigenunit
    (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]
    [IsCyclotomicExtension {p} F K] [IsCyclotomicExtension {p} L E] :
    ∃ (b : Kˣ)
      (u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1),
      (∀ γ : K ≃ₐ[F] K, algebraMap K E (γ (b : K)) =
        padicIntToFieldOfMixedChar vE p
          (primeCyclotomicTeichmullerCharacter F K p γ : ℤ_[p]) *
            algebraMap K E (b : K)) ∧
      (principalUnitLogOfMixedChar vE p u).toAdd = algebraMap K E (b : K) ∧
      (∀ δ : E ≃ₐ[L] E,
        δ (((u : (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
          (completeDVFOfWithZeroValuation vE).valuationSubring) : E) =
        (((principalUnitPadicPowOfMixedChar vE p
          (primeCyclotomicTeichmullerCharacter L E p δ : ℤ_[p]) u :
          (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
          (completeDVFOfWithZeroValuation vE).valuationSubring) : E)) ∧
      ∀ c : Kˣ,
        (∀ γ : K ≃ₐ[F] K, algebraMap K E (γ (c : K)) =
          padicIntToFieldOfMixedChar vE p
            (primeCyclotomicTeichmullerCharacter F K p γ : ℤ_[p]) *
              algebraMap K E (c : K)) →
        (∃ z : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1,
          (principalUnitLogOfMixedChar vE p z).toAdd = algebraMap K E (c : K)) →
        (ofWithZeroValuation vE).val (Units.map (algebraMap K E).toMonoidHom b) ≤
          (ofWithZeroValuation vE).val (Units.map (algebraMap K E).toMonoidHom c)

MixedCharCyclotomicEigenUnit.lean

Module documentation

A minimal cyclotomic logarithm with an eigenunit preimage

valuation_algEquiv_eq_of_complete

exists_minimal_cyclotomic_log_eigenunit

Module documentation

A minimal cyclotomic logarithm with an eigenunit preimage

Declarations

valuation_algEquiv_eq_of_complete

exists_minimal_cyclotomic_log_eigenunit