NYLL
Module

Finrank.lean

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

Module documentation

Finrank-coprime common-top endpoints

Total tameness converts field-degree coprimality into the lower-index coprimality consumed by the common-top endpoints.

Imports2
Imported by1

Declarations

theorem

commonTop_rightCanonical_abhyankarIndexBound_of_lowerCanonical_totalTame_of_finrank_coprime

L47 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_abhyankarIndexBound_of_lowerCanonical_totalTame_of_finrank_coprime
Documentation

Finrank-coprime common-top Abhyankar index bound.

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_finrank_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 (Module.finrank K L) (Module.finrank K K')) :
    AbhyankarIndexBound
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)
      (ramificationIndex base.toDVF commonTarget.toDVF)
theorem

commonTop_right_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_coprime_of_dvd

L73 ↗
TameAbhyankar.FieldCompositum.commonTop_right_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime right upper index-one endpoint.

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_right_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (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_finrank_coprime_of_dvd

L94 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_isUnramified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime right upper unramified endpoint.

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_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (hdiv :
      ramificationIndex baseK.toDVF leftTarget.toDVF ∣
        ramificationIndex baseK.toDVF base.toDVF) :
    IsUnramified base.toDVF commonTarget.toDVF
theorem

commonTop_rightCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd

L115 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime right upper tame endpoint.

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_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (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_left_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_coprime_of_dvd

L138 ↗
TameAbhyankar.FieldCompositum.commonTop_left_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime left upper index-one endpoint.

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_left_ramificationIndex_eq_one_of_lower_totalTame_of_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (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_finrank_coprime_of_dvd

L159 ↗
TameAbhyankar.FieldCompositum.commonTop_leftCanonical_isUnramified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime left upper unramified endpoint.

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_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (hdiv :
      ramificationIndex baseK.toDVF base.toDVF ∣
        ramificationIndex baseK.toDVF leftTarget.toDVF) :
    IsUnramified leftTarget.toDVF commonTarget.toDVF
theorem

commonTop_leftCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd

L180 ↗
TameAbhyankar.FieldCompositum.commonTop_leftCanonical_isTamelyRamified_of_lowerCanonical_totalTame_of_finrank_coprime_of_dvd
Documentation

Finrank-coprime left upper tame endpoint.

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_finrank_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 (Module.finrank K L) (Module.finrank K K'))
    (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.