Module

StableGalois.lean

Nyll.ValuedFieldTheory.Valuation.Completion.StableGalois

8 declarations indexed from sourceView source ↗

Module documentation

Completion of a finite Galois extension with invariant valuation

Every relative automorphism preserving the valuation extends to the completion. If all automorphisms preserve the valuation class, comparison with the canonical surjective tensor map shows that the degree is unchanged and that every completion automorphism is obtained in this way.

Imports3

Nyll.ValuedFieldTheory.Valuation.Completion.EquivariantMap
Nyll.ValuedFieldTheory.Valuation.Completion.DVFTensorMap
Mathlib.FieldTheory.Galois.Basic

Imported by2

instance

stableCompletionAlgebra

L26 ↗

ValuationTheory.DiscreteValuationField.DVF.stableCompletionAlgebra

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]

Lean source · statement

instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion

def

completionAlgEquiv

L31 ↗

ValuationTheory.DiscreteValuationField.DVF.completionAlgEquiv

Documentation

Extend a relative field automorphism preserving the valuation class.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · full declaration

def completionAlgEquiv (τ : Gal(L/K))
    (hτ : target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    Gal(target.valuation.Completion/base.valuation.Completion) where
  __ := completionRingEquiv target target τ.toRingEquiv hτ
  commutes' a := DFunLike.congr_fun
    (completionRingEquiv_comp_completionMap base target target τ hτ) a

theorem

completionAlgEquiv_algebraMap

L39 ↗

ValuationTheory.DiscreteValuationField.DVF.completionAlgEquiv_algebraMap

Documentation

The completed automorphism retains its prescribed action on the original field.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · statement

theorem completionAlgEquiv_algebraMap (τ : Gal(L/K))
    (hτ : target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom))
    (x : L) :
    completionAlgEquiv base target τ hτ (algebraMap L target.valuation.Completion x) =
      algebraMap L target.valuation.Completion (τ x)

theorem

completionAlgEquiv_injective

L47 ↗

ValuationTheory.DiscreteValuationField.DVF.completionAlgEquiv_injective

Documentation

Distinct original automorphisms induce distinct completed automorphisms.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · full declaration

theorem completionAlgEquiv_injective
    (hstable : ∀ τ : Gal(L/K),
      target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    Function.Injective (fun τ => completionAlgEquiv base target τ (hstable τ)) := by
  intro τ σ h
  apply AlgEquiv.ext
  intro x
  apply (algebraMap L target.valuation.Completion).injective
  exact (completionAlgEquiv_algebraMap base target τ (hstable τ) x).symm.trans
    ((DFunLike.congr_fun h (algebraMap L target.valuation.Completion x)).trans
      (completionAlgEquiv_algebraMap base target σ (hstable σ) x))

theorem

finrank_completion_le

L60 ↗

ValuationTheory.DiscreteValuationField.DVF.finrank_completion_le

Documentation

The degree cannot increase on completing an extension of discrete valued fields.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · statement

theorem finrank_completion_le [FiniteDimensional K L] :
    Module.finrank base.valuation.Completion target.valuation.Completion ≤
      Module.finrank K L

theorem

finrank_completion_eq_of_galois_stable

L69 ↗

ValuationTheory.DiscreteValuationField.DVF.finrank_completion_eq_of_galois_stable

Documentation

An invariant prolongation preserves the degree of a finite Galois extension.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · statement

theorem finrank_completion_eq_of_galois_stable [FiniteDimensional K L] [IsGalois K L]
    (hstable : ∀ τ : Gal(L/K),
      target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    Module.finrank base.valuation.Completion target.valuation.Completion =
      Module.finrank K L

theorem

completion_isGalois_of_stable

L86 ↗

ValuationTheory.DiscreteValuationField.DVF.completion_isGalois_of_stable

Documentation

Completing at an invariant prolongation preserves the Galois property.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · statement

theorem completion_isGalois_of_stable [FiniteDimensional K L] [IsGalois K L]
    (hstable : ∀ τ : Gal(L/K),
      target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    IsGalois base.valuation.Completion target.valuation.Completion

theorem

completionAlgEquiv_surjective

L102 ↗

ValuationTheory.DiscreteValuationField.DVF.completionAlgEquiv_surjective

Documentation

Every completed automorphism extends an original automorphism when the prolongation is invariant under the finite Galois group.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [base.valuation.HasExtension target.valuation]
local instance stableCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target

Lean source · full declaration

theorem completionAlgEquiv_surjective [FiniteDimensional K L] [IsGalois K L]
    (hstable : ∀ τ : Gal(L/K),
      target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    Function.Surjective (fun τ => completionAlgEquiv base target τ (hstable τ)) := by
  have : FiniteDimensional base.valuation.Completion target.valuation.Completion :=
    completion_finiteDimensional base target
  have : IsGalois base.valuation.Completion target.valuation.Completion :=
    completion_isGalois_of_stable base target hstable
  exact ((completionAlgEquiv_injective base target hstable).bijective_of_nat_card_le
    (by rw [IsGalois.card_aut_eq_finrank, IsGalois.card_aut_eq_finrank,
      finrank_completion_eq_of_galois_stable base target hstable])).2

Module documentation

Completion of a finite Galois extension with invariant valuation

Declarations