NYLL
Module

DegreeNormTrace.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DegreeNormTrace
5 declarations indexed from sourceView source ↗

Module documentation

Compatibility of local degree, norm, and trace

The canonical decomposition of the completion tensor-product decomposition gives the sum of the local degrees and the product/sum formulas for norm and trace. Since the global norm and trace lie in K, their Lean statements are mapped into K_v.

Imports3
Imported by4

Declarations

theorem

completionModuleFinite

L34 ↗
AlgebraicNumberTheory.Valuations.completionModuleFinite
Documentation

Every local completion is finite-dimensional over K_v. This is derived from the completion tensor-product decomposition by projecting from its finite product.

Source context 6 commands

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

noncomputable section
open scoped BigOperators TensorProduct
open ValuationTheory.Completion
namespace AlgebraicNumberTheory
namespace Valuations
universe u v
Lean source · full declaration
theorem completionModuleFinite
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) :
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    Module.Finite vK.Completion w.1.Completion := by
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : Module.Finite vK.Completion (vK.Completion ⊗[K] L) :=
    inferInstance
  let : Module.Finite vK.Completion
      (∀ w : AbsoluteValueExtension vK L, w.1.Completion) :=
    Module.Finite.equiv (completionTensorDecomposition_left vK hvK).toLinearEquiv
  exact moduleFiniteOfPi
    (fun w : AbsoluteValueExtension vK L ↦ w.1.Completion) w
theorem

completionDegreeNormTrace_degree

L53 ↗
AlgebraicNumberTheory.Valuations.completionDegreeNormTrace_degree
Documentation

the local degree, norm, and trace formulas, degree formula.

Source context 6 commands

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

noncomputable section
open scoped BigOperators TensorProduct
open ValuationTheory.Completion
namespace AlgebraicNumberTheory
namespace Valuations
universe u v
Lean source · full declaration
theorem completionDegreeNormTrace_degree
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial) :
    letI := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
    letI : ∀ w : AbsoluteValueExtension vK L,
        Algebra vK.Completion w.1.Completion :=
      fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w : AbsoluteValueExtension vK L,
        Module.Finite vK.Completion w.1.Completion :=
      fun w ↦ completionModuleFinite vK hvK w
    Module.finrank K L =
      ∑ w : AbsoluteValueExtension vK L,
        Module.finrank vK.Completion w.1.Completion := by
  let := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Finite vK.Completion w.1.Completion :=
    fun w ↦ completionModuleFinite vK hvK w
  exact baseChange_pi_finrank_eq_sum
    (fun w : AbsoluteValueExtension vK L ↦ w.1.Completion)
    (completionTensorDecomposition_left vK hvK)
theorem

completionDegreeNormTrace_norm

L79 ↗
AlgebraicNumberTheory.Valuations.completionDegreeNormTrace_norm
Documentation

the local degree, norm, and trace formulas, norm formula, written in K_v.

Source context 6 commands

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

noncomputable section
open scoped BigOperators TensorProduct
open ValuationTheory.Completion
namespace AlgebraicNumberTheory
namespace Valuations
universe u v
Lean source · full declaration
theorem completionDegreeNormTrace_norm
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial) (x : L) :
    letI := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
    letI : ∀ w : AbsoluteValueExtension vK L,
        Algebra vK.Completion w.1.Completion :=
      fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w : AbsoluteValueExtension vK L,
        Module.Finite vK.Completion w.1.Completion :=
      fun w ↦ completionModuleFinite vK hvK w
    algebraMap K vK.Completion (Algebra.norm K x) =
      ∏ w : AbsoluteValueExtension vK L,
        Algebra.norm vK.Completion
          (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x) := by
  let := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Finite vK.Completion w.1.Completion :=
    fun w ↦ completionModuleFinite vK hvK w
  simpa using baseChange_pi_norm_eq_prod
    (fun w : AbsoluteValueExtension vK L ↦ w.1.Completion)
    (completionTensorDecomposition_left vK hvK) x
theorem

completionDegreeNormTrace_trace

L106 ↗
AlgebraicNumberTheory.Valuations.completionDegreeNormTrace_trace
Documentation

the local degree, norm, and trace formulas, trace formula, written in K_v.

Source context 6 commands

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

noncomputable section
open scoped BigOperators TensorProduct
open ValuationTheory.Completion
namespace AlgebraicNumberTheory
namespace Valuations
universe u v
Lean source · full declaration
theorem completionDegreeNormTrace_trace
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial) (x : L) :
    letI := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
    letI : ∀ w : AbsoluteValueExtension vK L,
        Algebra vK.Completion w.1.Completion :=
      fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w : AbsoluteValueExtension vK L,
        Module.Finite vK.Completion w.1.Completion :=
      fun w ↦ completionModuleFinite vK hvK w
    algebraMap K vK.Completion (Algebra.trace K L x) =
      ∑ w : AbsoluteValueExtension vK L,
        Algebra.trace vK.Completion w.1.Completion
          (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x) := by
  let := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Finite vK.Completion w.1.Completion :=
    fun w ↦ completionModuleFinite vK hvK w
  simpa using baseChange_pi_trace_eq_sum
    (fun w : AbsoluteValueExtension vK L ↦ w.1.Completion)
    (completionTensorDecomposition_left vK hvK) x
theorem

completionDegreeNormTrace

L134 ↗
AlgebraicNumberTheory.Valuations.completionDegreeNormTrace
Documentation

the local degree, norm, and trace formulas. The degree, norm, and trace formulas obtained simultaneously from the canonical decomposition of the completion tensor-product decomposition.

Source context 6 commands

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

noncomputable section
open scoped BigOperators TensorProduct
open ValuationTheory.Completion
namespace AlgebraicNumberTheory
namespace Valuations
universe u v
Lean source · full declaration
theorem completionDegreeNormTrace
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial) :
    letI := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
    letI : ∀ w : AbsoluteValueExtension vK L,
        Algebra vK.Completion w.1.Completion :=
      fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
    letI : ∀ w : AbsoluteValueExtension vK L,
        Module.Finite vK.Completion w.1.Completion :=
      fun w ↦ completionModuleFinite vK hvK w
    (Module.finrank K L =
      ∑ w : AbsoluteValueExtension vK L,
        Module.finrank vK.Completion w.1.Completion) ∧
    (∀ x : L,
      algebraMap K vK.Completion (Algebra.norm K x) =
        ∏ w : AbsoluteValueExtension vK L,
          Algebra.norm vK.Completion
            (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x)) ∧
    (∀ x : L,
      algebraMap K vK.Completion (Algebra.trace K L x) =
        ∑ w : AbsoluteValueExtension vK L,
          Algebra.trace vK.Completion w.1.Completion
            (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x)) := by
  let := completionTensorDecomposition_extensionFintype (K := K) (L := L) vK hvK
  let : ∀ w : AbsoluteValueExtension vK L,
      Algebra vK.Completion w.1.Completion :=
    fun w ↦ AbsoluteValue.completionAlgebra vK w.1 w.2
  let : ∀ w : AbsoluteValueExtension vK L,
      Module.Finite vK.Completion w.1.Completion :=
    fun w ↦ completionModuleFinite vK hvK w
  exact ⟨completionDegreeNormTrace_degree (K := K) (L := L) vK hvK,
    fun x ↦ completionDegreeNormTrace_norm (K := K) (L := L) vK hvK x,
    fun x ↦ completionDegreeNormTrace_trace (K := K) (L := L) vK hvK x⟩

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