NYLL
Module

RamificationInvariants.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.RamificationInvariants
20 declarations indexed from sourceView source ↗

Module documentation

Canonical ramification invariants

The ramification index and residue degree are the ideal-theoretic invariants of the chosen valuation rings. Every theorem below is stated directly in the ambient valued-extension context; there are no compatibility aliases or extension-marker arguments.

Imports1
Imported by5

Declarations

theorem

degree_eq_ramificationIndex_mul_residueDegree

L36 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.degree_eq_ramificationIndex_mul_residueDegree
Documentation

The local fundamental identity for a finite extension of valuation rings.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem degree_eq_ramificationIndex_mul_residueDegree
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF =
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF *
        ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF
theorem

ramificationIndex_ne_zero

L54 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_ne_zero
Documentation

Establishes the inequality ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF ≠ 0.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem ramificationIndex_ne_zero
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
      base.toDVF target.toDVF ≠ 0
theorem

ramificationIndex_pos

L65 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_pos
Documentation

Establishes the strict bound 0 < ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem ramificationIndex_pos
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    0 < ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
      base.toDVF target.toDVF
theorem

residueDegree_ne_zero

L75 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_ne_zero
Documentation

Establishes the inequality ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF ≠ 0.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem residueDegree_ne_zero
    [Module.Finite base.valuationSubring target.valuationSubring] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
      base.toDVF target.toDVF ≠ 0
theorem

residueDegree_pos

L86 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_pos
Documentation

Establishes the strict bound 0 < ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem residueDegree_pos
    [Module.Finite base.valuationSubring target.valuationSubring] :
    0 < ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
      base.toDVF target.toDVF
theorem

ramificationIndex_le_degree

L98 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_le_degree
Documentation

Proves the bound ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF ≤ ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem ramificationIndex_le_degree
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF ≤
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

residueDegree_le_degree

L117 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_le_degree
Documentation

Proves the bound ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF ≤ ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem residueDegree_le_degree
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
        base.toDVF target.toDVF ≤
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

degree_eq_one_iff_ramificationIndex_eq_one_and_residueDegree_eq_one

L147 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.degree_eq_one_iff_ramificationIndex_eq_one_and_residueDegree_eq_one
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF = 1 by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = 1 ∧ ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = 1.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem degree_eq_one_iff_ramificationIndex_eq_one_and_residueDegree_eq_one
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.degree
          base.toDVF target.toDVF = 1 ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF = 1 ∧
        ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF = 1
theorem

residueDegree_eq_degree_of_ramificationIndex_eq_one

L175 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_eq_degree_of_ramificationIndex_eq_one
Documentation

Establishes the identity ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem residueDegree_eq_degree_of_ramificationIndex_eq_one
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (h :
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF = 1) :
    ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
        base.toDVF target.toDVF =
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

ramificationIndex_eq_degree_of_residueDegree_eq_one

L192 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_eq_degree_of_residueDegree_eq_one
Documentation

Establishes the identity ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem ramificationIndex_eq_degree_of_residueDegree_eq_one
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (h :
      ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
        base.toDVF target.toDVF = 1) :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF =
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

isUnramified_iff_ramificationIndex_eq_one

L210 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.isUnramified_iff_ramificationIndex_eq_one
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.IsUnramified base.toDVF target.toDVF by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = 1.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem isUnramified_iff_ramificationIndex_eq_one :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsUnramified
          base.toDVF target.toDVF ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF = 1
theorem

isTotallyRamified_iff_residueDegree_eq_one

L223 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.isTotallyRamified_iff_residueDegree_eq_one
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyRamified base.toDVF target.toDVF by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = 1.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem isTotallyRamified_iff_residueDegree_eq_one :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyRamified
          base.toDVF target.toDVF ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
        base.toDVF target.toDVF = 1
theorem

degree_eq_ramificationIndex_mul_residueDegree_of_finite_separable

L238 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.degree_eq_ramificationIndex_mul_residueDegree_of_finite_separable
Documentation

Establishes the identity ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF * ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem degree_eq_ramificationIndex_mul_residueDegree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF =
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF *
        ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF
theorem

isDefectless_of_finite_separable

L252 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.isDefectless_of_finite_separable
Documentation

A finite separable extension of the discrete valued fields is defectless.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem isDefectless_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsDefectless
      base.toDVF target.toDVF
theorem

ramificationIndex_le_degree_of_finite_separable

L264 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_le_degree_of_finite_separable
Documentation

Proves the bound ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF ≤ ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem ramificationIndex_le_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        base.toDVF target.toDVF ≤
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

residueDegree_le_degree_of_finite_separable

L281 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_le_degree_of_finite_separable
Documentation

Proves the bound ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF ≤ ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem residueDegree_le_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
        base.toDVF target.toDVF ≤
      ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        base.toDVF target.toDVF
theorem

ramificationIndex_eq_one_iff_residueDegree_eq_degree_of_finite_separable

L302 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_eq_one_iff_residueDegree_eq_degree_of_finite_separable
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = 1 by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem ramificationIndex_eq_one_iff_residueDegree_eq_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF = 1 ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF =
        ValuationTheory.DiscreteValuationField.ValuedExtension.degree
          base.toDVF target.toDVF
theorem

residueDegree_eq_one_iff_ramificationIndex_eq_degree_of_finite_separable

L330 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.residueDegree_eq_one_iff_ramificationIndex_eq_degree_of_finite_separable
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = 1 by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem residueDegree_eq_one_iff_ramificationIndex_eq_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF = 1 ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF =
        ValuationTheory.DiscreteValuationField.ValuedExtension.degree
          base.toDVF target.toDVF
theorem

isUnramified_iff_residueDegree_eq_degree_of_finite_separable

L361 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.isUnramified_iff_residueDegree_eq_degree_of_finite_separable
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.IsUnramified base.toDVF target.toDVF by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem isUnramified_iff_residueDegree_eq_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsUnramified
          base.toDVF target.toDVF ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          base.toDVF target.toDVF =
        ValuationTheory.DiscreteValuationField.ValuedExtension.degree
          base.toDVF target.toDVF
theorem

isTotallyRamified_iff_ramificationIndex_eq_degree_of_finite_separable

L379 ↗
LocalFieldTheory.DiscreteValuationField.ValuedExtension.isTotallyRamified_iff_ramificationIndex_eq_degree_of_finite_separable
Documentation

Characterizes ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyRamified base.toDVF target.toDVF by the equivalent condition ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex base.toDVF target.toDVF = ValuationTheory.DiscreteValuationField.ValuedExtension.degree base.toDVF target.toDVF.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
Lean source · statement
theorem isTotallyRamified_iff_ramificationIndex_eq_degree_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyRamified
          base.toDVF target.toDVF ↔
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          base.toDVF target.toDVF =
        ValuationTheory.DiscreteValuationField.ValuedExtension.degree
          base.toDVF target.toDVF

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