NYLL
Module

Tower.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValuedExtension.Tower
10 declarations indexed from sourceView source ↗

Module documentation

Tame ramification in valued towers

Tameness and total tameness propagate through a finite valued tower. The statements use the canonical invariants of ValuedExtension directly, so the same declarations apply to complete and Henselian discretely valued fields through their toDVF projections.

Imports2
Imported by2

Declarations

theorem

residueField_isScalarTower

L42 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueField_isScalarTower
Documentation

The residue-field algebra maps induced by a valued tower form a scalar tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K M] [FiniteDimensional M L]
  [FiniteDimensional K L] in
Lean source · statement
theorem residueField_isScalarTower :
    IsScalarTower base.residueField middle.residueField target.residueField
theorem

residueMap_surjective_tower

L63 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueMap_surjective_tower
Documentation

Surjectivity of the two residue maps implies surjectivity of the composite residue map.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K M] [FiniteDimensional M L]
  [FiniteDimensional K L] in
Lean source · statement
theorem residueMap_surjective_tower
    (hbase : Function.Surjective (residueMap base middle))
    (htarget : Function.Surjective (residueMap middle target)) :
    Function.Surjective (residueMap base target)
theorem

ramificationIndex_tower

L82 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_tower
Documentation

Multiplicativity of the canonical ramification index in a valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [IsScalarTower K M L] [FiniteDimensional K M]
  [FiniteDimensional M L] [FiniteDimensional K L] in
Lean source · statement
theorem ramificationIndex_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring] :
    ramificationIndex base target =
      ramificationIndex base middle * ramificationIndex middle target
theorem

residueDegree_tower

L96 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree_tower
Documentation

Multiplicativity of the canonical residue degree in a valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [IsScalarTower K M L] [FiniteDimensional K M]
  [FiniteDimensional M L] [FiniteDimensional K L] in
Lean source · statement
theorem residueDegree_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring] :
    residueDegree base target =
      residueDegree base middle * residueDegree middle target
theorem

degree_tower

L113 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.degree_tower
Documentation

Multiplicativity of field degrees in a finite valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L]
  [base.valuation.HasExtension middle.valuation]
  [middle.valuation.HasExtension target.valuation]
  [base.valuation.HasExtension target.valuation] in
Lean source · statement
theorem degree_tower :
    degree base target = degree base middle * degree middle target
theorem

isTotallyRamified_tower_iff

L121 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyRamified_tower_iff
Documentation

A composite valued extension is totally ramified exactly when both steps are totally ramified.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [IsScalarTower K M L] [FiniteDimensional K M]
  [FiniteDimensional M L] [FiniteDimensional K L] in
Lean source · statement
theorem isTotallyRamified_tower_iff
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring] :
    IsTotallyRamified base target ↔
      IsTotallyRamified base middle ∧ IsTotallyRamified middle target
theorem

isDefectless_tower

L139 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isDefectless_tower
Documentation

Defectlessness is preserved by a finite valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem isDefectless_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring]
    (hbase : IsDefectless base middle)
    (htarget : IsDefectless middle target) :
    IsDefectless base target
theorem

isTamelyRamified_tower

L165 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_tower
Documentation

Tame ramification is preserved by a finite valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem isTamelyRamified_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring]
    (hbase : IsTamelyRamified base middle)
    (htarget : IsTamelyRamified middle target) :
    IsTamelyRamified base target
theorem

isTotallyTamelyRamified_tower

L191 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_tower
Documentation

Total tame ramification is preserved by a finite valued tower.

Source context 16 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
omit [FiniteDimensional K L] in
Lean source · statement
theorem isTotallyTamelyRamified_tower
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring]
    (hbase : IsTotallyTamelyRamified base middle)
    (htarget : IsTotallyTamelyRamified middle target) :
    IsTotallyTamelyRamified base target
theorem

ramificationIndex_square

L218 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_square
Documentation

The two products of ramification indices around a valued square agree.

Source context 24 commands

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

noncomputable section
universe u v w x y z a b
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {M : Type y} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]
variable [FiniteDimensional K M] [FiniteDimensional M L]
variable [FiniteDimensional K L]
variable {base : DVF.{u, v} K}
variable {middle : DVF.{y, z} M}
variable {target : DVF.{w, x} L}
variable [base.valuation.HasExtension middle.valuation]
variable [middle.valuation.HasExtension target.valuation]
variable [base.valuation.HasExtension target.valuation]
section Square
variable {M' : Type a} [Field M']
variable [Algebra K M'] [Algebra M' L]
variable [IsScalarTower K M' L]
variable [FiniteDimensional K M'] [FiniteDimensional M' L]
variable {leftMiddle : DVF.{a, b} M'}
variable [base.valuation.HasExtension leftMiddle.valuation]
variable [leftMiddle.valuation.HasExtension target.valuation]
omit [IsScalarTower K M L] [IsScalarTower K M' L]
  [FiniteDimensional K M] [FiniteDimensional M L]
  [FiniteDimensional K L] [FiniteDimensional K M']
  [FiniteDimensional M' L] in
Lean source · statement
theorem ramificationIndex_square
    [IsScalarTower base.valuationSubring middle.valuationSubring
      target.valuationSubring]
    [IsScalarTower base.valuationSubring leftMiddle.valuationSubring
      target.valuationSubring] :
    ramificationIndex base middle * ramificationIndex middle target =
      ramificationIndex base leftMiddle * ramificationIndex leftMiddle target

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