Module

Subpadic.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.Subpadic

1 declaration indexed from sourceView source ↗

Module documentation

Abelian faithfulness of sub-p-adic fields

An embedding into an essentially finite-type p-adic extension supplies abelian faithfulness and finiteness of primary roots of unity in every finite extension of the embedded field.

Imports5

Imported by2

theorem

subpadic_isAbFaithful_and_finite_roots

L28 ↗

Yamaguchi26AbfaithfulGalois.subpadic_isAbFaithful_and_finite_roots

Documentation

Sub-p-adic fields have a mixed-characteristic discrete valuation and finite primary roots in all finite extensions. The embedding is the sole sub-p-adic datum.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
universe u v

Lean source · statement

theorem subpadic_isAbFaithful_and_finite_roots
    (p : ℕ) [Fact p.Prime] (K : Type u) (E : Type v)
    [Field K] [Field E] [Algebra (Padic p) E] [Algebra.EssFiniteType (Padic p) E]
    (f : K →+* E) :
    IsAbFaithful Gal(AlgebraicClosure K/K) ∧
      ∀ (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L],
        ∀ (ℓ : ℕ) [Fact ℓ.Prime], Finite (CommGroup.primaryComponent Lˣ ℓ)

Module documentation

Abelian faithfulness of sub-p-adic fields

Declarations

subpadic_isAbFaithful_and_finite_roots