@[reducible, inline]

noncomputable abbrev AKLB_residueChar (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : ℕ

def AKLB_IsTamelyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] : Prop

def AKLB_IsTotallyTamelyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] (L : Type u_4) [Field L] [Algebra K L] : Prop

theorem tamelyRamified_of_tower_left {p e_EK e_EL e_LK : ℕ} (hmul : e_EK = e_EL * e_LK) (h : ¬p ∣ e_EK) : ¬p ∣ e_LK

theorem tamelyRamified_of_tower_right {p e_EK e_EL e_LK : ℕ} (hmul : e_EK = e_EL * e_LK) (h : ¬p ∣ e_EK) : ¬p ∣ e_EL

theorem tamelyRamified_tower {p e_EK e_EL e_LK : ℕ} (hp : Nat.Prime p ∨ p = 0) (hmul : e_EK = e_EL * e_LK) (hEL : ¬p ∣ e_EL) (hLK : ¬p ∣ e_LK) : ¬p ∣ e_EK

theorem tamelyRamified_tower_iff {p e_EK e_EL e_LK : ℕ} (hp : Nat.Prime p ∨ p = 0) (hmul : e_EK = e_EL * e_LK) : ¬p ∣ e_EK ↔ ¬p ∣ e_EL ∧ ¬p ∣ e_LK

theorem residueChar_prime_or_zero (F : Type u_1) [Field F] : Nat.Prime (ringChar F) ∨ ringChar F = 0

theorem totallyRamified_tower {f_EK f_EL f_LK : ℕ} (hmul_f : f_EK = f_EL * f_LK) (hEL : f_EL = 1) (hLK : f_LK = 1) : f_EK = 1

structure IsNthRootOfUniformizer (A : Type u_1) [CommRing A] (B : Type u_3) [CommRing B] [Algebra A B] (n : ℕ) (π : B) (πA : A) : Prop

• uniformizer_A : Irreducible πA
• pow_eq : π ^ n = (algebraMap A B) πA
• adjoin_eq_top : A[π] = ⊤

theorem nth_root_of_uniformizer_generates (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_7) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_8) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (n : ℕ) (hn : 1 < n) (π : B) (πA : A) (hπA : Irreducible πA) (hpow : π ^ n = (algebraMap A B) πA) (hn_eq : n = Module.finrank K L) : Irreducible π ∧ A[π] = ⊤

theorem uniformizer_pow_associated_algebraMap (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_7) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_8) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA₀ : A) (hπA₀ : Irreducible πA₀) (πB : B) (hπB : Irreducible πB) : ∃ (u : Bˣ), πB ^ Module.finrank K L = ↑u * (algebraMap A B) πA₀

theorem hensel_unit_nth_root_of_one_mod (B : Type u_5) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [IsAdicComplete (IsLocalRing.maximalIdeal B) B] (n : ℕ) (hn : 1 < n) (hp : ¬ringChar (IsLocalRing.ResidueField B) ∣ n) (u : Bˣ) (hu_mod : ↑u - 1 ∈ IsLocalRing.maximalIdeal B) : ∃ (r : Bˣ), ↑r ^ n = ↑u

theorem uniformizer_adjust_mod_maximal (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_7) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_8) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA₀ : A) (hπA₀ : Irreducible πA₀) (πB : B) (hπB : Irreducible πB) (u : Bˣ) (hu : πB ^ Module.finrank K L = ↑u * (algebraMap A B) πA₀) : ∃ (πA₁ : A) (u₁ : Bˣ), Irreducible πA₁ ∧ πB ^ Module.finrank K L = ↑u₁ * (algebraMap A B) πA₁ ∧ ↑u₁ - 1 ∈ IsLocalRing.maximalIdeal B

theorem isPrecomplete_of_pow {R : Type u_5} [CommRing R] {I : Ideal R} {M : Type u_6} [AddCommGroup M] [Module R M] (e : ℕ) (he : 1 ≤ e) [hpc : IsPrecomplete (I ^ e) M] : IsPrecomplete I M

theorem finite_extension_adic_complete (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_6) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] : IsAdicComplete (IsLocalRing.maximalIdeal B) B

theorem residue_char_eq_of_local_hom (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (B : Type u_6) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] : ringChar (IsLocalRing.ResidueField B) = ringChar (IsLocalRing.ResidueField A)

