Module

Different.lean

Nyll.ValuedFieldTheory.Ramification.Different

32 declarations indexed from sourceView source ↗

Module documentation

Different and codifferent for valued finite extensions

This file specializes mathlib's Dedekind-domain different ideal to complete DVF valuation rings. The ideal itself remains mathlib's differentIdeal; the extra API here connects it to the chosen valuation rings, the codifferent, and the local unramified criterion.

Imports2

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Core
Mathlib.RingTheory.DedekindDomain.Different

Imported by2

def

codifferentSubmodule

L42 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.codifferentSubmodule

Documentation

The codifferent submodule of the valuation ring extension, i.e. the trace-dual of the target valuation ring.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

def codifferentSubmodule
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    Submodule target.valuationSubring L

theorem

mem_codifferentSubmodule_iff_trace_mul_integral

L50 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.mem_codifferentSubmodule_iff_trace_mul_integral

Documentation

Trace-dual membership written directly as a trace integrality condition.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem mem_codifferentSubmodule_iff_trace_mul_integral
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    {z : L} :
    z ∈ (codifferentSubmodule base target) ↔
      ∀ a ∈ (1 : Submodule target.valuationSubring L),
        IsIntegral base.valuationSubring (Algebra.trace K L (z * a))

theorem

traceDual_antitone

L68 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.traceDual_antitone

Documentation

The trace-dual operation is antitone. This is the general filtration transfer lemma used to move between ideal/submodule levels and trace bounds.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem traceDual_antitone
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    {I J : Submodule target.valuationSubring L} (hIJ : I ≤ J) :
    Submodule.traceDual base.valuationSubring K J ≤
      Submodule.traceDual base.valuationSubring K I

theorem

trace_mul_mem_integer_range_of_mem_codifferent

L81 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.trace_mul_mem_integer_range_of_mem_codifferent

Documentation

Elements of the codifferent pair integrally with every integral element under the trace form.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem trace_mul_mem_integer_range_of_mem_codifferent
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    {z a : L} (hz : z ∈ (codifferentSubmodule base target))
    (ha : a ∈ (1 : Submodule target.valuationSubring L)) :
    Algebra.trace K L (z * a) ∈
      (algebraMap base.valuationSubring K).range

def

differentIdealOfFiniteSeparable

L95 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdealOfFiniteSeparable

Documentation

The different ideal with the torsion-free certificate supplied by finite separability of complete-DVF extensions.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

def differentIdealOfFiniteSeparable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    Ideal target.valuationSubring

theorem

differentIdealOfFiniteSeparable_eq_differentIdeal

L106 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdealOfFiniteSeparable_eq_differentIdeal

Documentation

The finite-separable different ideal agrees with mathlib's differentIdeal whenever a torsion-free instance is already in scope.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem differentIdealOfFiniteSeparable_eq_differentIdeal
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    (differentIdealOfFiniteSeparable base target) =
      differentIdeal base.valuationSubring target.valuationSubring

theorem

mem_codifferentSubmodule_iff_trace_mul_integral_of_finite_separable

L116 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.mem_codifferentSubmodule_iff_trace_mul_integral_of_finite_separable

Documentation

Finite-separable trace-dual membership written directly as a trace integrality condition.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem mem_codifferentSubmodule_iff_trace_mul_integral_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    {z : L} :
    z ∈ (codifferentSubmodule base target) ↔
      ∀ a ∈ (1 : Submodule target.valuationSubring L),
        IsIntegral base.valuationSubring (Algebra.trace K L (z * a))

theorem

coeSubmodule_differentIdealOfFiniteSeparable_eq_one_div_codifferent

L129 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.coeSubmodule_differentIdealOfFiniteSeparable_eq_one_div_codifferent

Documentation

The local different/codifferent relation in finite separable complete-DVF extensions, using the finite-separable different ideal.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem coeSubmodule_differentIdealOfFiniteSeparable_eq_one_div_codifferent
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    IsLocalization.coeSubmodule L (differentIdealOfFiniteSeparable base target) =
      1 / (codifferentSubmodule base target)

theorem

differentIdeal_ne_bot

L151 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdeal_ne_bot

Documentation

