Module

Branch.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Compositum.CommonTop.Branch

18 declarations indexed from sourceView source ↗

Module documentation

Common-top branch calculus

This file contains the ramification-index square, branch divisibility statements, and lower-branch lcm product used by the Abhyankar step. All invariants belong directly to the chosen valued fields; there are no extension records or canonicalization constructors.

Imports4

Imported by4

instance

finiteDimensional_commonTop_over_base

L50 ↗

TameAbhyankar.FieldCompositum.finiteDimensional_commonTop_over_base

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

instance finiteDimensional_commonTop_over_base :
    FiniteDimensional K (L ⊔ K' : IntermediateField K Ω)

instance

finiteDimensional_commonTop_over_right

L54 ↗

TameAbhyankar.FieldCompositum.finiteDimensional_commonTop_over_right

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

instance finiteDimensional_commonTop_over_right :
    FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω)

instance

finiteDimensional_commonTop_over_left

L58 ↗

TameAbhyankar.FieldCompositum.finiteDimensional_commonTop_over_left

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

instance finiteDimensional_commonTop_over_left :
    FiniteDimensional L (L ⊔ K' : IntermediateField K Ω)

instance

isSeparable_commonTop_over_right

L62 ↗

TameAbhyankar.FieldCompositum.isSeparable_commonTop_over_right

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

instance isSeparable_commonTop_over_right :
    Algebra.IsSeparable K' (L ⊔ K' : IntermediateField K Ω)

instance

isSeparable_commonTop_over_left

L66 ↗

TameAbhyankar.FieldCompositum.isSeparable_commonTop_over_left

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

instance isSeparable_commonTop_over_left :
    Algebra.IsSeparable L (L ⊔ K' : IntermediateField K Ω)

theorem

commonTop_ramificationIndex_square

L74 ↗

TameAbhyankar.FieldCompositum.commonTop_ramificationIndex_square

Documentation

Ramification-index products agree for the compositum square with common top L ⊔ K'.

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 [FiniteDimensional K L] [FiniteDimensional K K']
  [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] in

Lean source · statement

theorem commonTop_ramificationIndex_square
    [IsScalarTower baseK.valuationSubring base.valuationSubring
      commonTarget.valuationSubring]
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring
      commonTarget.valuationSubring] :
    ramificationIndex baseK.toDVF base.toDVF *
        ramificationIndex base.toDVF commonTarget.toDVF =
      ramificationIndex baseK.toDVF leftTarget.toDVF *
        ramificationIndex leftTarget.toDVF commonTarget.toDVF

theorem

commonTop_exists_commonPrimitiveQuotient_of_ramificationIndex_square

L89 ↗

TameAbhyankar.FieldCompositum.commonTop_exists_commonPrimitiveQuotient_of_ramificationIndex_square

Documentation

The common-top ramification square factors both upper indices through the primitive parts of the two lower indices, with one shared quotient.

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_commonPrimitiveQuotient_of_ramificationIndex_square
    [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 Ω)] :
    ∃ commonQuotient,
      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

theorem

commonTop_rightPrimitive_iff_leftPrimitive_of_ramificationIndex_square

L135 ↗

TameAbhyankar.FieldCompositum.commonTop_rightPrimitive_iff_leftPrimitive_of_ramificationIndex_square

Documentation

In the common-top square, the two upper branches are primitive at the same time.

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_rightPrimitive_iff_leftPrimitive_of_ramificationIndex_square
    [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 Ω)] :
    Iff
      (ramificationIndex base.toDVF commonTarget.toDVF =
        ramificationIndex baseK.toDVF leftTarget.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF))
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF =
        ramificationIndex baseK.toDVF base.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF))

theorem

commonTop_rightNePrimitive_iff_leftNePrimitive_of_ramificationIndex_square

L179 ↗

TameAbhyankar.FieldCompositum.commonTop_rightNePrimitive_iff_leftNePrimitive_of_ramificationIndex_square

Documentation

Contrapositive form of commonTop_rightPrimitive_iff_leftPrimitive_of_ramificationIndex_square.

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_rightNePrimitive_iff_leftNePrimitive_of_ramificationIndex_square
    [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 Ω)] :
    Iff
      (ramificationIndex base.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF leftTarget.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF))
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF ≠
        ramificationIndex baseK.toDVF base.toDVF /
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF))

theorem

commonTop_exists_commonPrimitiveQuotient_le_gcd_of_leftCanonical_totalTame

L214 ↗

TameAbhyankar.FieldCompositum.commonTop_exists_commonPrimitiveQuotient_le_gcd_of_leftCanonical_totalTame

Documentation

If the lower left branch is totally tame, the right common-top degree bound bounds the shared primitive quotient by the lower gcd.

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_commonPrimitiveQuotient_le_gcd_of_leftCanonical_totalTame
    [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) :
    ∃ commonQuotient,
      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 ∧
        commonQuotient ≤
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)

theorem

commonTop_exists_commonPrimitiveQuotient_le_gcd_of_baseChangeCanonical_totalTame

L278 ↗

TameAbhyankar.FieldCompositum.commonTop_exists_commonPrimitiveQuotient_le_gcd_of_baseChangeCanonical_totalTame

