NYLL
Module

PrimeObstruction.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Compositum.CommonTop.PrimeObstruction
6 declarations indexed from sourceView source ↗

Module documentation

Common-top prime obstructions

Prime divisors of a nontrivial common primitive quotient obstruct coprimality of the two upper ramification indices.

Imports1
Imported by1

Declarations

theorem

commonTop_exists_prime_commonPrimitiveObstruction_of_leftCanonical_totalTame_of_right_ne

L48 ↗
TameAbhyankar.FieldCompositum.commonTop_exists_prime_commonPrimitiveObstruction_of_leftCanonical_totalTame_of_right_ne
Documentation

If the right upper index is not its primitive lower value and the lower left branch is totally tame, the shared quotient has a prime factor dividing both upper indices.

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_exists_prime_commonPrimitiveObstruction_of_leftCanonical_totalTame_of_right_ne
    [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)
    (hright_ne :
      ramificationIndex base.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF leftTarget.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ∃ commonQuotient,
      commonQuotient ≤
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF) ∧
        ramificationIndex base.toDVF commonTarget.toDVF =
          (ramificationIndex baseK.toDVF leftTarget.toDVF /
              Nat.gcd
                (ramificationIndex baseK.toDVF leftTarget.toDVF)
                (ramificationIndex baseK.toDVF base.toDVF)) *
            commonQuotient ∧
        ramificationIndex leftTarget.toDVF commonTarget.toDVF =
          (ramificationIndex baseK.toDVF base.toDVF /
              Nat.gcd
                (ramificationIndex baseK.toDVF leftTarget.toDVF)
                (ramificationIndex baseK.toDVF base.toDVF)) *
            commonQuotient ∧
        ∃ p, Nat.Prime p ∧ p ∣ commonQuotient ∧
          p ∣ ramificationIndex base.toDVF commonTarget.toDVF ∧
          p ∣ ramificationIndex leftTarget.toDVF commonTarget.toDVF
theorem

commonTop_not_coprime_upperBranches_of_leftCanonical_totalTame_of_right_ne

L123 ↗
TameAbhyankar.FieldCompositum.commonTop_not_coprime_upperBranches_of_leftCanonical_totalTame_of_right_ne
Documentation

Right upper non-primitiveity contradicts coprimality of the upper 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_not_coprime_upperBranches_of_leftCanonical_totalTame_of_right_ne
    [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)
    (hright_ne :
      ramificationIndex base.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF leftTarget.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ¬ Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF)
theorem

commonTop_not_coprime_upperBranches_of_leftCanonical_totalTame_of_left_ne

L155 ↗
TameAbhyankar.FieldCompositum.commonTop_not_coprime_upperBranches_of_leftCanonical_totalTame_of_left_ne
Documentation

Left upper non-primitiveity gives the same obstruction when the lower left branch is totally tame.

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_not_coprime_upperBranches_of_leftCanonical_totalTame_of_left_ne
    [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)
    (hleftTop_ne :
      ramificationIndex leftTarget.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF base.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ¬ Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF)
theorem

commonTop_exists_prime_commonPrimitiveObstruction_of_baseChangeCanonical_totalTame_of_left_ne

L190 ↗
TameAbhyankar.FieldCompositum.commonTop_exists_prime_commonPrimitiveObstruction_of_baseChangeCanonical_totalTame_of_left_ne
Documentation

Symmetric prime obstruction extracted from the left upper branch when the lower base-change branch is totally tame.

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_exists_prime_commonPrimitiveObstruction_of_baseChangeCanonical_totalTame_of_left_ne
    [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 Ω)]
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hleftTop_ne :
      ramificationIndex leftTarget.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF base.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ∃ commonQuotient,
      commonQuotient ≤
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF) ∧
        ramificationIndex base.toDVF commonTarget.toDVF =
          (ramificationIndex baseK.toDVF leftTarget.toDVF /
              Nat.gcd
                (ramificationIndex baseK.toDVF leftTarget.toDVF)
                (ramificationIndex baseK.toDVF base.toDVF)) *
            commonQuotient ∧
        ramificationIndex leftTarget.toDVF commonTarget.toDVF =
          (ramificationIndex baseK.toDVF base.toDVF /
              Nat.gcd
                (ramificationIndex baseK.toDVF leftTarget.toDVF)
                (ramificationIndex baseK.toDVF base.toDVF)) *
            commonQuotient ∧
        ∃ p, Nat.Prime p ∧ p ∣ commonQuotient ∧
          p ∣ ramificationIndex base.toDVF commonTarget.toDVF ∧
          p ∣ ramificationIndex leftTarget.toDVF commonTarget.toDVF
theorem

commonTop_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_left_ne

L265 ↗
TameAbhyankar.FieldCompositum.commonTop_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_left_ne
Documentation

Left upper non-primitiveity contradicts upper-branch coprimality when the lower base-change branch is totally tame.

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_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_left_ne
    [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 Ω)]
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hleftTop_ne :
      ramificationIndex leftTarget.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF base.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ¬ Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF)
theorem

commonTop_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_right_ne

L297 ↗
TameAbhyankar.FieldCompositum.commonTop_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_right_ne
Documentation

Right upper non-primitiveity gives the symmetric obstruction when the lower base-change branch is totally tame.

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_not_coprime_upperBranches_of_baseChangeCanonical_totalTame_of_right_ne
    [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 Ω)]
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hright_ne :
      ramificationIndex base.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF leftTarget.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)) :
    ¬ Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex 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.