NYLL
Module

MixedCharCyclotomicLogDifference.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharCyclotomicLogDifference
2 declarations indexed from sourceView source ↗

Module documentation

Logarithmic action differences from trivial mod-p cohomology

The actual Kummer power witness gives a principal-unit logarithm after subtracting the finite exponent. The exponent agrees modulo p with the specified primitive-root character, so a p-adic power corrects that logarithm to the actual character difference. No p-primary degree assumption is made on the lower extension.

Imports4
Imported by2

Declarations

theorem

log_character_difference_of_power_witness

L29 ↗
ClassFieldTower.Martinet.Shafarevich.log_character_difference_of_power_witness
Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation

-- Keep the analytic correction over an abstract field. This prevents the
-- intermediate-field scalar tower from being searched in each log identity.
Lean source · statement
theorem log_character_difference_of_power_witness
    {F E : Type*} [Field F] [Field E] [Algebra F E] [CharZero E]
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    {ζ : E} (hζ : IsPrimitiveRoot ζ p)
    (u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1)
    (υ : Gal(E/F)) (hval : ∀ x : E, vE (υ x) = vE x)
    (a : ℕ) (ha : a < p) (hroot : υ ζ = ζ ^ a) (y : Eˣ)
    (hy : Units.map υ.toRingEquiv.toMonoidHom
        (CompleteDVF.valuationSubringUnitsToFieldUnits (completeDVFOfWithZeroValuation vE)
          (u : (completeDVFOfWithZeroValuation vE).valuationSubringˣ)) /
        (CompleteDVF.valuationSubringUnitsToFieldUnits (completeDVFOfWithZeroValuation vE)
          (u : (completeDVFOfWithZeroValuation vE).valuationSubringˣ)) ^ a = y ^ (p ^ 1)) :
    ∃ z : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1,
      υ (principalUnitLogOfMixedChar vE p u).toAdd -
        padicIntToFieldOfMixedChar vE p
          (primitiveRootTeichmullerCharacter F p hζ υ : ℤ_[p]) *
            (principalUnitLogOfMixedChar vE p u).toAdd =
        (p : E) * (principalUnitLogOfMixedChar vE p z).toAdd
theorem

exists_principalUnit_log_character_difference_of_trivial_lowerH1Action

L80 ↗
ClassFieldTower.Martinet.Shafarevich.exists_principalUnit_log_character_difference_of_trivial_lowerH1Action
Documentation

Trivial mod-p action produces a p-divisible character difference inside the actual principal-unit logarithm image.

Source context 4 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation

-- Keep the analytic correction over an abstract field. This prevents the
-- intermediate-field scalar tower from being searched in each log identity.
variable {F K Ω : Type*} [Field F] [Field K] [Field Ω]
  [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
Lean source · statement
theorem exists_principalUnit_log_character_difference_of_trivial_lowerH1Action
    (E : IntermediateField K Ω) [Algebra F E]
    (vE : _root_.Valuation E (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vE]
    (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K E]
    [CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    {ζ : E} (hζ : IsPrimitiveRoot ζ p)
    (u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1)
    (hueigen : ∀ δ : E ≃ₐ[K] E,
      δ (((u : (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
        (completeDVFOfWithZeroValuation vE).valuationSubring) : E) =
      (((principalUnitPadicPowOfMixedChar vE p
        (primeCyclotomicTeichmullerCharacter K E p δ : ℤ_[p]) u :
          (completeDVFOfWithZeroValuation vE).valuationSubringˣ) :
            (completeDVFOfWithZeroValuation vE).valuationSubring) : E))
    (τ : Gal(K/F)) (υ : Gal(E/F))
    (hυ : ∀ x : K, υ (algebraMap K E x) = algebraMap K E (τ x))
    (hval : ∀ x : E, vE (υ x) = vE x)
    (hτ : relativeGaloisH1Action (n := p) F K τ = 1) :
    ∃ z : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation vE) 1,
      υ (principalUnitLogOfMixedChar vE p u).toAdd -
        padicIntToFieldOfMixedChar vE p
          (primitiveRootTeichmullerCharacter F p hζ υ : ℤ_[p]) *
            (principalUnitLogOfMixedChar vE p u).toAdd =
        (p : E) * (principalUnitLogOfMixedChar vE p z).toAdd

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.