theorem hensel_lift_ramificationIdx_eq_one {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)] (α : IsLocalRing.ResidueField B) (hα : (IsLocalRing.ResidueField A)⟮α⟯ = ⊤) (β : B) (hβ : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal B)) β = α) [IsDiscreteValuationRing ↥(integralClosure A ↥K⟮(algebraMap B L) β⟯)] [IsLocalHom (algebraMap A ↥(integralClosure A ↥K⟮(algebraMap B L) β⟯))] : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal ↥(integralClosure A ↥K⟮(algebraMap B L) β⟯)) = 1

theorem integralClosure_formallyUnramified_of_hensel_lift (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)] (α : IsLocalRing.ResidueField B) (hα : (IsLocalRing.ResidueField A)⟮α⟯ = ⊤) (β : B) (hβ : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal B)) β = α) : Algebra.FormallyUnramified A ↥(integralClosure A ↥K⟮(algebraMap B L) β⟯)

theorem adjoin_degree_eq_resDeg_of_hensel_lift (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)] (α : IsLocalRing.ResidueField B) (hα : (IsLocalRing.ResidueField A)⟮α⟯ = ⊤) (β : B) (hβ : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal B)) β = α) : Module.finrank K ↥K⟮(algebraMap B L) β⟯ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem thm_10_13_exists_unram_subext_of_degree_f (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)] : ∃ (E₀ : IntermediateField K L), IsFiniteUnramifiedSubext A K L E₀ ∧ Module.finrank K ↥E₀ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem thm_10_13_unram_le {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)] (E E₀ : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) (hE₀_unram : IsFiniteUnramifiedSubext A K L E₀) (hE₀_deg : Module.finrank K ↥E₀ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) : E ≤ E₀

theorem thm_10_13_unram_field_embedding (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)] (E E₀ : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) (hE₀_unram : IsFiniteUnramifiedSubext A K L E₀) (hE₀_deg : Module.finrank K ↥E₀ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) : ∃ (ι : ↥E →ₐ[K] ↥E₀), ∀ (e : ↥E), (algebraMap (↥E₀) L) (ι e) = (algebraMap (↥E) L) e

theorem thm_10_13_unram_subext_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)] (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) : IsFiniteUnramifiedSubext A K L E → E ≤ E₀

theorem AKLB_resDeg_over_eq_one (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)] (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)) [Algebra (↥(integralClosure A ↥E₀)) B] [IsScalarTower A (↥(integralClosure A ↥E₀)) B] [IsLocalHom (algebraMap (↥(integralClosure A ↥E₀)) B)] : have _instDVR := ⋯; Module.finrank (IsLocalRing.ResidueField ↥(integralClosure A ↥E₀)) (IsLocalRing.ResidueField B) = 1

theorem thm_10_13_totally_ramified_complement (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)] (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)) : have _instDVR := ⋯; ∃ (algOEB : Algebra (↥(integralClosure A ↥E₀)) B) (_ : IsScalarTower A (↥(integralClosure A ↥E₀)) B) (x : IsLocalHom (algebraMap (↥(integralClosure A ↥E₀)) B)), Module.finrank (IsLocalRing.ResidueField ↥(integralClosure A ↥E₀)) (IsLocalRing.ResidueField B) = 1

theorem thm_10_13_maxUnram_eq_resDeg (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)] : ∃ (E₀ : IntermediateField K L), IsFiniteUnramifiedSubext A K L E₀ ∧ Module.finrank K ↥E₀ = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) ∧ (∀ (E : IntermediateField K L), IsFiniteUnramifiedSubext A K L E → E ≤ E₀) ∧ have _instDVR := ⋯; ∃ (algOEB : Algebra (↥(integralClosure A ↥E₀)) B) (_ : IsScalarTower A (↥(integralClosure A ↥E₀)) B) (x : IsLocalHom (algebraMap (↥(integralClosure A ↥E₀)) B)), Module.finrank (IsLocalRing.ResidueField ↥(integralClosure A ↥E₀)) (IsLocalRing.ResidueField B) = 1

theorem thm_10_23_part_i (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)] : Module.finrank K ↥(maximalUnramifiedSubextension A K L) = AKLB_resDeg A B

theorem thm_10_23_part_ii_degree (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)] : Module.finrank (↥(maximalUnramifiedSubextension A K L)) L = AKLB_ramIdx A B

