Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharMovingRootDetection

Module documentation

Detection when a prime-power root does not descend

The upper extension is Galois by its actual splitting-field construction. A root outside the lower cyclotomic field is moved by a Galois automorphism. Its restriction cannot act trivially on H¹, since the logarithmic minimum argument would then fix that same root.

theorem

exists_nontrivial_relativeH1Action_of_roots_not_in_cyclotomic_base

L32 ↗

ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_relativeH1Action_of_roots_not_in_cyclotomic_base

Documentation

If the selected prime-power roots do not all descend to the lower cyclotomic field, the actual lower H¹ action is nontrivial.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory

-- The supplied data are the same thirteen structures as in RootFixing.
-- The proof adds only finite-dimensionality, normality, characteristic, and
-- Galois propositions. In particular it introduces no alternate algebra tower.

Lean source · statement

theorem exists_nontrivial_relativeH1Action_of_roots_not_in_cyclotomic_base
    {F K L Ω : Type*} [Field F] [Field K] [Field L] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
    (E : IntermediateField K Ω)
    [Algebra F L] [Algebra F E] [Algebra L E]
    [IsScalarTower F K E] [IsScalarTower F L E]
    [FiniteDimensional F K] [Normal F K]
    (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 L] [IsCyclotomicExtension {p} K E]
    (s : ℕ) (hmu : (primitiveRoots (p ^ (s + 1)) E).Nonempty)
    (hnot : ¬ ∀ ζ : E, ζ ^ (p ^ (s + 1)) = 1 →
      ζ ∈ Set.range (algebraMap L E)) :
    ∃ τ : Gal(K/F), relativeGaloisH1Action (n := p ^ (s + 1)) F K τ ≠ 1

Module documentation

Detection when a prime-power root does not descend

Declarations

exists_nontrivial_relativeH1Action_of_roots_not_in_cyclotomic_base