The different ideal is nonzero for finite separable torsion-free valuation ring extensions.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem differentIdeal_ne_bot
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Algebra.IsSeparable
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring)] :
    differentIdeal base.valuationSubring target.valuationSubring ≠ ⊥

theorem

fractionRing_isSeparable_of_finite_separable

L164 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.fractionRing_isSeparable_of_finite_separable

Documentation

The fraction-field extension attached to a finite separable complete-DVF extension is separable. This is kept private to prevent typeclass search from trying the very general FractionRing.liftAlgebra instance globally.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · full declaration

theorem fractionRing_isSeparable_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    letI : FaithfulSMul base.valuationSubring target.valuationSubring :=
      Module.IsTorsionFree.to_faithfulSMul
    letI : FaithfulSMul base.valuationSubring
        (FractionRing target.valuationSubring) := inferInstance
    letI : Algebra (FractionRing base.valuationSubring)
        (FractionRing target.valuationSubring) := FractionRing.liftAlgebra _ _
    Algebra.IsSeparable (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring) := by
  let : FaithfulSMul base.valuationSubring target.valuationSubring :=
    Module.IsTorsionFree.to_faithfulSMul
  let : FaithfulSMul base.valuationSubring
      (FractionRing target.valuationSubring) := inferInstance
  let fracAlgebra : Algebra (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring) := FractionRing.liftAlgebra _ _
  let : SMul (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring) :=
    @Algebra.toSMul _ _ _ _ fracAlgebra
  let : IsScalarTower base.valuationSubring
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring) :=
    FractionRing.isScalarTower_liftAlgebra _ _
  have H : RingHom.comp
      (algebraMap (FractionRing base.valuationSubring)
        (FractionRing target.valuationSubring))
      (FractionRing.algEquiv base.valuationSubring K).symm.toRingEquiv =
        RingHom.comp
          (FractionRing.algEquiv target.valuationSubring L).symm.toRingEquiv
          (algebraMap K L) := by
    apply IsLocalization.ringHom_ext (nonZeroDivisors base.valuationSubring)
    ext a
    simp only [RingHom.coe_comp, RingHom.coe_coe,
      AlgEquiv.coe_ringEquiv, Function.comp_apply,
      AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply
      base.valuationSubring target.valuationSubring L,
      AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
  exact Algebra.IsSeparable.of_equiv_equiv _ _ H

theorem

differentIdealOfFiniteSeparable_ne_bot

L210 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdealOfFiniteSeparable_ne_bot

Documentation

The finite-separable different ideal is nonzero without separately providing the module-finiteness, torsion-free, or fraction-field separability certificates.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem differentIdealOfFiniteSeparable_ne_bot
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    (differentIdealOfFiniteSeparable base target) ≠ ⊥

theorem

coeSubmodule_differentIdeal_eq_one_div_codifferent

L230 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.coeSubmodule_differentIdeal_eq_one_div_codifferent

Documentation

The local different/codifferent relation specialized to the valuation rings.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem coeSubmodule_differentIdeal_eq_one_div_codifferent
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring] :
    IsLocalization.coeSubmodule L
        (differentIdeal base.valuationSubring target.valuationSubring) =
      1 / (codifferentSubmodule base target)

theorem

isIntegral_discriminant_mul_of_mem_codifferent

L250 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.isIntegral_discriminant_mul_of_mem_codifferent

Documentation

Discriminant control for the codifferent: if a K-basis of L is integral over the base valuation ring, then multiplying an element of the codifferent by the discriminant and an integral element gives an integral element.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem isIntegral_discriminant_mul_of_mem_codifferent
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    {ι : Type*} [DecidableEq ι] [Fintype ι]
    {b : Module.Basis ι K L} (hb : ∀ i, IsIntegral base.valuationSubring (b i))
    {a z : L} (ha : a ∈ (1 : Submodule target.valuationSubring L))
    (hz : z ∈ (codifferentSubmodule base target)) :
    IsIntegral base.valuationSubring
      (Algebra.discr K b • a * z)

theorem

isIntegral_discriminant_mul_of_mem_codifferent_of_finite_separable

L266 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.isIntegral_discriminant_mul_of_mem_codifferent_of_finite_separable

Documentation

