NYLL
Module

Core.lean

Nyll.ValuedFieldTheory.Ramification.LocalField.Core
23 declarations indexed from sourceView source ↗

Module documentation

Upper ramification jumps

The actual finite-level upper filtration attached to the canonical complete-DVF structure of a nonarchimedean local field, together with its right-limit subgroup and the intrinsic predicate for an upper jump.

Imports7
Imported by13

Declarations

theorem

chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension

L37 ↗
LocalFieldTheory.chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension
Documentation

Uniqueness after forgetting completeness, in the form consumed by the real lower and upper ramification APIs.

Source context 6 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace LocalFieldTheory
Lean source · statement
theorem chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{0, 0, 0, 0, y}
      (localCompleteDVF K).toDVF
      (chosenLocalExtensionCompleteDVF K L).toDVF
def

completeDVFComapAlgEquiv

L57 ↗
RamificationTheory.LocalField.completeDVFComapAlgEquiv
Documentation

Pull a complete discrete valuation back along a field equivalence.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · full declaration
def completeDVFComapAlgEquiv
    {L M : Type} [Field L] [Field M]
    (target : CompleteDVF.{0, 0} M) (e : L ≃+* M) :
    CompleteDVF.{0, 0} L where
  ValueGroup := target.ValueGroup
  valuation := target.valuation.comap e.toRingHom
  instCompleteDiscrete :=
    Valuation.isCompleteDiscrete_comap_ringEquiv target.valuation e
theorem

completeDVFComapAlgEquiv_hasExtension

L68 ↗
RamificationTheory.LocalField.completeDVFComapAlgEquiv_hasExtension
Documentation

Pullback along a base-linear equivalence preserves extension of the base valuation.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · full declaration
theorem completeDVFComapAlgEquiv_hasExtension
    (K L M : Type) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    (base : CompleteDVF.{0, 0} K)
    (target : CompleteDVF.{0, 0} M)
    [base.valuation.HasExtension target.valuation]
    (e : L ≃ₐ[K] M) :
    base.valuation.HasExtension
      (completeDVFComapAlgEquiv target e.toRingEquiv).valuation where
  val_isEquiv_comap := by
    rw [_root_.Valuation.isEquiv_iff_val_le_one]
    intro a
    change
      base.valuation a ≤ 1 ↔
        target.valuation (e ((algebraMap K L) a)) ≤ 1
    rw [e.commutes]
    exact
      (_root_.Valuation.HasExtension.val_map_le_one_iff
        (vR := base.valuation) (vA := target.valuation) a).symm
def

localLowerRamificationGroup

L91 ↗
RamificationTheory.LocalField.localLowerRamificationGroup
Documentation

The actual real lower ramification group of an arbitrary finite Galois extension of nonarchimedean local fields, using its integral-closure valuation.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
def localLowerRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) : Subgroup Gal(L / K)
def

localUpperRamificationGroup

L104 ↗
RamificationTheory.LocalField.localUpperRamificationGroup
Documentation

The actual real upper ramification group of an arbitrary finite Galois extension of nonarchimedean local fields.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
def localUpperRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) : Subgroup Gal(L / K)
theorem

localUpperRamificationGroup_map_autCongr

L117 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_map_autCongr
Documentation

A base-linear field equivalence transports every local upper ramification group to the corresponding group of the equivalent extension.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_map_autCongr
    (K L M : Type)
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K L] [IsGalois K M]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (e : L ≃ₐ[K] M) (t : ℝ) :
    Subgroup.map (AlgEquiv.autCongr e).toMonoidHom
        (localUpperRamificationGroup K L t) =
      localUpperRamificationGroup K M t
theorem

fixedFieldUpperRamificationGroup_map_autCongr

L343 ↗
RamificationTheory.LocalField.fixedFieldUpperRamificationGroup_map_autCongr
Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem fixedFieldUpperRamificationGroup_map_autCongr
    (K L M : Type)
    [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsGalois K L] [IsGalois K M]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Gal(L/K)) [H.Normal]
    (e : IntermediateField.fixedField H ≃ₐ[K] M)
    (t : ℝ) :
    Subgroup.map (AlgEquiv.autCongr e).toMonoidHom
        (fixedFieldUpperRamificationGroup
          (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension
            K L) H t) =
      localUpperRamificationGroup K M t
theorem

fixedFieldUpperRamificationGroup_eq_local

L590 ↗
RamificationTheory.LocalField.fixedFieldUpperRamificationGroup_eq_local
Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem fixedFieldUpperRamificationGroup_eq_local
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : Subgroup Gal(L/K)) [H.Normal]
    (t : ℝ) :
    fixedFieldUpperRamificationGroup
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension
          K L) H t =
      localUpperRamificationGroup K (IntermediateField.fixedField H) t
theorem

localUpperRamificationGroup_map_restrict

L610 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_map_restrict
Documentation

Upper ramification groups descend along restriction between finite Galois intermediate fields in a common separable closure.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_map_restrict
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F]
    (t : ℝ) :
    Subgroup.map
        (intermediateFieldRestrictNormalHom E F hEF)
        (localUpperRamificationGroup K F t) =
      localUpperRamificationGroup K E t
theorem

localUpperRamificationGroup_antitone

L736 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_antitone
Documentation

The local upper ramification filtration is antitone.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_antitone
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Antitone (localUpperRamificationGroup K L)
def

