NYLL
Module

MixedCharCyclotomicDetection.lean

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

Module documentation

Nontrivial H¹ action from both cyclotomic branches

The positive branch descends the actual invariant Kummer trace. Triviality of the lower action would fix that same trace, contradicting its construction. The other branch uses the logarithmic minimum argument. The common last root level and the branch split are generated internally.

Imports10
Imported by2

Declarations

theorem

characterAction_fixed_of_trivial_lowerH1Action

L35 ↗
ClassFieldTower.Martinet.Shafarevich.characterAction_fixed_of_trivial_lowerH1Action
Source context 3 commands

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

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

-- This helper separates character descent from the two-cyclotomic-field setup.
-- Reversing the action uses its proved group law, not a comparison of chosen lifts.
Lean source · statement
theorem characterAction_fixed_of_trivial_lowerH1Action
    {F K Ω : Type*} [Field F] [Field K] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
    (E : IntermediateField K Ω) [FiniteDimensional K E] [Normal K E]
    (n : ℕ) (hdegree : (Module.finrank K E).Coprime n)
    (f : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))
    (hinv : ∀ δ : Gal(E/K), absoluteContinuousCharacterAction (K := E)
      (A := Multiplicative (ZMod n)) δ.toRingEquiv f = f)
    (τ : Gal(K/F)) (υ : E ≃+* E)
    (hυ : ∀ x : K, υ (algebraMap K E x) = algebraMap K E (τ x))
    (hτ : relativeGaloisH1Action (n := n) F K τ = 1) :
    absoluteContinuousCharacterAction (K := E)
      (A := Multiplicative (ZMod n)) υ f = f
theorem

exists_nontrivial_relativeH1Action_of_prime_degree_cyclotomic_tower

L73 ↗
ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_relativeH1Action_of_prime_degree_cyclotomic_tower
Documentation

For the actual prime-degree normal extension, cyclotomic fields and complete extension valuation, some positive p-power H¹ action is nontrivial. The last root level and both sides of the roots-downstairs split are internal.

Source context 3 commands

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

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

-- This helper separates character descent from the two-cyclotomic-field setup.
-- Reversing the action uses its proved group law, not a comparison of chosen lifts.
Lean source · statement
theorem exists_nontrivial_relativeH1Action_of_prime_degree_cyclotomic_tower
    {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] [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]
    [hres : CharP (IsLocalRing.ResidueField vE.valuationSubring) p]
    [IsCyclotomicExtension {p} F L] [IsCyclotomicExtension {p} K E]
    (hdegree : Module.finrank F K = p) :
    ∃ s : ℕ, 1 ≤ s ∧ ∃ τ : Gal(K/F),
      relativeGaloisH1Action (n := p ^ s) F K τ ≠ 1

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