theorem totally_tamely_ramified_has_nth_root (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_7) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_8) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (htame : ¬AKLB_residueChar A ∣ AKLB_ramIdx A B) (hn1 : 1 < Module.finrank K L) : ∃ (πA : A) (π : B), Irreducible πA ∧ π ^ Module.finrank K L = (algebraMap A B) πA ∧ A[π] = ⊤

theorem totallyTamelyRamified_of_nthRootOfUniformizer (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (hn : 1 < Module.finrank K L) (π : B) (πA : A) (hroot : IsNthRootOfUniformizer A B (Module.finrank K L) π πA) (htame : ¬AKLB_residueChar A ∣ Module.finrank K L) : AKLB_IsTotallyTamelyRamified A K B L

theorem nthRootOfUniformizer_of_totallyTamelyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (httr : AKLB_IsTotallyTamelyRamified A K B L) : ∃ (πA : A) (π : B), IsNthRootOfUniformizer A B (Module.finrank K L) π πA

theorem totallyTamelyRamified_iff_nthRootOfUniformizer (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (hn : 1 < Module.finrank K L) (htame_deg : ¬AKLB_residueChar A ∣ Module.finrank K L) : AKLB_IsTotallyTamelyRamified A K B L ↔ ∃ (πA : A) (π : B), IsNthRootOfUniformizer A B (Module.finrank K L) π πA

theorem padic_decomp_exists (e : ℕ) (he : e ≠ 0) (p : ℕ) (hp : Nat.Prime p ∨ p = 0) : ∃ (m : ℕ) (a : ℕ), e = m * p ^ a ∧ ¬p ∣ m

theorem padic_decomp_unique (p : ℕ) (hp : Nat.Prime p ∨ p = 0) (m₁ m₂ a₁ a₂ : ℕ) (hm₁ : ¬p ∣ m₁) (hm₂ : ¬p ∣ m₂) (hne : m₁ * p ^ a₁ ≠ 0) (heq : m₁ * p ^ a₁ = m₂ * p ^ a₂) : m₁ = m₂ ∧ a₁ = a₂

theorem padic_decomp_unique_tower (p : ℕ) (hp : Nat.Prime p ∨ p = 0) {e m₁ m₂ a₁ a₂ : ℕ} (he : e ≠ 0) (heq₁ : e = m₁ * p ^ a₁) (hm₁ : ¬p ∣ m₁) (heq₂ : e = m₂ * p ^ a₂) (hm₂ : ¬p ∣ m₂) : m₁ = m₂ ∧ a₁ = a₂

theorem IntermediateField.adjoin_singleton_eq_of_smul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (α β : L) (h1 : ∃ (k : K), (algebraMap K L) k * β = α) (h2 : ∃ (k : K), (algebraMap K L) k * α = β) : K⟮α⟯ = K⟮β⟯

theorem ratio_pow_eq_one {L : Type u_1} [Field L] (α β c : L) (m : ℕ) (hα : α ^ m = c) (hβ : β ^ m = c) (hc : c ≠ 0) : (α * β⁻¹) ^ m = 1

theorem rootOfUnity_intCl_unramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (E : Type u_3) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra.IsSeparable K E] [Algebra A E] [IsScalarTower A K E] (m : ℕ) (hm_ne : ↑m ≠ 0) (ζ : E) (hζ : ζ ^ m = 1) (hgen : K⟮ζ⟯ = ⊤) : have _instDVR := ⋯; ∃ (x : IsLocalHom (algebraMap A ↥(integralClosure A E))), Ideal.map (algebraMap A ↥(integralClosure A E)) (IsLocalRing.maximalIdeal A) = IsLocalRing.maximalIdeal ↥(integralClosure A E) ∧ Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField ↥(integralClosure A E))