localUpperRamificationGroupAfter

L752 ↗
RamificationTheory.LocalField.localUpperRamificationGroupAfter
Documentation

The subgroup immediately after an upper ramification index for an arbitrary finite local Galois extension.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
def localUpperRamificationGroupAfter
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) : Subgroup Gal(L / K)
theorem

localUpperRamificationGroupAfter_le

L761 ↗
RamificationTheory.LocalField.localUpperRamificationGroupAfter_le
Documentation

The right-limit upper group lies in the group at the limiting index.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroupAfter_le
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) :
    localUpperRamificationGroupAfter K L t ≤
      localUpperRamificationGroup K L t
def

IsLocalUpperRamificationJump

L775 ↗
RamificationTheory.LocalField.IsLocalUpperRamificationJump
Documentation

Intrinsic upper-jump predicate for an arbitrary finite local Galois extension.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
def IsLocalUpperRamificationJump
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) : Prop
theorem

localUpperRamificationGroupAfter_map_restrict

L786 ↗
RamificationTheory.LocalField.localUpperRamificationGroupAfter_map_restrict
Documentation

Restriction along a finite Galois tower carries the right-limit of the upper filtration onto the corresponding right-limit downstairs.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroupAfter_map_restrict
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F]
    (t : ℝ) :
    Subgroup.map
        (intermediateFieldRestrictNormalHom E F hEF)
        (localUpperRamificationGroupAfter K F t) =
      localUpperRamificationGroupAfter K E t
theorem

isLocalUpperRamificationJump_of_map_restrict

L823 ↗
RamificationTheory.LocalField.isLocalUpperRamificationJump_of_map_restrict
Documentation

Every upper jump downstairs in a finite Galois tower was already an upper jump upstairs. Thus quotienting an extension cannot create new break indices.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem isLocalUpperRamificationJump_of_map_restrict
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F]
    {t : ℝ} (ht : IsLocalUpperRamificationJump K E t) :
    IsLocalUpperRamificationJump K F t
theorem

localInverseHerbrandFunction_eq_self_of_nonpos

L846 ↗
RamificationTheory.LocalField.localInverseHerbrandFunction_eq_self_of_nonpos
Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localInverseHerbrandFunction_eq_self_of_nonpos
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (ht : t ≤ 0) :
    inverseHerbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension K L)
        t =
      t
theorem

localUpperRamificationGroup_eq_localLowerRamificationGroup_of_nonpos

L879 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_eq_localLowerRamificationGroup_of_nonpos
Documentation

At every nonpositive index the inverse Herbrand function is the identity, so upper and lower numbering agree.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_eq_localLowerRamificationGroup_of_nonpos
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (ht : t ≤ 0) :
    localUpperRamificationGroup K L t =
      localLowerRamificationGroup K L t
theorem

localLowerRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos

L894 ↗
RamificationTheory.LocalField.localLowerRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos
Documentation

The lower filtration is constant between the distinguished endpoints -1 and 0: every such real index imposes exactly the first maximal-ideal power.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localLowerRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (hneg : -1 < t) (ht : t ≤ 0) :
    localLowerRamificationGroup K L t =
      localLowerRamificationGroup K L 0
theorem

localUpperRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos

L929 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos
Documentation

The upper filtration is constant on the half-open interval (-1, 0].

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_eq_zero_of_neg_one_lt_of_nonpos
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (hneg : -1 < t) (ht : t ≤ 0) :
    localUpperRamificationGroup K L t =
      localUpperRamificationGroup K L 0
theorem

localUpperRamificationGroup_eq_top_of_le_neg_one

L947 ↗
RamificationTheory.LocalField.localUpperRamificationGroup_eq_top_of_le_neg_one
Documentation

At and below -1, the local upper ramification group is the full Galois group.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem localUpperRamificationGroup_eq_top_of_le_neg_one
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (ht : t ≤ -1) :
    localUpperRamificationGroup K L t = ⊤
theorem

not_isLocalUpperRamificationJump_of_lt_neg_one

L962 ↗
RamificationTheory.LocalField.not_isLocalUpperRamificationJump_of_lt_neg_one
Documentation

No upper jump occurs strictly below the distinguished endpoint -1.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem not_isLocalUpperRamificationJump_of_lt_neg_one
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (ht : t < -1) :
    ¬ IsLocalUpperRamificationJump K L t
theorem

not_isLocalUpperRamificationJump_of_neg_one_lt_of_lt_zero

L992 ↗
RamificationTheory.LocalField.not_isLocalUpperRamificationJump_of_neg_one_lt_of_lt_zero
Documentation

No upper jump occurs strictly between -1 and 0.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem not_isLocalUpperRamificationJump_of_neg_one_lt_of_lt_zero
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (t : ℝ) (hneg : -1 < t) (ht : t < 0) :
    ¬ IsLocalUpperRamificationJump K L t
theorem

isLocalUpperRamificationJump_eq_neg_one_or_nonneg

L1030 ↗
RamificationTheory.LocalField.isLocalUpperRamificationJump_eq_neg_one_or_nonneg
Documentation

Every local upper jump is either the possible endpoint -1 or a nonnegative index.

Source context 10 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe y
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
Lean source · statement
theorem isLocalUpperRamificationJump_eq_neg_one_or_nonneg
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {t : ℝ} (ht : IsLocalUpperRamificationJump K L t) :
    t = -1 ∨ 0 ≤ t

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