theorem aeval_eq_eval_residue {A : Type u_1} [CommRing A] [IsLocalRing A] (p : Polynomial (IsLocalRing.ResidueField A)) (x : IsLocalRing.ResidueField A) : (Polynomial.aeval x) p = Polynomial.eval x p

theorem hensel_root_lift {A : Type u_1} [CommRing A] [IsLocalRing A] [HenselianLocalRing A] {f : Polynomial A} (hf : f.Monic) (hsep : (Polynomial.map (IsLocalRing.residue A) f).Separable) {a₀ : IsLocalRing.ResidueField A} (ha₀ : (Polynomial.map (IsLocalRing.residue A) f).IsRoot a₀) : ∃ (a : A), f.IsRoot a ∧ (IsLocalRing.residue A) a = a₀

theorem root_maps_to_residue_root {A : Type u_1} [CommRing A] [IsLocalRing A] {f : Polynomial A} {a : A} (ha : f.IsRoot a) : (Polynomial.map (IsLocalRing.residue A) f).IsRoot ((IsLocalRing.residue A) a)

theorem hensel_root_injective {A : Type u_1} [CommRing A] [IsLocalRing A] {f : Polynomial A} (hf : f.Monic) (hsep : (Polynomial.map (IsLocalRing.residue A) f).Separable) {a b : A} (ha : f.IsRoot a) (hb : f.IsRoot b) (hab : (IsLocalRing.residue A) a = (IsLocalRing.residue A) b) : a = b