theorem rootOfUnity_adjoin_le_maxUnram (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (ζ : L) (hζ : ζ ^ m = 1) : K⟮ζ⟯ ≤ maximalUnramifiedSubextension A K L

theorem rootOfUnity_trivialAdjoin_of_totallyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (ζ : L) (hζ : ζ ^ m = 1) : Module.finrank K ↥K⟮ζ⟯ = 1

theorem roots_of_unity_in_base_of_totally_ramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (ζ : L) (hζ : ζ ^ m = 1) : ∃ (ζ₀ : K), (algebraMap K L) ζ₀ = ζ

theorem hensel_dvr_mth_root_of_uniformizer (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (hm_dvd : m ∣ Module.finrank K L) : ∃ (ϖ : A) (π : L), Irreducible ϖ ∧ π ^ m = (algebraMap K L) ((algebraMap A K) ϖ) ∧ π ≠ 0

theorem hensel_uniformizer_construction (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m a : ℕ) (hma : Module.finrank K L = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (πA_img : K) (π : L), π ^ m = (algebraMap K L) πA_img ∧ (algebraMap K L) πA_img ≠ 0 ∧ π ≠ 0 ∧ Module.finrank K ↥K⟮π⟯ = m ∧ Module.finrank (↥K⟮π⟯) L = AKLB_residueChar A ^ a ∧ ∃ (πA : A), Irreducible πA ∧ (algebraMap A K) πA = πA_img

theorem hensel_dvr_mth_root_in_subext (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m : ℕ) (hm_pos : 0 < m) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) : ∃ (ϖ : A) (α₀ : ↥T), Irreducible ϖ ∧ ↑α₀ ^ m = (algebraMap K L) ((algebraMap A K) ϖ) ∧ ↑α₀ ≠ 0

theorem sub_ext_uniformizer_adjust (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA : A) (hπA_irr : Irreducible πA) (m : ℕ) (hm_pos : 0 < m) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) (ϖ : A) (hϖ_irr : Irreducible ϖ) (α₀ : ↥T) (hα₀ : ↑α₀ ^ m = (algebraMap K L) ((algebraMap A K) ϖ)) : ∃ (πA₁ : A) (α₁ : ↥T) (u : Aˣ), Irreducible πA₁ ∧ ↑α₁ ^ m = (algebraMap K L) ((algebraMap A K) πA₁) ∧ πA = ↑u * πA₁ ∧ ↑u - 1 ∈ IsLocalRing.maximalIdeal A

theorem hensel_mth_root_in_subext (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA : A) (hπA_irr : Irreducible πA) (m : ℕ) (hm_pos : 0 < m) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) : ∃ (α₀ : ↥T), ↑α₀ ^ m = (algebraMap K L) ((algebraMap A K) πA)

theorem subExtNewtonApproxInIntermediate (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA : A) (hπA_irr : Irreducible πA) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) : ∃ (ϖ : A) (α₀ : ↥T) (u : Aˣ), Irreducible ϖ ∧ ↑α₀ ^ m = (algebraMap K L) ((algebraMap A K) ϖ) ∧ πA = ↑u * ϖ ∧ ↑u - 1 ∈ IsLocalRing.maximalIdeal A

theorem rootInIntermediate_of_totallyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA_img : K) (_hπA : (algebraMap K L) πA_img ≠ 0) (hπA_img : ∃ (πA : A), Irreducible πA ∧ (algebraMap A K) πA = πA_img) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) : ∃ (α : ↥T), ↑α ^ m = (algebraMap K L) πA_img

theorem uniformizerPreimage (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA_img : K) (hπA : (algebraMap K L) πA_img ≠ 0) (hπA_img : ∃ (πA : A), Irreducible πA ∧ (algebraMap A K) πA = πA_img) : ∃ (πA : A), (algebraMap A K) πA = πA_img ∧ πA ∈ IsLocalRing.maximalIdeal A ∧ πA ∉ IsLocalRing.maximalIdeal A ^ 2

theorem irreducible_xm_sub_uniformizer (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA_img : K) (hπA : (algebraMap K L) πA_img ≠ 0) (hπA_img : ∃ (πA : A), Irreducible πA ∧ (algebraMap A K) πA = πA_img) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (hm_pos : 0 < m) : Irreducible (Polynomial.X ^ m - Polynomial.C πA_img)