theorem thm_10_23_part_ii_totally_ramified (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)] : have _instDVR := ⋯; ∃ (algOEB : Algebra (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B) (_ : IsScalarTower A (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B) (x : IsLocalHom (algebraMap (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B)), Module.finrank (IsLocalRing.ResidueField ↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) (IsLocalRing.ResidueField B) = 1

theorem thm_10_23_part_iii_galois (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)] [IsGalois K L] : IsGalois K ↥(maximalUnramifiedSubextension A K L)

theorem thm_10_23_galLK_eq_decomp (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : MulAction.stabilizer Gal(L/K) (IsLocalRing.maximalIdeal B) = ⊤

theorem smul_algebraMap_eq_galois {K : Type u_5} [Field K] {L : Type u_6} [Field L] [Algebra K L] {B : Type u_7} [CommRing B] [IsDomain B] [Algebra B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (σ : Gal(L/K)) (b : B) : (algebraMap B L) (σ • b) = σ ((algebraMap B L) b)

theorem dvr_card_inertia_subgroupOf_eq (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] (E : IntermediateField K L) [FiniteDimensional K ↥E] (hunram : Algebra.FormallyUnramified A ↥(integralClosure A ↥E)) : Nat.card ↥((Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)).subgroupOf E.fixingSubgroup) = Nat.card ↥(Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B))

theorem cor_7_14_inertia_le_fixingSubgroup_of_unramified (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] (E : IntermediateField K L) (hfin : FiniteDimensional K ↥E) (hunram : Algebra.FormallyUnramified A ↥(integralClosure A ↥E)) : Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B) ≤ E.fixingSubgroup

theorem cor_7_14_map_maximalIdeal_fixedField_inertia (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : let E := IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)); have _instDVR := ⋯; Ideal.map (algebraMap A ↥(integralClosure A ↥E)) (IsLocalRing.maximalIdeal A) = IsLocalRing.maximalIdeal ↥(integralClosure A ↥E)

theorem dvr_ramIdx_fixedField_inertia_eq_one (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : let E := IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)); have _instDVR := ⋯; (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal ↥(integralClosure A ↥E)) = 1

theorem dvr_isSeparable_residueField_fixedField_inertia (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [IsLocalHom (algebraMap A ↥(integralClosure A ↥(IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)))))] : let E := IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)); have _instDVR := ⋯; Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField ↥(integralClosure A ↥E))

theorem cor_7_14_fixedField_inertia_map_and_sep (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : let E := IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)); 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 cor_7_14_fixedField_inertia_formallyUnramified (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : Algebra.FormallyUnramified A ↥(integralClosure A ↥(IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B))))

theorem formallyUnramified_le_fixedField_inertia (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] (E : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) : E ≤ IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B))

theorem fixedField_inertia_formallyUnramified (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] : IsFiniteUnramifiedSubext A K L (IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)))

theorem fixedField_inertia_eq_maxUnram (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] : IntermediateField.fixedField (Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)) = maximalUnramifiedSubextension A K L

theorem thm_10_23_galLE_eq_inertia (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] : (maximalUnramifiedSubextension A K L).fixingSubgroup = Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B)

theorem thm_10_23_galEK_iso (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)] [IsGalois K L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [SMulCommClass Gal(L/K) A B] [Algebra.IsInvariant A B Gal(L/K)] : Nonempty (Gal(↥(maximalUnramifiedSubextension A K L)/K) ≃* Gal(IsLocalRing.ResidueField B/IsLocalRing.ResidueField A))

theorem thm_10_23 (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)] [IsGalois K L] : have _intCl := ⋯; have _act := IsIntegralClosure.MulSemiringAction A K L B; Module.finrank K ↥(maximalUnramifiedSubextension A K L) = AKLB_resDeg A B ∧ Module.finrank (↥(maximalUnramifiedSubextension A K L)) L = AKLB_ramIdx A B ∧ (have _instDVR := ⋯; ∃ (algOEB : Algebra (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B) (_ : IsScalarTower A (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B) (x : IsLocalHom (algebraMap (↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) B)), Module.finrank (IsLocalRing.ResidueField ↥(integralClosure A ↥(maximalUnramifiedSubextension A K L))) (IsLocalRing.ResidueField B) = 1) ∧ IsGalois K ↥(maximalUnramifiedSubextension A K L) ∧ MulAction.stabilizer Gal(L/K) (IsLocalRing.maximalIdeal B) = ⊤ ∧ (maximalUnramifiedSubextension A K L).fixingSubgroup = Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal B) ∧ Nonempty (Gal(↥(maximalUnramifiedSubextension A K L)/K) ≃* Gal(IsLocalRing.ResidueField B/IsLocalRing.ResidueField A))