Module

MixedCharPrimeToCyclotomicDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharPrimeToCyclotomicDetection

2 declarations indexed from sourceView source ↗

Module documentation

Detection for prime degrees outside the dyadic quadratic case

The normal-basis character vector and its principal-unit logarithm are noninvariant under an automorphism outside the cyclotomic restriction kernel. Trivial lower mod-p cohomology would make all action differences p-divisible. Averaging, or odd-prime binomial divisibility, and the log bound force the same vector to be invariant, a contradiction.

Imports9

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharCyclotomicLogAction
Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharCharacterLogRigidity
Nyll.Yamaguchi26AbfaithfulGalois.Analytic.MixedCharSubgroupCharacterLogVector
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianAutomorphismValuation
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NormalCyclotomicTower
Mathlib.Algebra.Algebra.Tower
Mathlib.FieldTheory.SeparableDegree
Mathlib.GroupTheory.OrderOfElement
Mathlib.SetTheory.Cardinal.NatCard

Imported by2

theorem

exists_nontrivial_relativeH1Action_of_cyclotomic_tower

L36 ↗

ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_relativeH1Action_of_cyclotomic_tower

Documentation

The actual mod-p action is nontrivial for a prime-degree Galois extension outside the dyadic quadratic case, after adjoining the p-th roots. All group orders, valuation invariance and character comparisons are constructed from the field tower.

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

Lean source · statement

theorem exists_nontrivial_relativeH1Action_of_cyclotomic_tower
    {F K Ω : Type*} [Field F] [Field K] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K] [IsGalois F K]
    (E : IntermediateField K Ω) [Algebra F E] [IsScalarTower F K E]
    (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 r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [hres : CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    [IsCyclotomicExtension {p} K E]
    (hprime : r ≠ p ∨ p ≠ 2) (hdegree : Module.finrank F K = r) :
    ∃ τ : Gal(K/F), relativeGaloisH1Action (n := p) F K τ ≠ 1

theorem

exists_nontrivial_relativeH1Action_of_primeTo_cyclotomic_tower

L118 ↗

ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_relativeH1Action_of_primeTo_cyclotomic_tower