NYLL
Module

MixedCharCompleteDetection.lean

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

Module documentation

Faithful prime-power H¹ action over a complete mixed-characteristic base

Both cyclotomic fields are constructed in an actual algebraic closure. A complete integer-valued extension valuation and its residue characteristic are generated from the base. The two-branch detection then gives a nontrivial action, which is faithful because the original Galois group has prime order.

Imports9
Imported by2

Declarations

theorem

exists_nontrivial_H1Action_in_closure

L37 ↗
ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_H1Action_in_closure
Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- The only new data instances are the single composite F-algebra on E and
-- its F/K/E tower. Constructing L inside E reuses canonical intermediate-field
-- instances; no F-algebra on the ambient closure is installed. The peak is
-- fifteen field/algebra/tower structures. Residue-field transport stays in
-- the separate two-field valuation source.
-- Keep the field construction abstract in Ω. On the concrete AlgebraicClosure K,
-- its lower-base algebra instance would introduce a second F-module on E.
Lean source · statement
theorem exists_nontrivial_H1Action_in_closure
    {F K Ω : Type*} [Field F] [Field K] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [Normal F K] [CharZero F]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete vF] (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    (hdegree : Module.finrank F K = p) :
    ∃ s : ℕ, 1 ≤ s ∧ ∃ τ : Gal(K/F),
      relativeGaloisH1Action (n := p ^ s) F K τ ≠ 1
theorem

exists_faithful_relativeH1Action_of_complete_mixedChar_prime_degree

L75 ↗
ClassFieldTower.Martinet.Shafarevich.exists_faithful_relativeH1Action_of_complete_mixedChar_prime_degree
Documentation

A prime-degree Galois extension of a complete discretely valued field of mixed characteristic has faithful H¹ action at some positive p-power level. No auxiliary field, extension valuation, root bound or action comparison is an input to this theorem.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- The only new data instances are the single composite F-algebra on E and
-- its F/K/E tower. Constructing L inside E reuses canonical intermediate-field
-- instances; no F-algebra on the ambient closure is installed. The peak is
-- fifteen field/algebra/tower structures. Residue-field transport stays in
-- the separate two-field valuation source.
-- Keep the field construction abstract in Ω. On the concrete AlgebraicClosure K,
-- its lower-base algebra instance would introduce a second F-module on E.
Lean source · statement
theorem exists_faithful_relativeH1Action_of_complete_mixedChar_prime_degree
    {F K : Type*} [Field F] [Field K] [Algebra F K] [IsGalois F K] [CharZero F]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete vF]
    (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    (hdegree : Module.finrank F K = p) :
    ∃ s : ℕ, 1 ≤ s ∧ Function.Injective (relativeGaloisH1Action (n := p ^ s) F K)

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