theorem intermediateField_generatedByRoot (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (πA_img : K) (hπA : (algebraMap K L) πA_img ≠ 0) (hπA_img : ∃ (πA : A), Irreducible πA ∧ (algebraMap A K) πA = πA_img) (m : ℕ) (hm : ¬AKLB_residueChar A ∣ m) (T : IntermediateField K L) (hT_deg : Module.finrank K ↥T = m) : ∃ (α : L), α ^ m = (algebraMap K L) πA_img ∧ T = K⟮α⟯

theorem tameWildDecomposition_existence (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m a : ℕ) (hma : Module.finrank K L = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (T : IntermediateField K L), Module.finrank K ↥T = m ∧ Module.finrank (↥T) L = AKLB_residueChar A ^ a

theorem tameWildDecomposition_uniqueness (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (m a : ℕ) (hma : Module.finrank K L = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) (T₁ T₂ : IntermediateField K L) (hT₁_deg : Module.finrank K ↥T₁ = m) (_hT₁_wild : Module.finrank (↥T₁) L = AKLB_residueChar A ^ a) (hT₂_deg : Module.finrank K ↥T₂ = m) (_hT₂_wild : Module.finrank (↥T₂) L = AKLB_residueChar A ^ a) : T₁ = T₂

theorem tameWildDecomposition (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (htotram : AKLB_ramIdx A B = Module.finrank K L) (hn : 0 < Module.finrank K L) : ∃! T : IntermediateField K L, ∃ (m : ℕ) (a : ℕ), Module.finrank K L = m * AKLB_residueChar A ^ a ∧ ¬AKLB_residueChar A ∣ m ∧ Module.finrank K ↥T = m ∧ Module.finrank (↥T) L = AKLB_residueChar A ^ a

noncomputable def intClE_to_L_algHom (A : Type u_1) [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (E : IntermediateField K L) : ↥(integralClosure A ↥E) →ₐ[A] L

noncomputable def intClE_to_B_algHom (A : Type u_1) [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {L : Type u_4} [Field L] [Algebra K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (E : IntermediateField K L) : ↥(integralClosure A ↥E) →ₐ[A] B

noncomputable def ramIdx_sub (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {L : Type u_4} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E : IntermediateField K L) : ℕ

noncomputable def ramIdx_over (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {L : Type u_4} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E : IntermediateField K L) : ℕ

theorem ramIdx_mul (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E : IntermediateField K L) : AKLB_ramIdx A B = ramIdx_over A B E * ramIdx_sub A B E

theorem ramIdx_over_eq_finrank_of_above_maxUnram (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E : IntermediateField K L) (hE : maximalUnramifiedSubextension A K L ≤ E) : ramIdx_over A B E = Module.finrank (↥E) L

theorem tameWildDecomposition_inSubTower (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (m a : ℕ) (hma : AKLB_ramIdx A B = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (T : IntermediateField (↥(maximalUnramifiedSubextension A K L)) L), Module.finrank (↥T) L = AKLB_residueChar A ^ a

theorem tameWildDecomposition_subTowerExistence (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (m a : ℕ) (hma : AKLB_ramIdx A B = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (E : IntermediateField K L), maximalUnramifiedSubextension A K L ≤ E ∧ Module.finrank (↥E) L = AKLB_residueChar A ^ a

theorem exists_intermediate_with_ramIdx_over_eq_pa (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (m a : ℕ) (hma : AKLB_ramIdx A B = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (E : IntermediateField K L), maximalUnramifiedSubextension A K L ≤ E ∧ ramIdx_over A B E = AKLB_residueChar A ^ a ∧ Module.finrank (↥E) L = AKLB_residueChar A ^ a

theorem tameWildDecomposition_towerTranslation (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (m a : ℕ) (hma : AKLB_ramIdx A B = m * AKLB_residueChar A ^ a) (hm : ¬AKLB_residueChar A ∣ m) : ∃ (E : IntermediateField K L), maximalUnramifiedSubextension A K L ≤ E ∧ ramIdx_sub A B E = m ∧ ramIdx_over A B E = Module.finrank (↥E) L ∧ Module.finrank (↥E) L = AKLB_residueChar A ^ a

theorem tameWildDecompositionGeneral_existence (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] : ∃ (E : IntermediateField K L), ¬AKLB_residueChar A ∣ ramIdx_sub A B E ∧ ramIdx_over A B E = Module.finrank (↥E) L ∧ (∃ (k : ℕ), ramIdx_over A B E = AKLB_residueChar A ^ k) ∧ maximalUnramifiedSubextension A K L ≤ E

theorem intClE_residue_surj_of_totallyRamified {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {B : Type u_3} [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {L : Type u_4} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E' : IntermediateField K L) (hE'_totram : ramIdx_over A B E' = Module.finrank (↥E') L) [Algebra (↥(integralClosure A ↥E')) B] [IsScalarTower A (↥(integralClosure A ↥E')) B] (α : IsLocalRing.ResidueField B) : ∃ (γ : ↥(integralClosure A ↥E')), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal B)) ((algebraMap (↥(integralClosure A ↥E')) B) γ) = α

theorem hensel_lift_in_totallyRamified_complement {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] {B : Type u_3} [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] {L : Type u_4} [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E' : IntermediateField K L) (hE'_totram : ramIdx_over A B E' = Module.finrank (↥E') L) (α : IsLocalRing.ResidueField B) (hα : (IsLocalRing.ResidueField A)⟮α⟯ = ⊤) (β : B) (hβ : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal B)) β = α) : (algebraMap B L) β ∈ ↑E'

theorem maxUnram_le_of_totally_ramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E₀ : IntermediateField K L) (hE₀_unram : IsFiniteUnramifiedSubext A K L E₀) (hE₀_deg : Module.finrank K ↥E₀ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (E' : IntermediateField K L) (hE'_totram : ramIdx_over A B E' = Module.finrank (↥E') L) : E₀ ≤ E'

theorem unramified_le_of_totallyRamified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) (E' : IntermediateField K L) (hE'_totram : ramIdx_over A B E' = Module.finrank (↥E') L) : E ≤ E'

theorem totally_wildly_ramified_contains_unramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E' : IntermediateField K L) (hE'_totram : ramIdx_over A B E' = Module.finrank (↥E') L) (_hE'_wild : ∃ (k : ℕ), ramIdx_over A B E' = AKLB_residueChar A ^ k) : maximalUnramifiedSubextension A K L ≤ E'

theorem tameWildDecomposition_uniquenessContainment (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E₁ E₂ : IntermediateField K L) (hE₁_F : maximalUnramifiedSubextension A K L ≤ E₁) (hE₂_F : maximalUnramifiedSubextension A K L ≤ E₂) (hE₁_totram : ramIdx_over A B E₁ = Module.finrank (↥E₁) L) (hE₂_totram : ramIdx_over A B E₂ = Module.finrank (↥E₂) L) (hE₁_tame : ¬AKLB_residueChar A ∣ ramIdx_sub A B E₁) (hfin_over : Module.finrank (↥E₁) L = Module.finrank (↥E₂) L) : E₁ ≤ E₂

theorem tameWildDecomposition_uniquenessTowerTranslation (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E₁ E₂ : IntermediateField K L) (hE₁_F : maximalUnramifiedSubextension A K L ≤ E₁) (hE₂_F : maximalUnramifiedSubextension A K L ≤ E₂) (hE₁_totram : ramIdx_over A B E₁ = Module.finrank (↥E₁) L) (hE₂_totram : ramIdx_over A B E₂ = Module.finrank (↥E₂) L) (hE₁_tame : ¬AKLB_residueChar A ∣ ramIdx_sub A B E₁) (hdeg : Module.finrank K ↥E₁ = Module.finrank K ↥E₂) : E₁ = E₂

theorem tameWildDecompositionGeneral_uniqueness (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (E₁ E₂ : IntermediateField K L) (hE₁_tame : ¬AKLB_residueChar A ∣ ramIdx_sub A B E₁) (hE₁_totram : ramIdx_over A B E₁ = Module.finrank (↥E₁) L) (hE₁_wild : ∃ (k : ℕ), ramIdx_over A B E₁ = AKLB_residueChar A ^ k) (hE₁_F : maximalUnramifiedSubextension A K L ≤ E₁) (hE₂_tame : ¬AKLB_residueChar A ∣ ramIdx_sub A B E₂) (hE₂_totram : ramIdx_over A B E₂ = Module.finrank (↥E₂) L) (hE₂_wild : ∃ (k : ℕ), ramIdx_over A B E₂ = AKLB_residueChar A ^ k) (hE₂_F : maximalUnramifiedSubextension A K L ≤ E₂) : E₁ = E₂

theorem tameWildDecompositionGeneral (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] : ∃! E : IntermediateField K L, ¬AKLB_residueChar A ∣ ramIdx_sub A B E ∧ ramIdx_over A B E = Module.finrank (↥E) L ∧ ∃ (k : ℕ), ramIdx_over A B E = AKLB_residueChar A ^ k