theorem dvr_ker_algebraMap_absurd (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [Module.Finite A B] (h_le : IsLocalRing.maximalIdeal A ≤ RingHom.ker (algebraMap A B)) : False

theorem algHom_dvr_isLocalHom {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {B₁ : Type u_2} [CommRing B₁] [IsDomain B₁] [IsDiscreteValuationRing B₁] [Algebra A B₁] {B₂ : Type u_3} [CommRing B₂] [IsDomain B₂] [IsDiscreteValuationRing B₂] [Algebra A B₂] [IsLocalHom (algebraMap A B₂)] [Module.Finite A B₂] (φ : B₁ →ₐ[A] B₂) : IsLocalHom φ.toRingHom

theorem adjoinRoot_isLocalRing_of_irred_map (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hg_monic : g.Monic) [IsDomain (AdjoinRoot g)] [Module.Finite A (AdjoinRoot g)] (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : IsLocalRing (AdjoinRoot g)

theorem adjoinRoot_of_injective_of_monic {A : Type u_1} [CommRing A] [IsDomain A] {g : Polynomial A} (hg : g.Monic) (hdeg : 0 < g.natDegree) : Function.Injective ⇑(AdjoinRoot.of g)

theorem natDegree_pos_of_monic_irred_map {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {g : Polynomial A} (hg_monic : g.Monic) (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : 0 < g.natDegree

theorem adjoinRoot_map_maximalIdeal_isMaximal (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) [IsDomain (AdjoinRoot g)] (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : (Ideal.map (AdjoinRoot.of g) (IsLocalRing.maximalIdeal A)).IsMaximal

theorem adjoinRoot_isDVR_of_irred_map (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hg_monic : g.Monic) [IsDomain (AdjoinRoot g)] [Module.Finite A (AdjoinRoot g)] [IsLocalRing (AdjoinRoot g)] (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : IsDiscreteValuationRing (AdjoinRoot g)

theorem adjoinRoot_isLocalHom_of_irred_map (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hg_monic : g.Monic) [IsDomain (AdjoinRoot g)] [Module.Finite A (AdjoinRoot g)] [IsLocalRing (AdjoinRoot g)] (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : IsLocalHom (AdjoinRoot.of g)

theorem adjoinRoot_maxIdeal_eq_map_of_irred (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hg_monic : g.Monic) [IsDomain (AdjoinRoot g)] [Module.Finite A (AdjoinRoot g)] [IsLocalRing (AdjoinRoot g)] (hg_irred_map : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g)) : IsLocalRing.maximalIdeal (AdjoinRoot g) = Ideal.map (AdjoinRoot.of g) (IsLocalRing.maximalIdeal A)

theorem adjoinRoot_dvr_of_irreducible_lift (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] (gbar : Polynomial (IsLocalRing.ResidueField A)) (hgbar_monic : gbar.Monic) (hgbar_irred : Irreducible gbar) (hgbar_sep : gbar.Separable) : ∃ (g : Polynomial A) (_ : g.Monic) (_ : Polynomial.map (IsLocalRing.residue A) g = gbar) (x : IsDomain (AdjoinRoot g)) (x_1 : IsDiscreteValuationRing (AdjoinRoot g)) (_ : IsLocalHom (AdjoinRoot.of g)) (_ : Module.Finite A (AdjoinRoot g)) (hAlg : Algebra (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField (AdjoinRoot g))) (_ : FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField (AdjoinRoot g))) (_ : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField (AdjoinRoot g))), Nonempty (IsLocalRing.ResidueField (AdjoinRoot g) ≃+* AdjoinRoot gbar)

theorem henselian_dvr_extension_of_henselian {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [IsAdicComplete (IsLocalRing.maximalIdeal B) B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] : HenselianLocalRing B

theorem finiteDimensional_residueField_of_finite_dvr (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] : FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

theorem adjoinRoot_module_finite_of_monic {A : Type u_1} [CommRing A] (g : Polynomial A) (hg : g.Monic) : Module.Finite A (AdjoinRoot g)

theorem adjoinRoot_isDomain_of_irreducible_mod {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (g : Polynomial A) (hg : g.Monic) (hirr : Irreducible (Polynomial.map (IsLocalRing.residue A) g)) : IsDomain (AdjoinRoot g)

theorem finrank_adjoinRoot_of_monic {A : Type u_1} [CommRing A] [IsDomain A] (g : Polynomial A) (hg : g.Monic) : Module.finrank A (AdjoinRoot g) = g.natDegree

theorem surjective_of_range_sup_maximalIdeal_smul_eq_top {A : Type u_1} [CommRing A] [IsLocalRing A] {C : Type u_2} [CommRing C] [Algebra A C] {B : Type u_3} [CommRing B] [Algebra A B] [Module.Finite A B] (φ : C →ₐ[A] B) (hsup : φ.toLinearMap.range ⊔ IsLocalRing.maximalIdeal A • ⊤ = ⊤) : Function.Surjective ⇑φ

theorem injective_of_surjective_of_finrank_eq_of_domain {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {C : Type u_2} [CommRing C] [IsDomain C] [Algebra A C] [Module.Finite A C] {B : Type u_3} [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] (φ : C →ₐ[A] B) (hrank : Module.finrank A C = Module.finrank A B) (hsurj : Function.Surjective ⇑φ) : Function.Injective ⇑φ

theorem surjective_adjoinRoot_to_quotient {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {B : Type u_2} [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] (g : Polynomial A) (α : B) (hα_aeval : (Polynomial.aeval α) g = 0) (hg_monic : g.Monic) (hg_irr : Irreducible (Polynomial.map (IsLocalRing.residue A) g)) (hfinrank : Module.finrank A (AdjoinRoot g) = Module.finrank A B) : Function.Surjective ⇑((Ideal.Quotient.mk (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A))).comp (AdjoinRoot.liftHom g α hα_aeval).toRingHom)

theorem range_sup_maximalIdeal_smul_eq_top_of_adjoinRoot_liftHom {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {B : Type u_2} [CommRing B] [IsDomain B] [Algebra A B] [Module.Finite A B] (g : Polynomial A) (α : B) (hα_aeval : (Polynomial.aeval α) g = 0) (hg_monic : g.Monic) (hg_irr : Irreducible (Polynomial.map (IsLocalRing.residue A) g)) (hfinrank : Module.finrank A (AdjoinRoot g) = Module.finrank A B) : (AdjoinRoot.liftHom g α hα_aeval).toLinearMap.range ⊔ IsLocalRing.maximalIdeal A • ⊤ = ⊤

theorem dvr_unramified_monogenicity (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [IsAdicComplete (IsLocalRing.maximalIdeal B) B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [IsUnramifiedDVRExtension A B] : ∃ (g : Polynomial A) (_ : g.Monic), (Polynomial.map (IsLocalRing.residue A) g).Separable ∧ Nonempty (B ≃ₐ[A] AdjoinRoot g)

theorem adjoinRoot_minpoly_ringEquiv {k : Type u_1} [Field k] {l : Type u_2} [Field l] [Algebra k l] [FiniteDimensional k l] (α : l) (hα : k⟮α⟯ = ⊤) (hint : IsIntegral k α) : Nonempty (AdjoinRoot (minpoly k α) ≃+* l)

theorem residue_comp_algebraMap_eq {A : Type u_1} [CommRing A] [IsLocalRing A] {B : Type u_2} [CommRing B] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] : (IsLocalRing.residue B).comp (algebraMap A B) = (algebraMap (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)).comp (IsLocalRing.residue A)

theorem residue_aeval_eq {A : Type u_1} [CommRing A] [IsLocalRing A] {B : Type u_2} [CommRing B] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] (p : Polynomial A) (b : B) : (IsLocalRing.residue B) ((Polynomial.aeval b) p) = (Polynomial.aeval ((IsLocalRing.residue B) b)) (Polynomial.map (IsLocalRing.residue A) p)

theorem adjoin_residue_top_of_adjoin_top {A : Type u_1} [CommRing A] [IsLocalRing A] {B : Type u_2} [CommRing B] [IsLocalRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] (α : B) (htop : A[α] = ⊤) : (IsLocalRing.ResidueField A)[(IsLocalRing.residue B) α] = ⊤

theorem dvr_extension_henselian (B : Type u_4) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [IsAdicComplete (IsLocalRing.maximalIdeal B) B] : HenselianLocalRing B

noncomputable def residueFieldFunctorAlg {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] {B₁ : Type u_2} [CommRing B₁] [IsDomain B₁] [IsDiscreteValuationRing B₁] [Algebra A B₁] [IsLocalHom (algebraMap A B₁)] {B₂ : Type u_3} [CommRing B₂] [IsDomain B₂] [IsDiscreteValuationRing B₂] [Algebra A B₂] [IsLocalHom (algebraMap A B₂)] [Module.Finite A B₂] (φ : B₁ →ₐ[A] B₂) : IsLocalRing.ResidueField B₁ →ₐ[IsLocalRing.ResidueField A] IsLocalRing.ResidueField B₂

theorem residueFieldFunctor_full_faithfulness {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] {B₁ : Type u_2} [CommRing B₁] [IsDomain B₁] [IsDiscreteValuationRing B₁] [Algebra A B₁] [IsLocalHom (algebraMap A B₁)] [Module.Finite A B₁] [IsAdicComplete (IsLocalRing.maximalIdeal B₁) B₁] {B₂ : Type u_3} [CommRing B₂] [IsDomain B₂] [IsDiscreteValuationRing B₂] [Algebra A B₂] [IsLocalHom (algebraMap A B₂)] [Module.Finite A B₂] [IsAdicComplete (IsLocalRing.maximalIdeal B₂) B₂] [IsUnramifiedDVRExtension A B₁] [IsUnramifiedDVRExtension A B₂] : Function.Bijective residueFieldFunctorAlg

theorem residueFieldFunctor_essential_surjectivity {A : Type} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] (l : Type) [Field l] [Algebra (IsLocalRing.ResidueField A) l] [FiniteDimensional (IsLocalRing.ResidueField A) l] [Algebra.IsSeparable (IsLocalRing.ResidueField A) l] : ∃ (B : Type) (x : CommRing B) (x_1 : IsDomain B) (x_2 : IsDiscreteValuationRing B) (x_3 : Algebra A B) (_ : IsLocalHom (algebraMap A B)) (_ : Module.Finite A B) (hAlg : Algebra (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (_ : FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (_ : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)), Nonempty (IsLocalRing.ResidueField B ≃+* l)

theorem residueFieldFunctor_injectivity {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] {B₁ : Type u_2} [CommRing B₁] [IsDomain B₁] [IsDiscreteValuationRing B₁] [Algebra A B₁] [IsLocalHom (algebraMap A B₁)] [Module.Finite A B₁] [IsAdicComplete (IsLocalRing.maximalIdeal B₁) B₁] {B₂ : Type u_3} [CommRing B₂] [IsDomain B₂] [IsDiscreteValuationRing B₂] [Algebra A B₂] [IsLocalHom (algebraMap A B₂)] [Module.Finite A B₂] [IsAdicComplete (IsLocalRing.maximalIdeal B₂) B₂] [IsUnramifiedDVRExtension A B₁] [IsUnramifiedDVRExtension A B₂] (e : IsLocalRing.ResidueField B₁ ≃ₐ[IsLocalRing.ResidueField A] IsLocalRing.ResidueField B₂) : Nonempty (B₁ ≃ₐ[A] B₂)

theorem residueFieldFunctor_isEquivalence {A : Type} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [HenselianLocalRing A] {B₁ : Type} [CommRing B₁] [IsDomain B₁] [IsDiscreteValuationRing B₁] [Algebra A B₁] [IsLocalHom (algebraMap A B₁)] [Module.Finite A B₁] [IsAdicComplete (IsLocalRing.maximalIdeal B₁) B₁] {B₂ : Type} [CommRing B₂] [IsDomain B₂] [IsDiscreteValuationRing B₂] [Algebra A B₂] [IsLocalHom (algebraMap A B₂)] [Module.Finite A B₂] [IsAdicComplete (IsLocalRing.maximalIdeal B₂) B₂] [IsUnramifiedDVRExtension A B₁] [IsUnramifiedDVRExtension A B₂] : Function.Bijective residueFieldFunctorAlg ∧ (∀ (l : Type) [inst : Field l] [inst_1 : Algebra (IsLocalRing.ResidueField A) l] [FiniteDimensional (IsLocalRing.ResidueField A) l] [Algebra.IsSeparable (IsLocalRing.ResidueField A) l], ∃ (B : Type) (x : CommRing B) (x_1 : IsDomain B) (x_2 : IsDiscreteValuationRing B) (x_3 : Algebra A B) (_ : IsLocalHom (algebraMap A B)) (_ : Module.Finite A B) (hAlg : Algebra (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (_ : FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) (_ : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)), Nonempty (IsLocalRing.ResidueField B ≃+* l)) ∧ ∀ (x : IsLocalRing.ResidueField B₁ ≃ₐ[IsLocalRing.ResidueField A] IsLocalRing.ResidueField B₂), Nonempty (B₁ ≃ₐ[A] B₂)