NYLL
Module

LowerCanonical.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Compositum.CommonTop.LowerCanonical
7 declarations indexed from sourceView source ↗

Module documentation

Lower-branch common-top Abhyankar consequences

This file exposes the common-top index-one, unramified, and tame endpoints whose inputs are total tameness of the two lower valued extensions.

Imports1
Imported by2

Declarations

theorem

commonTop_rightCanonical_abhyankarIndexBound_of_lowerCanonical_totalTame_of_coprime

L47 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_abhyankarIndexBound_of_lowerCanonical_totalTame_of_coprime
Documentation

Common-top Abhyankar index bound supplied by the lcm product for the lower branches.

Source context 20 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
Lean source · statement
theorem commonTop_rightCanonical_abhyankarIndexBound_of_lowerCanonical_totalTame_of_coprime
    [IsScalarTower baseK.valuationSubring base.valuationSubring
      commonTarget.valuationSubring]
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring
      commonTarget.valuationSubring]
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower base.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    [IsScalarTower leftTarget.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)) :
    AbhyankarIndexBound
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)
      (ramificationIndex base.toDVF commonTarget.toDVF)
theorem

commonTop_rightCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd

L83 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

In the coprime lower-index case, lower divisibility forces the right upper ramification index to be one.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [leftTarget.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem
  commonTop_rightCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower base.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF leftTarget.toDVF ∣
        ramificationIndex baseK.toDVF base.toDVF) :
    ramificationIndex base.toDVF commonTarget.toDVF = 1
theorem

commonTop_rightCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd

L106 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

Right common-top unramified consequence.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [leftTarget.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem commonTop_rightCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower base.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF leftTarget.toDVF ∣
        ramificationIndex baseK.toDVF base.toDVF) :
    IsUnramified base.toDVF commonTarget.toDVF
theorem

commonTop_rightCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd

L126 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

Tame form of the right common-top unramified consequence.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [leftTarget.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem commonTop_rightCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower base.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF leftTarget.toDVF ∣
        ramificationIndex baseK.toDVF base.toDVF)
    (hres : Algebra.IsSeparable base.residueField commonTarget.residueField) :
    IsTamelyRamified base.toDVF commonTarget.toDVF
theorem

commonTop_leftCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd

L150 ↗
TameAbhyankar.FieldCompositum.commonTop_leftCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

Symmetric index-one consequence for the left upper branch.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [base.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem
  commonTop_leftCanonical_ramificationIndex_eq_one_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower leftTarget.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF base.toDVF ∣
        ramificationIndex baseK.toDVF leftTarget.toDVF) :
    ramificationIndex leftTarget.toDVF commonTarget.toDVF = 1
theorem

commonTop_leftCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd

L173 ↗
TameAbhyankar.FieldCompositum.commonTop_leftCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

Left common-top unramified consequence.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [base.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem commonTop_leftCanonical_isUnramified_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower leftTarget.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF base.toDVF ∣
        ramificationIndex baseK.toDVF leftTarget.toDVF) :
    IsUnramified leftTarget.toDVF commonTarget.toDVF
theorem

commonTop_leftCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd

L193 ↗
TameAbhyankar.FieldCompositum.commonTop_leftCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd
Documentation

Tame form of the left common-top unramified consequence.

Source context 21 commands

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

noncomputable section
universe u v x y z t
namespace TameAbhyankar
namespace FieldCompositum
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
variable (L K' : IntermediateField K Ω)
variable [FiniteDimensional K L] [FiniteDimensional K K']
variable [Algebra.IsSeparable K L] [Algebra.IsSeparable K K']
variable {base : CompleteDVF.{v, x} K'}
variable {baseK : CompleteDVF.{u, z} K}
variable {leftTarget : CompleteDVF.{v, t} L}
variable [baseK.valuation.HasExtension leftTarget.valuation]
variable [baseK.valuation.HasExtension base.valuation]
section CommonTop
variable {commonTarget : CompleteDVF.{v, y} (L ⊔ K' : IntermediateField K Ω)}
variable [base.valuation.HasExtension commonTarget.valuation]
variable [leftTarget.valuation.HasExtension commonTarget.valuation]
variable [baseK.valuation.HasExtension commonTarget.valuation]
omit [base.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem commonTop_leftCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_coprime_of_dvd
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower leftTarget.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF))
    (hdiv :
      ramificationIndex baseK.toDVF base.toDVF ∣
        ramificationIndex baseK.toDVF leftTarget.toDVF)
    (hres :
      Algebra.IsSeparable leftTarget.residueField commonTarget.residueField) :
    IsTamelyRamified leftTarget.toDVF commonTarget.toDVF

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