Non-Archimedean Local Fields

Basic properties of nonarch local fields.

Main results

• ℚₚ is a nonarch local field (TODO currently sorried)
• equivResidueField : 𝓀[K] ≃ₐ[𝒪[K]] 𝓂[K].ResidueField for K nonarch local
• valuationOfIoo (ε : Set.Ioo (0 : ℝ) 1) : Valuation K ℝ≥0 (sending a uniformiser to ε)
• valuation_ext : Two Valuations which are compatible with the valuative structure are equal if they're equal on a uniformiser.
• We have the instance that a valuative extension of nonarch local fields is finite-dimensional.
• IsNonarchimedeanLocalField.isModuleTopology : the larger field in a valuative extension of nonarch local fields has the module topology for the smaller field.
• instance : extension of integer rings in a valuative extension of nonarch local fields is module-finite (TODO currently sorried)
• Basic API for e and f for a valuative extension of nonarch local fields up to and including ef=[L:K].
• Definition of unramified extension (for nonarch local fields, so automatically finite).
• Integral closure of O_K in a valuative extension of nonarch local fields is O_L
• isNonarchimedeanLocalField_of_valuativeExtension: Finite-diml valuative extension of a nonarch local field is a nonarch local field (in the sense that an appropriate topology exists)
• isNonarchimedeanLocalField_of_finiteDimensional: Finite-diml extension of a nonarch local field is a nonarch local field (in the sense that an appropriate valuative structure and topology exist).
• IsNonarchimedeanLocalField.ext_extension: uniqueness of these structures.

instance IsNonarchimedeanLocalField.instLocallyCompactSpacePadic_classFieldTheory (p : ℕ) [Fact (Nat.Prime p)] : LocallyCompactSpace ℚ_[p]

instance IsNonarchimedeanLocalField.instPadic_classFieldTheory (p : ℕ) [Fact (Nat.Prime p)] : IsNonarchimedeanLocalField ℚ_[p]

instance IsNonarchimedeanLocalField.instT2Space_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : T2Space K