Finite-separable discriminant control for the codifferent.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem isIntegral_discriminant_mul_of_mem_codifferent_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    {ι : Type*} [DecidableEq ι] [Fintype ι]
    {b : Module.Basis ι K L} (hb : ∀ i, IsIntegral base.valuationSubring (b i))
    {a z : L} (ha : a ∈ (1 : Submodule target.valuationSubring L))
    (hz : z ∈ (codifferentSubmodule base target)) :
    IsIntegral base.valuationSubring
      (Algebra.discr K b • a * z)

theorem

maximalIdeal_not_dvd_differentIdealOfFiniteSeparable_iff_isUnramifiedAt

L282 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_not_dvd_differentIdealOfFiniteSeparable_iff_isUnramifiedAt

Documentation

Finite-separable version of the different/unramified criterion, using differentIdealOfFiniteSeparable to avoid separate torsion-free and fraction-field separability certificates.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem maximalIdeal_not_dvd_differentIdealOfFiniteSeparable_iff_isUnramifiedAt
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    ¬ target.maximalIdeal ∣ (differentIdealOfFiniteSeparable base target) ↔
      Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

maximalIdeal_dvd_differentIdealOfFiniteSeparable_iff_not_isUnramifiedAt

L303 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_dvd_differentIdealOfFiniteSeparable_iff_not_isUnramifiedAt

Documentation

Finite-separable version of the ramified/different divisibility criterion, using differentIdealOfFiniteSeparable.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem maximalIdeal_dvd_differentIdealOfFiniteSeparable_iff_not_isUnramifiedAt
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    target.maximalIdeal ∣ (differentIdealOfFiniteSeparable base target) ↔
      ¬ Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

isUnit_differentIdeal_iff_isUnramifiedAt

L325 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.isUnit_differentIdeal_iff_isUnramifiedAt

Documentation

In a local valuation-ring extension, the different is a unit exactly when the extension is unramified at the target maximal ideal.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem isUnit_differentIdeal_iff_isUnramifiedAt
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Algebra.IsSeparable
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring)] :
    IsUnit (differentIdeal base.valuationSubring target.valuationSubring) ↔
      Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

isUnit_differentIdealOfFiniteSeparable_iff_isUnramifiedAt

L365 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.isUnit_differentIdealOfFiniteSeparable_iff_isUnramifiedAt

Documentation

Finite-separable version of the local unit criterion for the different.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem isUnit_differentIdealOfFiniteSeparable_iff_isUnramifiedAt
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    IsUnit (differentIdealOfFiniteSeparable base target) ↔
      Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

differentIdeal_eq_top_iff_isUnramifiedAt

L386 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdeal_eq_top_iff_isUnramifiedAt

Documentation

States the theorem differentIdeal_eq_top_iff_isUnramifiedAt.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem differentIdeal_eq_top_iff_isUnramifiedAt
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Algebra.IsSeparable
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring)] :
    differentIdeal base.valuationSubring target.valuationSubring = ⊤ ↔
      Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

differentIdealOfFiniteSeparable_eq_top_iff_isUnramifiedAt

L399 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdealOfFiniteSeparable_eq_top_iff_isUnramifiedAt

Documentation

Finite-separable version of the top/different criterion for unramifiedness.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem differentIdealOfFiniteSeparable_eq_top_iff_isUnramifiedAt
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    (differentIdealOfFiniteSeparable base target) = ⊤ ↔
      Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

conductor_mul_differentIdeal_eq_span_derivative

L421 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.conductor_mul_differentIdeal_eq_span_derivative

Documentation

The monogenic different formula: conductor times different is generated by the derivative of the minimal polynomial. This is the Dedekind-domain formula used in Eisenstein computations.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem conductor_mul_differentIdeal_eq_span_derivative
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    (z : target.valuationSubring)
    (hz : Algebra.adjoin K {(algebraMap target.valuationSubring L) z} = ⊤) :
    conductor base.valuationSubring z *
        differentIdeal base.valuationSubring target.valuationSubring =
      Ideal.span
        {Polynomial.aeval z
          (Polynomial.derivative (minpoly base.valuationSubring z))}

theorem

aeval_derivative_mem_differentIdeal

L438 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.aeval_derivative_mem_differentIdeal

Documentation