Documentation

Symmetric primitive-quotient bound from total tameness of the lower base-change branch.

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_commonPrimitiveQuotient_le_gcd_of_baseChangeCanonical_totalTame
    [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) :
    ∃ commonQuotient,
      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 ∧
        commonQuotient ≤
          Nat.gcd
            (ramificationIndex baseK.toDVF leftTarget.toDVF)
            (ramificationIndex baseK.toDVF base.toDVF)

theorem

commonTop_right_ramificationIndex_dvd_left_of_totalTame_of_linearDisjoint

L345 ↗

TameAbhyankar.FieldCompositum.commonTop_right_ramificationIndex_dvd_left_of_totalTame_of_linearDisjoint

Documentation

If the lower left extension is totally tame and L and K' are linearly disjoint, the right common-top ramification index divides the lower-left ramification index.

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 base.valuation]
  [leftTarget.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in

Lean source · statement

theorem commonTop_right_ramificationIndex_dvd_left_of_totalTame_of_linearDisjoint
    [IsScalarTower baseK.valuationSubring leftTarget.valuationSubring L]
    [IsScalarTower base.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hleft : IsTotallyTamelyRamified baseK.toDVF leftTarget.toDVF)
    (hlin : L.LinearDisjoint K') :
    ramificationIndex base.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF leftTarget.toDVF

theorem

commonTop_left_ramificationIndex_dvd_baseChange_of_totalTame_of_linearDisjoint

L375 ↗

TameAbhyankar.FieldCompositum.commonTop_left_ramificationIndex_dvd_baseChange_of_totalTame_of_linearDisjoint

Documentation

Symmetric divisibility for a totally tame lower base-change 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 [baseK.valuation.HasExtension leftTarget.valuation]
  [base.valuation.HasExtension commonTarget.valuation]
  [baseK.valuation.HasExtension commonTarget.valuation] in

Lean source · statement

theorem commonTop_left_ramificationIndex_dvd_baseChange_of_totalTame_of_linearDisjoint
    [IsScalarTower baseK.valuationSubring base.valuationSubring K']
    [IsScalarTower leftTarget.valuationSubring commonTarget.valuationSubring
      (L ⊔ K' : IntermediateField K Ω)]
    (hbase : IsTotallyTamelyRamified baseK.toDVF base.toDVF)
    (hlin : L.LinearDisjoint K') :
    ramificationIndex leftTarget.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF base.toDVF

theorem

linearDisjoint_of_lowerCanonical_totalTame_of_coprime

L407 ↗

TameAbhyankar.FieldCompositum.linearDisjoint_of_lowerCanonical_totalTame_of_coprime

Documentation

Lower total tameness turns coprimality of ramification indices into linear disjointness of the two field branches.

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 [FiniteDimensional K L] [FiniteDimensional K K']
  [Algebra.IsSeparable K L] [Algebra.IsSeparable K K'] in

Lean source · statement

theorem linearDisjoint_of_lowerCanonical_totalTame_of_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
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)) :
    L.LinearDisjoint K'

theorem

commonTop_right_ramificationIndex_dvd_left_of_lower_totalTame_of_coprime

L428 ↗

TameAbhyankar.FieldCompositum.commonTop_right_ramificationIndex_dvd_left_of_lower_totalTame_of_coprime

Documentation

Lower total tameness and lower coprimality supply the 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_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
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)) :
    ramificationIndex base.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF leftTarget.toDVF

theorem

commonTop_left_ramificationIndex_dvd_baseChange_of_lower_totalTame_of_coprime

L449 ↗

TameAbhyankar.FieldCompositum.commonTop_left_ramificationIndex_dvd_baseChange_of_lower_totalTame_of_coprime

Documentation

Lower total tameness and lower coprimality supply the 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_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
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)) :
    ramificationIndex leftTarget.toDVF commonTarget.toDVF ∣
      ramificationIndex baseK.toDVF base.toDVF

theorem

commonTop_canonical_ramificationIndex_coprime_of_lowerCanonical_totalTame_of_coprime

L469 ↗

TameAbhyankar.FieldCompositum.commonTop_canonical_ramificationIndex_coprime_of_lowerCanonical_totalTame_of_coprime

Documentation

The two upper ramification indices are coprime when the two lower indices are coprime and the lower branches are totally tame.

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_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
      (ramificationIndex baseK.toDVF leftTarget.toDVF)
      (ramificationIndex baseK.toDVF base.toDVF)) :
    Nat.Coprime
      (ramificationIndex base.toDVF commonTarget.toDVF)
      (ramificationIndex leftTarget.toDVF commonTarget.toDVF)

theorem

commonTop_rightCanonical_lcmRamificationProduct_of_lowerCanonical_totalTame_of_coprime

L499 ↗

TameAbhyankar.FieldCompositum.commonTop_rightCanonical_lcmRamificationProduct_of_lowerCanonical_totalTame_of_coprime

Documentation

The common-top square, the two lower-branch divisibilities, and lower coprimality reconstruct the lcm product for the right branch.

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

Module documentation

Common-top branch calculus

Declarations