Module

ValuativeExtension.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ValuativeExtension

3 declarations indexed from sourceView source ↗

Module documentation

Valuative extensions

Records when the valuation ring of an extension field is integral over the base valuation ring, the hypothesis needed to restrict field norms integrally.

Imports3

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.Valuation.Extension
Mathlib.Topology.Algebra.Valued.ValuativeRel

Imported by3

theorem

of_hasExtension

Valuation.IsNontrivial.of_hasExtension

Documentation

A nontrivial valuation stays nontrivial after passing to any valuation which extends it along an algebra map.

Source context 1 command

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

namespace Valuation

Lean source · statement

theorem IsNontrivial.of_hasExtension
    {R A ΓR ΓA : Type*}
    [CommRing R] [Ring A]
    [LinearOrderedCommMonoidWithZero ΓR]
    [LinearOrderedCommMonoidWithZero ΓA]
    [Algebra R A]
    (vR : Valuation R ΓR) (vA : Valuation A ΓA)
    [vR.IsNontrivial] [vR.HasExtension vA] :
    vA.IsNontrivial

class

ValuativeExtension

LocalFieldTheory.ValuativeExtension

Documentation

A valued extension whose valuation integer ring in L is integral over the base integer ring.

This is the algebraic input used to restrict field norms to valuation integer rings.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
open scoped ValuativeRel

Lean source · full declaration

class ValuativeExtension (K : Type u) (L : Type v) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L] : Prop where
  /-- Every target valuation integer is integral over the base valuation
  integers. -/
  integer_isIntegral : ∀ x : 𝒪[L], IsIntegral 𝒪[K] (x : L)

instance

valuativeExtensionOfIsIntegralClosure

LocalFieldTheory.valuativeExtensionOfIsIntegralClosure

Documentation

An integral-closure identification of valuation rings makes the target valuation an extension of the base valuation.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
open scoped ValuativeRel

Lean source · full declaration

instance valuativeExtensionOfIsIntegralClosure
    (K : Type u) (L : Type v) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L] [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    ValuativeExtension K L where
  integer_isIntegral x :=
    (IsIntegralClosure.isIntegral_iff (A := 𝒪[L]) (R := 𝒪[K]) (B := L)).2 ⟨x, rfl⟩