In a monogenic finite separable extension, the derivative of the minimal polynomial belongs to the different.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem aeval_derivative_mem_differentIdeal
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsIntegralClosure target.valuationSubring base.valuationSubring L]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    (z : target.valuationSubring)
    (hz : Algebra.adjoin K {(algebraMap target.valuationSubring L) z} = ⊤) :
    Polynomial.aeval z
        (Polynomial.derivative (minpoly base.valuationSubring z)) ∈
      differentIdeal base.valuationSubring target.valuationSubring

theorem

conductor_mul_differentIdealOfFiniteSeparable_eq_span_derivative

L453 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.conductor_mul_differentIdealOfFiniteSeparable_eq_span_derivative

Documentation

Monogenic different formula in finite separable complete-DVF extensions, using the finite-separable different ideal.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem conductor_mul_differentIdealOfFiniteSeparable_eq_span_derivative
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (z : target.valuationSubring)
    (hz : Algebra.adjoin K {(algebraMap target.valuationSubring L) z} = ⊤) :
    conductor base.valuationSubring z * (differentIdealOfFiniteSeparable base target) =
      Ideal.span
        {Polynomial.aeval z
          (Polynomial.derivative (minpoly base.valuationSubring z))}

theorem

aeval_derivative_mem_differentIdealOfFiniteSeparable

L472 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.aeval_derivative_mem_differentIdealOfFiniteSeparable

Documentation

In a monogenic finite separable complete-DVF extension, the derivative of the minimal polynomial belongs to the finite-separable different ideal.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem aeval_derivative_mem_differentIdealOfFiniteSeparable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (z : target.valuationSubring)
    (hz : Algebra.adjoin K {(algebraMap target.valuationSubring L) z} = ⊤) :
    Polynomial.aeval z
        (Polynomial.derivative (minpoly base.valuationSubring z)) ∈
      (differentIdealOfFiniteSeparable base target)

theorem

isUnramifiedAt_of_aeval_derivative_isUnit

L493 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.isUnramifiedAt_of_aeval_derivative_isUnit

Documentation

A monogenic finite separable complete-DVF extension is unramified when an integral equation for its generator has unit derivative. The equation need not be the minimal polynomial: integrally closed divisibility transfers the unit condition to the derivative of the minimal polynomial, which then generates the different.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem isUnramifiedAt_of_aeval_derivative_isUnit
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (z : target.valuationSubring)
    (hz : Algebra.adjoin K {(algebraMap target.valuationSubring L) z} = ⊤)
    (P : Polynomial base.valuationSubring)
    (hP : Polynomial.aeval z P = 0)
    (hPderiv :
      IsUnit (Polynomial.aeval z (Polynomial.derivative P))) :
    Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

maximalIdeal_pow_sub_one_dvd_differentIdeal

L544 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_pow_sub_one_dvd_differentIdeal

Documentation

Dedekind's different lower bound: if the image of the base maximal ideal is divisible by P^e, then P^(e-1) divides the different. For Eisenstein extensions this is the standard source of the derivative/different exponent bound.

Source context 13 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in

Lean source · statement

theorem maximalIdeal_pow_sub_one_dvd_differentIdeal
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Algebra.IsSeparable
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring)]
    (e : ℕ)
    (hpow :
      target.maximalIdeal ^ e ∣
        Ideal.map (algebraMap base.valuationSubring target.valuationSubring)
          base.maximalIdeal) :
    target.maximalIdeal ^ (e - 1) ∣
      differentIdeal base.valuationSubring target.valuationSubring

theorem

maximalIdeal_pow_sub_one_dvd_differentIdealOfFiniteSeparable

L563 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_pow_sub_one_dvd_differentIdealOfFiniteSeparable

Documentation

Finite-separable different lower bound, using differentIdealOfFiniteSeparable.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem maximalIdeal_pow_sub_one_dvd_differentIdealOfFiniteSeparable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (e : ℕ)
    (hpow :
      target.maximalIdeal ^ e ∣
        Ideal.map (algebraMap base.valuationSubring target.valuationSubring)
          base.maximalIdeal) :
    target.maximalIdeal ^ (e - 1) ∣ (differentIdealOfFiniteSeparable base target)

theorem

maximalIdeal_pow_ramificationIndex_sub_one_dvd_differentIdealOfFiniteSeparable

L590 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_pow_ramificationIndex_sub_one_dvd_differentIdealOfFiniteSeparable

