Module

DyadicModTwo.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.DyadicModTwo

1 declaration indexed from sourceView source ↗

Module documentation

Nontrivial dyadic mod-two action

The dyadic detection result retained from the earlier manuscript. A quadratic norm outside the two square classes gives a nonsquare norm in the extension. Trivial conjugation on the actual mod-two abelianization would make every norm a square by Kummer theory, which is a contradiction.

Imports6

Imported by2

theorem

dyadic_mod_two

L31 ↗

Yamaguchi26AbfaithfulGalois.dyadic_mod_two

Documentation

Dyadic mod-two detection: a quadratic extension acts nontrivially on G_Lᵃᵇ/2 in residue characteristic two.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian
universe u v

Lean source · statement

theorem dyadic_mod_two
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [CharZero K] (base : HenselianDVF.{u, v} K)
    [CharP base.residueField 2]
    (hdegree : Module.finrank K L = 2) :
    ∃ τ : Gal(L/K), τ ≠ 1 ∧
      ∃ z : abelianModPower Gal(AlgebraicClosure L/L) 2,
        relativeGaloisAbelianModPowerTransform K L 2 τ z ≠ z

Module documentation

Nontrivial dyadic mod-two action

Declarations

dyadic_mod_two