Module

CyclotomicCompletion.lean

Nyll.ValuedFieldTheory.Valuation.Completion.CyclotomicCompletion

3 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic extensions after completion

The completion of a finite extension is generated by the original field. The canonical completion algebra preserves cyclotomic extensions.

Imports3

Nyll.ValuedFieldTheory.Valuation.Completion.DVFTensorMap
Mathlib.NumberTheory.Cyclotomic.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

instance

cyclotomicCompletionAlgebra

L29 ↗

ValuationTheory.DiscreteValuationField.DVF.cyclotomicCompletionAlgebra

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
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 cyclotomicCompletionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion

theorem

completion_adjoin_range_eq_top

L34 ↗

ValuationTheory.DiscreteValuationField.DVF.completion_adjoin_range_eq_top

Documentation

A finite extension completion is generated by the original extension field.

Source context 5 commands

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

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

Lean source · statement

theorem completion_adjoin_range_eq_top [FiniteDimensional K L] :
    Algebra.adjoin base.valuation.Completion
      (Set.range (algebraMap L target.valuation.Completion)) = ⊤

theorem

completion_isCyclotomicExtension

L52 ↗

ValuationTheory.DiscreteValuationField.DVF.completion_isCyclotomicExtension

Documentation

Completion preserves a cyclotomic extension with its actual completion algebra.

Source context 5 commands

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

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

Lean source · statement

theorem completion_isCyclotomicExtension (n : ℕ) [NeZero n]
    [IsCyclotomicExtension {n} K L] :
    IsCyclotomicExtension {n} base.valuation.Completion target.valuation.Completion

Module documentation

Cyclotomic extensions after completion

Declarations

cyclotomicCompletionAlgebra

completion_adjoin_range_eq_top

completion_isCyclotomicExtension