Documentation

Finite-separable different lower bound at the canonical ramification index: P^(e - 1) divides the finite-separable different. This uses mathlib's defining containment for Ideal.ramificationIdx, so callers do not have to supply the divisibility hypothesis separately.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem maximalIdeal_pow_ramificationIndex_sub_one_dvd_differentIdealOfFiniteSeparable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    target.maximalIdeal ^ (ramificationIndex base.toDVF target.toDVF - 1) ∣
      (differentIdealOfFiniteSeparable base target)

theorem

maximalIdeal_dvd_differentIdealOfFiniteSeparable_of_one_lt_ramificationIndex

L605 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.maximalIdeal_dvd_differentIdealOfFiniteSeparable_of_one_lt_ramificationIndex

Documentation

If the canonical ramification index is nontrivial, the target maximal ideal divides the finite-separable different.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem maximalIdeal_dvd_differentIdealOfFiniteSeparable_of_one_lt_ramificationIndex
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (he : 1 < ramificationIndex base.toDVF target.toDVF) :
    target.maximalIdeal ∣ (differentIdealOfFiniteSeparable base target)

theorem

not_isUnramifiedAt_of_one_lt_ramificationIndex_of_finite_separable

L625 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.not_isUnramifiedAt_of_one_lt_ramificationIndex_of_finite_separable

Documentation

A finite separable extension with nontrivial ramification index is ramified at the target maximal ideal.

Source context 12 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem not_isUnramifiedAt_of_one_lt_ramificationIndex_of_finite_separable
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (he : 1 < ramificationIndex base.toDVF target.toDVF) :
    ¬ Algebra.IsUnramifiedAt base.valuationSubring target.maximalIdeal

theorem

differentIdeal_tower

L648 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdeal_tower

Documentation

Transitivity of the different ideal in a tower of valuation-ring extensions.

Source context 20 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section Tower
variable {M : Type*} [Field M]
variable [Algebra K M] [Algebra M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable {middle : CompleteDVF M}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] [FiniteDimensional K M]
    [FiniteDimensional M L] in

Lean source · statement

theorem differentIdeal_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring target.valuationSubring]
    [Module.Finite base.valuationSubring middle.valuationSubring]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [Module.Finite middle.valuationSubring target.valuationSubring]
    [Module.IsTorsionFree base.valuationSubring middle.valuationSubring]
    [Module.IsTorsionFree base.valuationSubring target.valuationSubring]
    [Module.IsTorsionFree middle.valuationSubring target.valuationSubring]
    [Algebra.IsSeparable
      (FractionRing base.valuationSubring)
      (FractionRing target.valuationSubring)] :
    differentIdeal base.valuationSubring target.valuationSubring =
      differentIdeal middle.valuationSubring target.valuationSubring *
        Ideal.map (algebraMap middle.valuationSubring target.valuationSubring)
          (differentIdeal base.valuationSubring middle.valuationSubring)

theorem

differentIdealOfFiniteSeparable_tower

L668 ↗

RamificationTheory.DiscreteValuationField.ValuedExtension.differentIdealOfFiniteSeparable_tower

Documentation

Finite-separable tower formula for the different, using the finite-separable different ideals on all three steps.

Source context 19 commands

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

noncomputable section
universe u v w x
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace RamificationTheory
namespace DiscreteValuationField
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section Tower
variable {M : Type*} [Field M]
variable [Algebra K M] [Algebra M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable {middle : CompleteDVF M}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]

Lean source · statement

theorem differentIdealOfFiniteSeparable_tower
    [IsScalarTower K M L]
    [Algebra.IsSeparable K M] [Algebra.IsSeparable M L]
    [Algebra.IsSeparable K L]
    [IsScalarTower base.valuationSubring middle.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring middle.valuationSubring M]
    [IsScalarTower middle.valuationSubring target.valuationSubring L]
    [IsScalarTower base.valuationSubring target.valuationSubring L] :
    (differentIdealOfFiniteSeparable base target) =
      (differentIdealOfFiniteSeparable middle target) *
        Ideal.map (algebraMap middle.valuationSubring target.valuationSubring)
          (differentIdealOfFiniteSeparable base middle)

Module documentation

Different and codifferent for valued finite extensions

Declarations