NYLL
Module

BranchFinrank.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Compositum.CommonTop.BranchFinrank
5 declarations indexed from sourceView source ↗

Module documentation

Finrank-coprime common-top branch calculus

Field-degree coprimality supplies the lower ramification-index coprimality used by the common-top branch theorems.

Imports1
Imported by2

Declarations

theorem

commonTop_lowerCanonicalRamificationIndex_coprime_of_totalTame_of_finrank_coprime

L42 ↗
TameAbhyankar.FieldCompositum.commonTop_lowerCanonicalRamificationIndex_coprime_of_totalTame_of_finrank_coprime
Documentation

Lower total tameness converts field-degree coprimality into coprimality of the lower ramification indices.

Source context 16 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]
omit [FiniteDimensional K L] [FiniteDimensional K K']
  [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] in
Lean source · statement
theorem commonTop_lowerCanonicalRamificationIndex_coprime_of_totalTame_of_finrank_coprime
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hcop : Nat.Coprime (Module.finrank K L) (Module.finrank K K')) :
    Nat.Coprime
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)
theorem

commonTop_right_ramificationIndex_dvd_left_of_lower_totalTame_of_finrank_coprime

L65 ↗
TameAbhyankar.FieldCompositum.commonTop_right_ramificationIndex_dvd_left_of_lower_totalTame_of_finrank_coprime
Documentation

Finrank-coprime source for right common-top branch divisibility.

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_dvd_left_of_lower_totalTame_of_finrank_coprime
    [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')) :
    ramificationIndex base.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF leftTarget.toDVF
theorem

commonTop_left_ramificationIndex_dvd_baseChange_of_lower_totalTame_of_finrank_coprime

L83 ↗
TameAbhyankar.FieldCompositum.commonTop_left_ramificationIndex_dvd_baseChange_of_lower_totalTame_of_finrank_coprime
Documentation

Finrank-coprime source for left common-top branch divisibility.

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_dvd_baseChange_of_lower_totalTame_of_finrank_coprime
    [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')) :
    ramificationIndex leftTarget.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF base.toDVF
theorem

commonTop_canonical_ramificationIndex_coprime_of_lowerCanonical_totalTame_of_finrank_coprime

L101 ↗
TameAbhyankar.FieldCompositum.commonTop_canonical_ramificationIndex_coprime_of_lowerCanonical_totalTame_of_finrank_coprime
Documentation

Finrank-coprime source for coprimality of the two common-top branch ramification indices.

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 [baseK.valuation.HasExtension commonTarget.valuation] in
Lean source · statement
theorem commonTop_canonical_ramificationIndex_coprime_of_lowerCanonical_totalTame_of_finrank_coprime
    [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')) :
    Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF)
theorem

commonTop_rightCanonical_lcmRamificationProduct_of_lowerCanonical_totalTame_of_finrank_coprime

L120 ↗
TameAbhyankar.FieldCompositum.commonTop_rightCanonical_lcmRamificationProduct_of_lowerCanonical_totalTame_of_finrank_coprime
Documentation

Finrank-coprime source for the right common-top lcm product.

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_lcmRamificationProduct_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')) :
    ramificationIndex baseK.toDVF base.toDVF *
        ramificationIndex base.toDVF commonTarget.toDVF =
      Nat.lcm
        (ramificationIndex baseK.toDVF leftTarget.toDVF)
        (ramificationIndex baseK.toDVF base.toDVF)

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