Nyll.ValuedFieldTheory.LocalField.Unramified.Composition

theorem

finiteUnramifiedExtension_trans

AlgebraicNumberTheory.Valuations.finiteUnramifiedExtension_trans

Documentation

The finite tower step used in the proof of stability under finite composita.

This is the literal the finite unramified-extension definition argument: separability of the residue extensions is transitive, while both field degrees and residue degrees are multiplicative in a tower.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open DiscreteValuationField.FieldCompositum
section Tower
variable {K M L : Type u}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem finiteUnramifiedExtension_trans
    [FiniteDimensional K M]
    [FiniteDimensional M L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation M)
    (u : LubinTate.Valuations.ExponentialValuation L)
    (hKM : ∀ a : K, w (algebraMap K M a) = v a)
    (hML : ∀ a : M, u (algebraMap M L a) = w a)
    (hKL : ∀ a : K, u (algebraMap K L a) = v a)
    (hM : FiniteUnramifiedExtension v w hKM)
    (hL : FiniteUnramifiedExtension w u hML) :
    FiniteUnramifiedExtension v u hKL

theorem

finiteUnramifiedExtension_sup

L185 ↗

AlgebraicNumberTheory.Valuations.finiteUnramifiedExtension_sup

Documentation

Finite common-ambient form of stability under composita.

If L/K and K'/K are finite unramified extensions inside the same algebraic ambient field, then their actual compositum L ⊔ K' is finite unramified over K. No separate degree or separability hypothesis is used.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
open DiscreteValuationField.FieldCompositum
section FiniteCompositum
variable {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω]

Lean source · full declaration

theorem finiteUnramifiedExtension_sup
    (L K' : IntermediateField K Ω)
    [FiniteDimensional K L]
    [FiniteDimensional K K']
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation Ω)
    (hExt : ∀ a : K, w (algebraMap K Ω a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hL : FiniteUnramifiedExtension v
      (exponentialValuationRestrict w L)
      (exponentialValuationRestrict_extends v w hExt L))
    (hK' : FiniteUnramifiedExtension v
      (exponentialValuationRestrict w K')
      (exponentialValuationRestrict_extends v w hExt K')) :
    let wTop := exponentialValuationRestrict w (L ⊔ K')
    let hBaseTop : ∀ a : K,
        wTop (algebraMap K (L ⊔ K' : IntermediateField K Ω) a) =
          v a := exponentialValuationRestrict_extends v w hExt (L ⊔ K')
    letI : FiniteDimensional K (L ⊔ K' : IntermediateField K Ω) :=
      IntermediateField.finiteDimensional_sup L K'
    FiniteUnramifiedExtension v wTop hBaseTop := by
  let wRight := exponentialValuationRestrict w K'
  let wTop := exponentialValuationRestrict w (L ⊔ K')
  let hBaseRight : ∀ a : K,
      wRight (algebraMap K K' a) = v a :=
    exponentialValuationRestrict_extends v w hExt K'
  let hRightTop : ∀ a : K',
      wTop (algebraMap K' (L ⊔ K' : IntermediateField K Ω) a) =
        wRight a := by
    intro a
    rfl
  let hBaseTop : ∀ a : K,
      wTop (algebraMap K (L ⊔ K' : IntermediateField K Ω) a) =
        v a := exponentialValuationRestrict_extends v w hExt (L ⊔ K')
  let : Algebra.IsAlgebraic K K' := Algebra.IsAlgebraic.of_finite K K'
  let : FiniteDimensional K' (L ⊔ K' : IntermediateField K Ω) :=
    finiteDimensional_sup_over_right_of_left L K'
  let : FiniteDimensional K (L ⊔ K' : IntermediateField K Ω) :=
    IntermediateField.finiteDimensional_sup L K'
  have hTopRight : FiniteUnramifiedExtension wRight wTop hRightTop := by
    exact finiteUnramifiedExtension_commonTop_of_baseChange
      L K' v w hExt hhens hL
  exact finiteUnramifiedExtension_trans
    v wRight wTop hBaseRight hRightTop hBaseTop hK' hTopRight

Composition.lean

Module documentation

Finite composita of unramified extensions

finiteUnramifiedExtension_trans

finiteUnramifiedExtension_sup

Module documentation

Finite composita of unramified extensions

Declarations

finiteUnramifiedExtension_trans

finiteUnramifiedExtension_sup