theorem IsNonarchimedeanLocalField.prime_ringChar (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Nat.Prime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

theorem IsNonarchimedeanLocalField.associated_iff_of_irreducible (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : ↥(ValuativeRel.valuation K).integer) (hx : Irreducible x) : Associated y x ↔ Irreducible y

def IsNonarchimedeanLocalField.compactOpenOK (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TopologicalSpace.CompactOpens K

noncomputable def IsNonarchimedeanLocalField.equivResidueField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer ≃ₐ[↥(ValuativeRel.valuation K).integer] (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer).ResidueField

instance IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Finite (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer).ResidueField

noncomputable def IsNonarchimedeanLocalField.valuationOfIoo (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (ε : ↑(Set.Ioo 0 1)) : Valuation K NNReal

A chosen valuation to ℝ≥0 that sends any uniformiser to the given ε.

theorem IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt_irreducible {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) : (valueGroupWithZeroIsoInt K) ((ValuativeRel.valuation K) ↑ϖ) = WithZero.exp (-1)

theorem IsNonarchimedeanLocalField.valuation_irreducible {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) : (ValuativeRel.valuation K) ↑ϖ = (valueGroupWithZeroIsoInt K).symm (WithZero.exp (-1))

@[simp]

theorem IsNonarchimedeanLocalField.WithZeroMulInt.toNNReal_exp {e : NNReal} (he : e ≠ 0) {n : ℤ} : (WithZeroMulInt.toNNReal he) (WithZero.exp n) = e ^ n

theorem IsNonarchimedeanLocalField.valuationOfIoo_irreducible {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ε : ↑(Set.Ioo 0 1)} {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) : ↑((valuationOfIoo K ε) ↑ϖ) = ↑ε

noncomputable def IsNonarchimedeanLocalField.rankOneOfIoo (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (ε : ↑(Set.Ioo 0 1)) : (ValuativeRel.valuation K).RankOne

noncomputable def IsNonarchimedeanLocalField.inhabitedIoo : Inhabited ↑(Set.Ioo 0 1)

theorem IsNonarchimedeanLocalField.valuation_ext (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {v₁ v₂ : Valuation K Γ₀} [v₁.Compatible] [v₂.Compatible] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) (h : v₁ ↑ϖ = v₂ ↑ϖ) : v₁ = v₂

theorem Irreducible.ne_zero' {K : Type u_3} {S : Type u_4} [MonoidWithZero K] [SetLike S K] [SubmonoidClass S K] {s : S} {x : ↥s} (h : Irreducible x) : ↑x ≠ 0

instance Valued.toNormedField.compatible (K : Type u_3) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsValuativeTopology K] [hv : v.RankOne] : NormedField.valuation.Compatible

instance IsNonarchimedeanLocalField.instCompatibleNNRealValuationOfIoo (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (ε : ↑(Set.Ioo 0 1)) : (valuationOfIoo K ε).Compatible

instance IsNonarchimedeanLocalField.instFiniteDimensional_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : FiniteDimensional K L

instance IsNonarchimedeanLocalField.isModuleTopology (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsModuleTopology K L

theorem IsNonarchimedeanLocalField.algebraMap_mem_integer (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] (x : ↥(ValuativeRel.valuation K).integer) : (algebraMap (↥(ValuativeRel.valuation K).integer) L) x ∈ (ValuativeRel.valuation L).integer

instance IsNonarchimedeanLocalField.instAlgebraSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : Algebra ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

@[simp]

theorem IsNonarchimedeanLocalField.algebraMap_integers_apply_coe (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] (x : ↥(ValuativeRel.valuation K).integer) : ↑((algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x) = (algebraMap K L) ↑x

instance IsNonarchimedeanLocalField.instContinuousSMul_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ContinuousSMul K L

instance IsNonarchimedeanLocalField.instFaithfulSMulSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : FaithfulSMul ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

instance IsNonarchimedeanLocalField.instFiniteSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_4) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.Finite ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

instance IsNonarchimedeanLocalField.instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [Algebra K L] : IsScalarTower (↥(ValuativeRel.valuation K).integer) K L

instance IsNonarchimedeanLocalField.instIsScalarTowerSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1 (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : IsScalarTower (↥(ValuativeRel.valuation K).integer) (↥(ValuativeRel.valuation L).integer) L

noncomputable def IsNonarchimedeanLocalField.e (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ℕ

The e[L/K] of an extension of local fields (also called the ramification index) is such that vL(iKL ϖK) = vL(ϖL^e[L/K]), or alternatively 𝓂[K] 𝒪[L] = 𝓂[L] ^ e.

theorem IsNonarchimedeanLocalField.e_spec (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {ϖK : ↥(ValuativeRel.valuation K).integer} {ϖL : ↥(ValuativeRel.valuation L).integer} (hϖk : Irreducible ϖK) (hϖl : Irreducible ϖL) : Associated (ϖL ^ e K L) ((algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) ϖK)

theorem IsNonarchimedeanLocalField.e_spec' (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Ideal.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ e K L

noncomputable def IsNonarchimedeanLocalField.f (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ℕ

The f[L/K] of an extension of local fields, which is [𝓀[L] : 𝓀[K]]. It is also called the inertia degree.

instance IsNonarchimedeanLocalField.instLiesOverSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer).LiesOver (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)

instance IsNonarchimedeanLocalField.instIsLocalHomSubtypeMemSubringIntegerValueGroupWithZeroValuationRingHomAlgebraMap_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] (L : Type u_2) [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : IsLocalHom (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer)

noncomputable instance IsNonarchimedeanLocalField.instAlgebraResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Algebra (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

instance IsNonarchimedeanLocalField.instFiniteDimensionalResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : FiniteDimensional (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

instance IsNonarchimedeanLocalField.instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Algebra.IsSeparable (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

theorem IsNonarchimedeanLocalField.f_spec (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.finrank (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) = f K L

theorem IsNonarchimedeanLocalField.f_spec' (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f K L = Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

theorem IsNonarchimedeanLocalField.e_pos (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : 0 < e K L

theorem IsNonarchimedeanLocalField.f_pos (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : 0 < f K L

theorem IsNonarchimedeanLocalField.factors_map_maximalIdeal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : UniqueFactorizationMonoid.factors (Ideal.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) = Multiset.replicate (e K L) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

theorem IsNonarchimedeanLocalField.toFinset_factors_map_maximalIdeal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [DecidableEq (Ideal ↥(ValuativeRel.valuation L).integer)] : (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer))).toFinset = {IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer}

theorem IsNonarchimedeanLocalField.e_mul_f_eq_n (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : e K L * f K L = Module.finrank K L

theorem IsNonarchimedeanLocalField.e_le_n (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : e K L ≤ Module.finrank K L

theorem IsNonarchimedeanLocalField.f_le_n (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : f K L ≤ Module.finrank K L

theorem IsNonarchimedeanLocalField.e_eq_one_of_n_eq_one (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (hn : Module.finrank K L = 1) : e K L = 1

theorem IsNonarchimedeanLocalField.f_eq_one_of_n_eq_one (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (hn : Module.finrank K L = 1) : f K L = 1

class IsNonarchimedeanLocalField.IsUnramified (K : Type u_3) (L : Type u_4) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Prop

• e_eq_one : e K L = 1

theorem IsNonarchimedeanLocalField.isUnramified_iff (K : Type u_3) (L : Type u_4) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsUnramified K L ↔ e K L = 1

theorem IsNonarchimedeanLocalField.isUnramified_iff_map_maximalIdeal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsUnramified K L ↔ Ideal.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer

instance IsNonarchimedeanLocalField.instIsSeparableResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation_classFieldTheory_1 (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Algebra.IsSeparable (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

theorem IsNonarchimedeanLocalField.isUnramified_iff_isUnramifiedAt (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsUnramified K L ↔ Algebra.IsUnramifiedAt (↥(ValuativeRel.valuation K).integer) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

theorem Algebra.unramifiedLocus_eq_univ_iff' {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] : unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

theorem Algebra.isOpen_unramifiedLocus' {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [EssFiniteType R A] : IsOpen (unramifiedLocus R A)

theorem IsNonarchimedeanLocalField.isUnramified_iff_unramified (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsUnramified K L ↔ Algebra.Unramified ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

theorem ValuativeExtension.valuation_le_one_of_isIntegral {K : Type u_1} [Field K] [ValuativeRel K] {L : Type u_2} [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] {y : L} (hy : IsIntegral (↥(ValuativeRel.valuation K).integer) y) : (ValuativeRel.valuation L) y ≤ 1

instance IsNonarchimedeanLocalField.isIntegralClosure (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsIntegralClosure (↥(ValuativeRel.valuation L).integer) (↥(ValuativeRel.valuation K).integer) L

theorem IsNonarchimedeanLocalField.isIntegral_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type u_2} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {y : L} : IsIntegral (↥(ValuativeRel.valuation K).integer) y ↔ (ValuativeRel.valuation L) y ≤ 1

theorem IsNonarchimedeanLocalField.isNonarchimedeanLocalField_of_valuativeExtension_of_isValuativeTopology (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [ValuativeExtension K L] [TopologicalSpace L] [IsValuativeTopology L] : IsNonarchimedeanLocalField L

theorem IsNonarchimedeanLocalField.isNonarchimedeanLocalField_of_valuativeExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [ValuativeExtension K L] : ∃ (x : TopologicalSpace L), IsNonarchimedeanLocalField L

theorem IsNonarchimedeanLocalField.isNonarchimedeanLocalField_of_finiteDimensional (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : ∃ (x : ValuativeRel L) (_ : ValuativeExtension K L) (x_2 : TopologicalSpace L), IsNonarchimedeanLocalField L

theorem IsNonarchimedeanLocalField.ext_extension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] (v₁ v₂ : ValuativeRel L) (t₁ t₂ : TopologicalSpace L) (e₁ : ValuativeExtension K L) (e₂ : ValuativeExtension K L) (h₁ : IsNonarchimedeanLocalField L) (h₂ : IsNonarchimedeanLocalField L) : v₁ = v₂ ∧ t₁ = t₂

theorem IsNonarchimedeanLocalField.unique_isNonarchimedeanLocalField (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] : ∃! i : ValuativeRel L × TopologicalSpace L, ValuativeExtension K L ∧ IsNonarchimedeanLocalField L